MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2re Structured version   Unicode version

Theorem 2re 10061
Description: The number 2 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
2re  |-  2  e.  RR

Proof of Theorem 2re
StepHypRef Expression
1 df-2 10050 . 2  |-  2  =  ( 1  +  1 )
2 1re 9082 . . 3  |-  1  e.  RR
32, 2readdcli 9095 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2505 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1725  (class class class)co 6073   RRcr 8981   1c1 8983    + caddc 8985   2c2 10041
This theorem is referenced by:  2cn  10062  3re  10063  2ne0  10075  3pos  10076  2lt3  10135  1lt3  10136  2lt4  10138  1lt4  10139  2lt5  10142  2lt6  10147  1lt6  10148  2lt7  10153  1lt7  10154  2lt8  10160  1lt8  10161  2lt9  10168  1lt9  10169  2lt10  10177  1lt10  10178  halfgt0  10180  halflt1  10181  halfpm6th  10184  rehalfcl  10186  halfpos2  10189  halfnneg2  10191  addltmul  10195  nominpos  10196  avglt1  10197  avglt2  10198  nn0lele2xi  10264  nn0n0n1ge2b  10273  halfnz  10340  2rp  10609  fzprval  11098  fztpval  11099  4fvwrd4  11113  fzo0to42pr  11178  flhalf  11223  expubnd  11432  expmulnbnd  11503  nn0opthlem2  11554  faclbnd2  11574  faclbnd4lem1  11576  faclbnd5  11581  hashfun  11692  f1oun2prg  11856  sqrlem7  12046  sqr4  12070  sqr2gt1lt2  12072  abstri  12126  rddif  12136  absrdbnd  12137  sqreulem  12155  amgm2  12165  caucvgrlem  12458  iseralt  12470  climcndslem1  12621  climcndslem2  12622  climcnds  12623  geoihalfsum  12651  efcllem  12672  ege2le3  12684  ef01bndlem  12777  cos01bnd  12779  cos2bnd  12781  cos01gt0  12784  sin02gt0  12785  sincos2sgn  12787  sin4lt0  12788  eirrlem  12795  egt2lt3  12797  epos  12798  sqr2re  12841  oexpneg  12903  bitsp1o  12937  bitsfzolem  12938  bitsfzo  12939  bitsmod  12940  bitsfi  12941  bitsinv1lem  12945  isprm3  13080  oddprm  13181  iserodd  13201  prmreclem2  13277  prmreclem6  13281  4sqlem11  13315  4sqlem12  13316  2expltfac  13418  oppgtset  15140  efgredleme  15367  mgpsca  15647  mgptset  15648  mgpds  15650  abvtrivd  15920  psmetge0  18335  xmetge0  18366  bl2in  18422  metnrmlem3  18883  iihalf1  18948  iihalf2  18950  pcoass  19041  tchcphlem1  19184  minveclem2  19319  minveclem4  19325  pjthlem1  19330  ovolunlem1a  19384  dyadss  19478  opnmbllem  19485  vitalilem2  19493  vitalilem4  19495  mbfi1fseqlem5  19603  lhop1lem  19889  aaliou3lem1  20251  aaliou3lem2  20252  aaliou3lem3  20253  aaliou3lem8  20254  pilem2  20360  pilem3  20361  pipos  20365  sinhalfpilem  20366  sincosq1lem  20397  sincosq4sgn  20401  tangtx  20405  sinq12gt0  20407  sincos4thpi  20413  tan4thpi  20414  sincos6thpi  20415  sineq0  20421  cosordlem  20425  tanord1  20431  efif1olem1  20436  efif1olem2  20437  efif1olem4  20439  efif1o  20440  efifo  20441  logsqr  20587  cxpcn3lem  20623  root1id  20630  root1eq1  20631  root1cj  20632  cxpeq  20633  ang180lem1  20643  ang180lem2  20644  chordthmlem2  20666  1cubrlem  20673  atancj  20742  atantan  20755  atanbndlem  20757  atans2  20763  leibpilem1  20772  leibpi  20774  log2tlbnd  20777  log2ublem2  20779  log2ub  20781  divsqrsumlem  20810  harmonicbnd3  20838  basellem1  20855  basellem2  20856  basellem3  20857  basellem5  20859  ppisval  20878  chtdif  20933  ppidif  20938  ppinncl  20949  chtrpcl  20950  ppieq0  20951  ppiltx  20952  ppiublem1  20978  ppiub  20980  chpeq0  20984  chteq0  20985  chtublem  20987  chtub  20988  chpval2  20994  chpub  20996  mersenne  21003  perfectlem1  21005  perfectlem2  21006  dchrptlem1  21040  dchrptlem2  21041  bcmono  21053  bclbnd  21056  bpos1lem  21058  bposlem1  21060  bposlem2  21061  bposlem3  21062  bposlem4  21063  bposlem5  21064  bposlem6  21065  bposlem7  21066  bposlem8  21067  bposlem9  21068  lgslem1  21072  lgsdirprm  21105  lgseisenlem1  21125  lgseisenlem2  21126  lgseisenlem3  21127  lgseisen  21129  lgsquadlem1  21130  lgsquadlem2  21131  m1lgs  21138  2sqlem11  21151  chebbnd1lem1  21155  chebbnd1lem2  21156  chebbnd1lem3  21157  chebbnd1  21158  chtppilimlem1  21159  chtppilimlem2  21160  chtppilim  21161  chto1ub  21162  chebbnd2  21163  chto1lb  21164  chpchtlim  21165  chpo1ub  21166  chpo1ubb  21167  rplogsumlem1  21170  rplogsumlem2  21171  dchrisumlem2  21176  dchrisumlem3  21177  dchrvmasumiflem1  21187  dchrisum0fno1  21197  dchrisum0re  21199  dchrisum0lem1b  21201  dchrisum0lem1  21202  dchrisum0lem2  21204  rplogsum  21213  mulog2sumlem1  21220  mulog2sumlem2  21221  log2sumbnd  21230  selberglem2  21232  selbergb  21235  selberg2b  21238  chpdifbndlem1  21239  logdivbnd  21242  selberg3lem1  21243  selberg3  21245  selberg4lem1  21246  selberg4  21247  pntrmax  21250  pntrsumbnd2  21253  selberg3r  21255  selberg4r  21256  selberg34r  21257  pntrlog2bndlem2  21264  pntrlog2bndlem3  21265  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  pntrlog2bndlem6  21269  pntrlog2bnd  21270  pntpbnd1a  21271  pntpbnd1  21272  pntpbnd2  21273  pntpbnd  21274  pntibndlem2  21277  pntibndlem3  21278  pntibnd  21279  pntlemb  21283  pntlemg  21284  pntlemh  21285  pntlemr  21288  pntlemk  21292  pntlemo  21293  pnt2  21299  pnt  21300  ostth2lem1  21304  ostth3  21324  umgrafi  21349  usisuslgra  21379  usgraexvlem  21406  usgraex2elv  21409  usgraexmpldifpr  21411  wlkntrllem2  21552  constr3lem4  21626  constr3trllem3  21631  constr3pthlem1  21634  constr3pthlem3  21636  konigsberg  21701  ex-pss  21728  ex-res  21741  ex-fv  21743  ex-fl  21747  nvge0  22155  ipidsq  22201  minvecolem2  22369  minvecolem4  22374  normlem7  22610  norm-ii-i  22631  norm3lemt  22646  normpar2i  22650  bcsiALT  22673  pjhthlem1  22885  opsqrlem6  23640  cdj3lem1  23929  addltmulALT  23941  sqsscirc1  24298  rnlogblem  24391  dya2iocucvr  24626  coinfliplem  24728  coinflipspace  24730  ballotlem2  24738  zetacvg  24791  lgamgulmlem2  24806  lgamgulmlem3  24807  lgamgulmlem4  24808  lgamgulmlem6  24810  lgamucov  24814  subfacp1lem1  24857  subfacp1lem5  24862  subfacval3  24867  circum  25103  4bc2eq6  25196  axlowdimlem3  25875  axlowdimlem4  25876  axlowdimlem6  25878  axlowdimlem16  25888  axlowdimlem17  25889  axlowdim  25892  mblfinlem  26234  itg2addnclem  26246  nn0prpwlem  26316  csbrn  26447  trirn  26448  isbnd2  26483  isbnd3  26484  heiborlem7  26517  rabren3dioph  26867  pellexlem2  26884  pellexlem5  26887  pell14qrgapw  26930  pellfundex  26940  rmspecsqrnq  26960  jm2.24nn  27015  jm2.17a  27016  jm2.17b  27017  jm2.17c  27018  acongrep  27036  acongeq  27039  jm2.22  27057  jm2.23  27058  jm2.20nn  27059  jm3.1lem2  27080  expdiophlem1  27083  matplusg  27437  lhe4.4ex1a  27514  stoweidlem13  27729  stoweidlem14  27730  stoweidlem26  27742  stoweidlem49  27765  stoweidlem52  27768  wallispilem4  27784  wallispilem5  27785  wallispi  27786  wallispi2lem1  27787  wallispi2lem2  27788  wallispi2  27789  stirlinglem1  27790  stirlinglem3  27792  stirlinglem5  27794  stirlinglem6  27795  stirlinglem7  27796  stirlinglem10  27799  stirlinglem11  27800  stirlinglem15  27804  stirlingr  27806  2leaddle2  28077  2eluzge0  28086  2eluzge1  28087  2txmodxeq0  28140  2cshwmod  28223  usgra2pthlem1  28263  vdgfrgragt2  28355  ene1  28468  isosctrlem1ALT  28983  sineq0ALT  28986
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-i2m1 9050  ax-1ne0 9051  ax-rrecex 9054  ax-cnre 9055
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076  df-2 10050
  Copyright terms: Public domain W3C validator