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

Theorem 2re 10033
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 10022 . 2  |-  2  =  ( 1  +  1 )
2 1re 9054 . . 3  |-  1  e.  RR
32, 2readdcli 9067 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2482 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1721  (class class class)co 6048   RRcr 8953   1c1 8955    + caddc 8957   2c2 10013
This theorem is referenced by:  2cn  10034  3re  10035  2ne0  10047  3pos  10048  2lt3  10107  1lt3  10108  2lt4  10110  1lt4  10111  2lt5  10114  2lt6  10119  1lt6  10120  2lt7  10125  1lt7  10126  2lt8  10132  1lt8  10133  2lt9  10140  1lt9  10141  2lt10  10149  1lt10  10150  halfgt0  10152  halflt1  10153  halfpm6th  10156  rehalfcl  10158  halfpos2  10161  halfnneg2  10163  addltmul  10167  nominpos  10168  avglt1  10169  avglt2  10170  nn0lele2xi  10236  nn0n0n1ge2b  10245  halfnz  10312  2rp  10581  fzprval  11070  fztpval  11071  4fvwrd4  11084  fzo0to42pr  11149  flhalf  11194  expubnd  11403  expmulnbnd  11474  nn0opthlem2  11525  faclbnd2  11545  faclbnd4lem1  11547  faclbnd5  11552  hashfun  11663  f1oun2prg  11827  sqrlem7  12017  sqr4  12041  sqr2gt1lt2  12043  abstri  12097  rddif  12107  absrdbnd  12108  sqreulem  12126  amgm2  12136  caucvgrlem  12429  iseralt  12441  climcndslem1  12592  climcndslem2  12593  climcnds  12594  geoihalfsum  12622  efcllem  12643  ege2le3  12655  ef01bndlem  12748  cos01bnd  12750  cos2bnd  12752  cos01gt0  12755  sin02gt0  12756  sincos2sgn  12758  sin4lt0  12759  eirrlem  12766  egt2lt3  12768  epos  12769  sqr2re  12812  oexpneg  12874  bitsp1o  12908  bitsfzolem  12909  bitsfzo  12910  bitsmod  12911  bitsfi  12912  bitsinv1lem  12916  isprm3  13051  oddprm  13152  iserodd  13172  prmreclem2  13248  prmreclem6  13252  4sqlem11  13286  4sqlem12  13287  2expltfac  13389  oppgtset  15111  efgredleme  15338  mgpsca  15618  mgptset  15619  mgpds  15621  abvtrivd  15891  psmetge0  18304  xmetge0  18335  bl2in  18391  metnrmlem3  18852  iihalf1  18917  iihalf2  18919  pcoass  19010  tchcphlem1  19153  minveclem2  19288  minveclem4  19294  pjthlem1  19299  ovolunlem1a  19353  dyadss  19447  opnmbllem  19454  vitalilem2  19462  vitalilem4  19464  mbfi1fseqlem5  19572  lhop1lem  19858  aaliou3lem1  20220  aaliou3lem2  20221  aaliou3lem3  20222  aaliou3lem8  20223  pilem2  20329  pilem3  20330  pipos  20334  sinhalfpilem  20335  sincosq1lem  20366  sincosq4sgn  20370  tangtx  20374  sinq12gt0  20376  sincos4thpi  20382  tan4thpi  20383  sincos6thpi  20384  sineq0  20390  cosordlem  20394  tanord1  20400  efif1olem1  20405  efif1olem2  20406  efif1olem4  20408  efif1o  20409  efifo  20410  logsqr  20556  cxpcn3lem  20592  root1id  20599  root1eq1  20600  root1cj  20601  cxpeq  20602  ang180lem1  20612  ang180lem2  20613  chordthmlem2  20635  1cubrlem  20642  atancj  20711  atantan  20724  atanbndlem  20726  atans2  20732  leibpilem1  20741  leibpi  20743  log2tlbnd  20746  log2ublem2  20748  log2ub  20750  divsqrsumlem  20779  harmonicbnd3  20807  basellem1  20824  basellem2  20825  basellem3  20826  basellem5  20828  ppisval  20847  chtdif  20902  ppidif  20907  ppinncl  20918  chtrpcl  20919  ppieq0  20920  ppiltx  20921  ppiublem1  20947  ppiub  20949  chpeq0  20953  chteq0  20954  chtublem  20956  chtub  20957  chpval2  20963  chpub  20965  mersenne  20972  perfectlem1  20974  perfectlem2  20975  dchrptlem1  21009  dchrptlem2  21010  bcmono  21022  bclbnd  21025  bpos1lem  21027  bposlem1  21029  bposlem2  21030  bposlem3  21031  bposlem4  21032  bposlem5  21033  bposlem6  21034  bposlem7  21035  bposlem8  21036  bposlem9  21037  lgslem1  21041  lgsdirprm  21074  lgseisenlem1  21094  lgseisenlem2  21095  lgseisenlem3  21096  lgseisen  21098  lgsquadlem1  21099  lgsquadlem2  21100  m1lgs  21107  2sqlem11  21120  chebbnd1lem1  21124  chebbnd1lem2  21125  chebbnd1lem3  21126  chebbnd1  21127  chtppilimlem1  21128  chtppilimlem2  21129  chtppilim  21130  chto1ub  21131  chebbnd2  21132  chto1lb  21133  chpchtlim  21134  chpo1ub  21135  chpo1ubb  21136  rplogsumlem1  21139  rplogsumlem2  21140  dchrisumlem2  21145  dchrisumlem3  21146  dchrvmasumiflem1  21156  dchrisum0fno1  21166  dchrisum0re  21168  dchrisum0lem1b  21170  dchrisum0lem1  21171  dchrisum0lem2  21173  rplogsum  21182  mulog2sumlem1  21189  mulog2sumlem2  21190  log2sumbnd  21199  selberglem2  21201  selbergb  21204  selberg2b  21207  chpdifbndlem1  21208  logdivbnd  21211  selberg3lem1  21212  selberg3  21214  selberg4lem1  21215  selberg4  21216  pntrmax  21219  pntrsumbnd2  21222  selberg3r  21224  selberg4r  21225  selberg34r  21226  pntrlog2bndlem2  21233  pntrlog2bndlem3  21234  pntrlog2bndlem4  21235  pntrlog2bndlem5  21236  pntrlog2bndlem6  21238  pntrlog2bnd  21239  pntpbnd1a  21240  pntpbnd1  21241  pntpbnd2  21242  pntpbnd  21243  pntibndlem2  21246  pntibndlem3  21247  pntibnd  21248  pntlemb  21252  pntlemg  21253  pntlemh  21254  pntlemr  21257  pntlemk  21261  pntlemo  21262  pnt2  21268  pnt  21269  ostth2lem1  21273  ostth3  21293  umgrafi  21318  usisuslgra  21348  usgraexvlem  21375  usgraex2elv  21378  usgraexmpldifpr  21380  wlkntrllem2  21521  constr3lem4  21595  constr3trllem3  21600  constr3pthlem1  21603  constr3pthlem3  21605  konigsberg  21670  ex-pss  21697  ex-res  21710  ex-fv  21712  ex-fl  21716  nvge0  22124  ipidsq  22170  minvecolem2  22338  minvecolem4  22343  normlem7  22579  norm-ii-i  22600  norm3lemt  22615  normpar2i  22619  bcsiALT  22642  pjhthlem1  22854  opsqrlem6  23609  cdj3lem1  23898  addltmulALT  23910  sqsscirc1  24267  rnlogblem  24360  dya2iocucvr  24595  coinfliplem  24697  coinflipspace  24699  ballotlem2  24707  zetacvg  24760  lgamgulmlem2  24775  lgamgulmlem3  24776  lgamgulmlem4  24777  lgamgulmlem6  24779  lgamucov  24783  subfacp1lem1  24826  subfacp1lem5  24831  subfacval3  24836  circum  25072  4bc2eq6  25165  axlowdimlem3  25795  axlowdimlem4  25796  axlowdimlem6  25798  axlowdimlem16  25808  axlowdimlem17  25809  axlowdim  25812  mblfinlem  26151  itg2addnclem  26163  nn0prpwlem  26223  csbrn  26354  trirn  26355  isbnd2  26390  isbnd3  26391  heiborlem7  26424  rabren3dioph  26774  pellexlem2  26791  pellexlem5  26794  pell14qrgapw  26837  pellfundex  26847  rmspecsqrnq  26867  jm2.24nn  26922  jm2.17a  26923  jm2.17b  26924  jm2.17c  26925  acongrep  26943  acongeq  26946  jm2.22  26964  jm2.23  26965  jm2.20nn  26966  jm3.1lem2  26987  expdiophlem1  26990  matplusg  27345  lhe4.4ex1a  27422  stoweidlem13  27637  stoweidlem14  27638  stoweidlem26  27650  stoweidlem49  27673  stoweidlem52  27676  wallispilem4  27692  wallispilem5  27693  wallispi  27694  wallispi2lem1  27695  wallispi2lem2  27696  wallispi2  27697  stirlinglem1  27698  stirlinglem3  27700  stirlinglem5  27702  stirlinglem6  27703  stirlinglem7  27704  stirlinglem10  27707  stirlinglem11  27708  stirlinglem15  27712  stirlingr  27714  usgra2pthlem1  28048  vdgfrgragt2  28140  ene1  28253  isosctrlem1ALT  28765
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-i2m1 9022  ax-1ne0 9023  ax-rrecex 9026  ax-cnre 9027
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-iota 5385  df-fv 5429  df-ov 6051  df-2 10022
  Copyright terms: Public domain W3C validator