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

Theorem 2re 10107
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 10096 . 2  |-  2  =  ( 1  +  1 )
2 1re 9128 . . 3  |-  1  e.  RR
32, 2readdcli 9141 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2513 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1728  (class class class)co 6117   RRcr 9027   1c1 9029    + caddc 9031   2c2 10087
This theorem is referenced by:  2cn  10108  3re  10109  2ne0  10121  3pos  10122  2lt3  10181  1lt3  10182  2lt4  10184  1lt4  10185  2lt5  10188  2lt6  10193  1lt6  10194  2lt7  10199  1lt7  10200  2lt8  10206  1lt8  10207  2lt9  10214  1lt9  10215  2lt10  10223  1lt10  10224  halfgt0  10226  halflt1  10227  halfpm6th  10230  rehalfcl  10232  halfpos2  10235  halfnneg2  10237  addltmul  10241  nominpos  10242  avglt1  10243  avglt2  10244  nn0lele2xi  10310  nn0n0n1ge2b  10319  halfnz  10386  2rp  10655  fzprval  11144  fztpval  11145  4fvwrd4  11159  fzo0to42pr  11224  flhalf  11269  expubnd  11478  expmulnbnd  11549  nn0opthlem2  11600  faclbnd2  11620  faclbnd4lem1  11622  faclbnd5  11627  hashfun  11738  f1oun2prg  11902  sqrlem7  12092  sqr4  12116  sqr2gt1lt2  12118  abstri  12172  rddif  12182  absrdbnd  12183  sqreulem  12201  amgm2  12211  caucvgrlem  12504  iseralt  12516  climcndslem1  12667  climcndslem2  12668  climcnds  12669  geoihalfsum  12697  efcllem  12718  ege2le3  12730  ef01bndlem  12823  cos01bnd  12825  cos2bnd  12827  cos01gt0  12830  sin02gt0  12831  sincos2sgn  12833  sin4lt0  12834  eirrlem  12841  egt2lt3  12843  epos  12844  sqr2re  12887  oexpneg  12949  bitsp1o  12983  bitsfzolem  12984  bitsfzo  12985  bitsmod  12986  bitsfi  12987  bitsinv1lem  12991  isprm3  13126  oddprm  13227  iserodd  13247  prmreclem2  13323  prmreclem6  13327  4sqlem11  13361  4sqlem12  13362  2expltfac  13464  oppgtset  15186  efgredleme  15413  mgpsca  15693  mgptset  15694  mgpds  15696  abvtrivd  15966  psmetge0  18381  xmetge0  18412  bl2in  18468  metnrmlem3  18929  iihalf1  18994  iihalf2  18996  pcoass  19087  tchcphlem1  19230  minveclem2  19365  minveclem4  19371  pjthlem1  19376  ovolunlem1a  19430  dyadss  19524  opnmbllem  19531  vitalilem2  19539  vitalilem4  19541  mbfi1fseqlem5  19647  lhop1lem  19935  aaliou3lem1  20297  aaliou3lem2  20298  aaliou3lem3  20299  aaliou3lem8  20300  pilem2  20406  pilem3  20407  pipos  20411  sinhalfpilem  20412  sincosq1lem  20443  sincosq4sgn  20447  tangtx  20451  sinq12gt0  20453  sincos4thpi  20459  tan4thpi  20460  sincos6thpi  20461  sineq0  20467  cosordlem  20471  tanord1  20477  efif1olem1  20482  efif1olem2  20483  efif1olem4  20485  efif1o  20486  efifo  20487  logsqr  20633  cxpcn3lem  20669  root1id  20676  root1eq1  20677  root1cj  20678  cxpeq  20679  ang180lem1  20689  ang180lem2  20690  chordthmlem2  20712  1cubrlem  20719  atancj  20788  atantan  20801  atanbndlem  20803  atans2  20809  leibpilem1  20818  leibpi  20820  log2tlbnd  20823  log2ublem2  20825  log2ub  20827  divsqrsumlem  20856  harmonicbnd3  20884  basellem1  20901  basellem2  20902  basellem3  20903  basellem5  20905  ppisval  20924  chtdif  20979  ppidif  20984  ppinncl  20995  chtrpcl  20996  ppieq0  20997  ppiltx  20998  ppiublem1  21024  ppiub  21026  chpeq0  21030  chteq0  21031  chtublem  21033  chtub  21034  chpval2  21040  chpub  21042  mersenne  21049  perfectlem1  21051  perfectlem2  21052  dchrptlem1  21086  dchrptlem2  21087  bcmono  21099  bclbnd  21102  bpos1lem  21104  bposlem1  21106  bposlem2  21107  bposlem3  21108  bposlem4  21109  bposlem5  21110  bposlem6  21111  bposlem7  21112  bposlem8  21113  bposlem9  21114  lgslem1  21118  lgsdirprm  21151  lgseisenlem1  21171  lgseisenlem2  21172  lgseisenlem3  21173  lgseisen  21175  lgsquadlem1  21176  lgsquadlem2  21177  m1lgs  21184  2sqlem11  21197  chebbnd1lem1  21201  chebbnd1lem2  21202  chebbnd1lem3  21203  chebbnd1  21204  chtppilimlem1  21205  chtppilimlem2  21206  chtppilim  21207  chto1ub  21208  chebbnd2  21209  chto1lb  21210  chpchtlim  21211  chpo1ub  21212  chpo1ubb  21213  rplogsumlem1  21216  rplogsumlem2  21217  dchrisumlem2  21222  dchrisumlem3  21223  dchrvmasumiflem1  21233  dchrisum0fno1  21243  dchrisum0re  21245  dchrisum0lem1b  21247  dchrisum0lem1  21248  dchrisum0lem2  21250  rplogsum  21259  mulog2sumlem1  21266  mulog2sumlem2  21267  log2sumbnd  21276  selberglem2  21278  selbergb  21281  selberg2b  21284  chpdifbndlem1  21285  logdivbnd  21288  selberg3lem1  21289  selberg3  21291  selberg4lem1  21292  selberg4  21293  pntrmax  21296  pntrsumbnd2  21299  selberg3r  21301  selberg4r  21302  selberg34r  21303  pntrlog2bndlem2  21310  pntrlog2bndlem3  21311  pntrlog2bndlem4  21312  pntrlog2bndlem5  21313  pntrlog2bndlem6  21315  pntrlog2bnd  21316  pntpbnd1a  21317  pntpbnd1  21318  pntpbnd2  21319  pntpbnd  21320  pntibndlem2  21323  pntibndlem3  21324  pntibnd  21325  pntlemb  21329  pntlemg  21330  pntlemh  21331  pntlemr  21334  pntlemk  21338  pntlemo  21339  pnt2  21345  pnt  21346  ostth2lem1  21350  ostth3  21370  umgrafi  21395  usisuslgra  21425  usgraexvlem  21452  usgraex2elv  21455  usgraexmpldifpr  21457  wlkntrllem2  21598  constr3lem4  21672  constr3trllem3  21677  constr3pthlem1  21680  constr3pthlem3  21682  konigsberg  21747  ex-pss  21774  ex-res  21787  ex-fv  21789  ex-fl  21793  nvge0  22201  ipidsq  22247  minvecolem2  22415  minvecolem4  22420  normlem7  22656  norm-ii-i  22677  norm3lemt  22692  normpar2i  22696  bcsiALT  22719  pjhthlem1  22931  opsqrlem6  23686  cdj3lem1  23975  addltmulALT  23987  sqsscirc1  24341  rnlogblem  24434  dya2iocucvr  24669  coinfliplem  24771  coinflipspace  24773  ballotlem2  24781  zetacvg  24834  lgamgulmlem2  24849  lgamgulmlem3  24850  lgamgulmlem4  24851  lgamgulmlem6  24853  lgamucov  24857  subfacp1lem1  24900  subfacp1lem5  24905  subfacval3  24910  circum  25146  4bc2eq6  25239  axlowdimlem3  25918  axlowdimlem4  25919  axlowdimlem6  25921  axlowdimlem16  25931  axlowdimlem17  25932  axlowdim  25935  sin2h  26278  cos2h  26279  tan2h  26280  opnmbllem0  26282  mblfinlem1  26283  mblfinlem2  26284  itg2addnclem  26298  nn0prpwlem  26367  csbrn  26498  trirn  26499  isbnd2  26534  isbnd3  26535  heiborlem7  26568  rabren3dioph  26988  pellexlem2  27005  pellexlem5  27008  pell14qrgapw  27051  pellfundex  27061  rmspecsqrnq  27081  jm2.24nn  27136  jm2.17a  27137  jm2.17b  27138  jm2.17c  27139  acongrep  27157  acongeq  27160  jm2.22  27178  jm2.23  27179  jm2.20nn  27180  jm3.1lem2  27201  expdiophlem1  27204  matplusg  27558  lhe4.4ex1a  27635  stoweidlem13  27850  stoweidlem14  27851  stoweidlem26  27863  stoweidlem49  27886  stoweidlem52  27889  wallispilem4  27905  wallispilem5  27906  wallispi  27907  wallispi2lem1  27908  wallispi2lem2  27909  wallispi2  27910  stirlinglem1  27911  stirlinglem3  27913  stirlinglem5  27915  stirlinglem6  27916  stirlinglem7  27917  stirlinglem10  27920  stirlinglem11  27921  stirlinglem15  27925  stirlingr  27927  2leaddle2  28213  2eluzge0  28222  2eluzge1  28223  2txmodxeq0  28283  wrdlenge2n0  28306  2cshwmod  28389  swrdtrcfvl  28397  usgra2pthlem1  28446  vdgfrgragt2  28590  ene1  28703  isosctrlem1ALT  29220  sineq0ALT  29223
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-1cn 9086  ax-icn 9087  ax-addcl 9088  ax-addrcl 9089  ax-mulcl 9090  ax-mulrcl 9091  ax-i2m1 9096  ax-1ne0 9097  ax-rrecex 9100  ax-cnre 9101
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-br 4244  df-iota 5453  df-fv 5497  df-ov 6120  df-2 10096
  Copyright terms: Public domain W3C validator