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

Theorem 2re 10849
Description: The number 2 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
2re 2 ∈ ℝ

Proof of Theorem 2re
StepHypRef Expression
1 df-2 10838 . 2 2 = (1 + 1)
2 1re 9798 . . 3 1 ∈ ℝ
32, 2readdcli 9812 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2588 1 2 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 1938  (class class class)co 6431  cr 9694  1c1 9696   + caddc 9698  2c2 10829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-1cn 9753  ax-icn 9754  ax-addcl 9755  ax-addrcl 9756  ax-mulcl 9757  ax-mulrcl 9758  ax-i2m1 9763  ax-1ne0 9764  ax-rrecex 9767  ax-cnre 9768
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-iota 5658  df-fv 5702  df-ov 6434  df-2 10838
This theorem is referenced by:  2cn  10850  3re  10853  2ne0  10872  3pos  10873  2lt3  10954  1lt3  10955  2lt4  10957  1lt4  10958  2lt5  10961  2lt6  10966  1lt6  10967  2lt7  10972  1lt7  10973  2lt8  10979  1lt8  10980  2lt9  10987  1lt9  10988  2lt10OLD  10996  1lt10OLD  10997  1le2  11000  2rene0  11002  halfre  11005  halfgt0  11007  halflt1  11009  rehalfcl  11017  halfpos2  11020  halfnneg2  11022  addltmul  11027  nominpos  11028  avglt1  11029  avglt2  11030  div4p1lem1div2  11046  nn0lele2xi  11107  nn0n0n1ge2b  11118  nn0ge2m1nn  11119  halfnz  11199  3halfnz  11200  2lt10  11424  1lt10  11425  uzuzle23  11473  uz3m2nn  11475  2rp  11583  zgt1rpn0n1  11617  fztpval  12144  fz0to4untppr  12183  fzo0to42pr  12294  2tnp1ge0ge0  12364  flhalf  12365  fldiv4p1lem1div2  12370  fldiv4lem1div2uz2  12371  2txmodxeq0  12464  expubnd  12655  expmulnbnd  12730  nn0opthlem2  12790  faclbnd2  12812  faclbnd4lem1  12814  faclbnd5  12819  4bc2eq6  12850  hashfun  12953  hashge2el2dif  12984  hashge2el2difr  12985  wrdlenge2n0  13059  f1oun2prg  13375  2swrd2eqwrdeq  13407  sqrlem7  13700  sqrt4  13724  sqrt2gt1lt2  13726  abstri  13781  sqreulem  13810  amgm2  13820  caucvgrlem  14121  caucvgrlemOLD  14122  iseralt  14136  climcndslem1  14293  climcndslem2  14294  climcnds  14295  geoihalfsum  14326  efcllem  14520  ege2le3  14532  ef01bndlem  14626  cos01bnd  14628  cos2bnd  14630  cos01gt0  14633  sin02gt0  14634  sincos2sgn  14636  sin4lt0  14637  eirrlem  14644  egt2lt3  14646  epos  14647  ene1  14650  sqrt2re  14691  oexpneg  14780  mod2eq1n2dvds  14782  oddge22np1  14784  evennn02n  14785  evennn2n  14786  nn0ehalf  14806  nn0o1gt2  14808  nno  14809  nn0o  14810  nn0oddm1d2  14812  nnoddm1d2  14813  n2dvds1  14815  flodddiv4t2lthalf  14854  bitsp1o  14869  bitsfzolem  14870  bitsfzolemOLD  14871  bitsfzo  14872  bitsfi  14874  6gcd4e2  14970  isprm7  15138  3lcm2e6  15158  oddprm  15241  iserodd  15266  prmreclem2  15347  prmreclem6  15351  4sqlem11  15385  4sqlem12  15386  prmgaplem7  15487  2expltfac  15525  oppgtset  17501  efgredleme  17891  mgpsca  18230  mgptset  18231  mgpds  18233  matplusg  19946  chfacfscmul0  20389  chfacfpmmul0  20393  psmetge0  21834  xmetge0  21865  bl2in  21921  metnrmlem3  22384  metnrmlem3OLD  22399  iihalf1  22465  iihalf2  22467  pcoass  22559  tchcphlem1  22713  csbren  22857  trirn  22858  minveclem2  22872  minveclem4  22878  minveclem2OLD  22884  minveclem4OLD  22890  pjthlem1  22895  ovolunlem1a  22950  dyadss  23047  opnmbllem  23054  vitalilem2  23063  vitalilem4  23065  mbfi1fseqlem5  23171  lhop1lem  23459  aaliou3lem2  23793  aaliou3lem8  23795  pilem2  23901  pilem3  23902  pipos  23907  sinhalfpilem  23910  sincosq1lem  23944  sincosq4sgn  23948  tangtx  23952  sinq12gt0  23954  sincos4thpi  23960  tan4thpi  23961  sincos6thpi  23962  sineq0  23968  cosordlem  23972  tanord1  23978  efif1olem1  23983  efif1olem2  23984  efif1olem4  23986  efif1o  23987  efifo  23988  cxpcn3lem  24179  root1id  24186  root1eq1  24187  root1cj  24188  cxpeq  24189  logblog  24221  ang180lem1  24230  ang180lem2  24231  chordthmlem2  24251  1cubrlem  24259  atancj  24328  atantan  24341  atanbndlem  24343  atans2  24349  leibpilem1  24358  leibpi  24360  log2tlbnd  24363  log2ublem2  24365  log2ub  24367  divsqrtsumlem  24397  harmonicbnd3  24425  zetacvg  24432  lgamgulmlem2  24447  lgamgulmlem3  24448  lgamgulmlem4  24449  lgamgulmlem6  24451  lgamucov  24455  basellem1  24500  basellem2  24501  basellem3  24502  basellem5  24504  chtdif  24577  ppidif  24582  ppinncl  24593  chtrpcl  24594  ppieq0  24595  ppiltx  24596  ppiublem1  24620  ppiub  24622  chpeq0  24626  chteq0  24627  chtublem  24629  chtub  24630  chpval2  24636  chpub  24638  mersenne  24645  perfectlem1  24647  perfectlem2  24648  dchrptlem1  24682  dchrptlem2  24683  bcmono  24695  bclbnd  24698  bpos1lem  24700  bposlem1  24702  bposlem2  24703  bposlem3  24704  bposlem4  24705  bposlem5  24706  bposlem6  24707  bposlem7  24708  bposlem8  24709  bposlem9  24710  lgslem1  24715  lgsdirprm  24749  gausslemma2dlem0c  24776  gausslemma2dlem1a  24783  gausslemma2dlem2  24785  gausslemma2dlem3  24786  lgseisenlem1  24793  lgseisenlem2  24794  lgseisenlem3  24795  lgseisen  24797  lgsquadlem1  24798  lgsquadlem2  24799  m1lgs  24806  2lgslem1a1  24807  2lgslem1a2  24808  2lgslem1c  24811  2lgslem4  24824  2sqlem11  24847  chebbnd1lem1  24851  chebbnd1lem2  24852  chebbnd1lem3  24853  chebbnd1  24854  chtppilimlem1  24855  chtppilimlem2  24856  chtppilim  24857  chto1ub  24858  chebbnd2  24859  chto1lb  24860  chpchtlim  24861  chpo1ub  24862  chpo1ubb  24863  rplogsumlem1  24866  rplogsumlem2  24867  dchrisumlem2  24872  dchrisumlem3  24873  dchrvmasumiflem1  24883  dchrisum0fno1  24893  dchrisum0re  24895  dchrisum0lem1b  24897  dchrisum0lem1  24898  dchrisum0lem2  24900  rplogsum  24909  mulog2sumlem1  24916  mulog2sumlem2  24917  log2sumbnd  24926  selberglem2  24928  selbergb  24931  selberg2b  24934  chpdifbndlem1  24935  logdivbnd  24938  selberg3lem1  24939  selberg3  24941  selberg4lem1  24942  selberg4  24943  pntrmax  24946  pntrsumbnd2  24949  selberg3r  24951  selberg4r  24952  selberg34r  24953  pntrlog2bndlem2  24960  pntrlog2bndlem3  24961  pntrlog2bndlem4  24962  pntrlog2bndlem5  24963  pntrlog2bndlem6  24965  pntrlog2bnd  24966  pntpbnd1a  24967  pntpbnd1  24968  pntpbnd2  24969  pntpbnd  24970  pntibndlem2  24973  pntibndlem3  24974  pntibnd  24975  pntlemb  24979  pntlemg  24980  pntlemh  24981  pntlemr  24984  pntlemk  24988  pntlemo  24989  pnt2  24995  pnt  24996  ostth2lem1  25000  ostth3  25020  istrkg3ld  25053  tgldimor  25090  trgcgrg  25104  tgcgr4  25120  axlowdimlem6  25521  axlowdimlem16  25531  axlowdimlem17  25532  axlowdim  25535  umgrafi  25593  usisuslgra  25636  usgraex2elv  25668  usgraexmpldifpr  25670  constr3lem4  25917  constr3trllem3  25922  constr3pthlem1  25925  constr3pthlem3  25927  wwlkextwrd  25998  wwlkextfun  25999  wwlkextinj  26000  wwlkm1edg  26005  wwlkextproplem3  26013  clwwlkgt0  26041  clwwlkn0  26044  clwlkisclwwlklem2a1  26049  clwlkisclwwlklem2a2  26050  clwlkisclwwlklem2fv1  26052  clwlkisclwwlklem2fv2  26053  clwlkisclwwlklem2a4  26054  clwlkisclwwlklem2a  26055  clwlkisclwwlklem1  26057  clwlkisclwwlk2  26060  clwwlkext2edg  26072  usg2cwwkdifex  26091  clwlkfclwwlk  26113  konigsberg  26256  vdgfrgragt2  26296  extwwlkfablem2  26347  numclwwlkovf2ex  26355  frgrareggt1  26385  frgrareg  26386  frgraregord013  26387  ex-pss  26419  ex-res  26432  ex-fv  26434  ex-fl  26438  ex-mod  26440  ex-abs  26446  nvge0  26683  ipidsq  26729  minvecolem2  26897  minvecolem4  26902  minvecolem2OLD  26907  minvecolem4OLD  26912  normlem7  27149  norm-ii-i  27170  norm3lemt  27185  normpar2i  27189  bcsiALT  27212  pjhthlem1  27426  opsqrlem6  28180  cdj3lem1  28469  addltmulALT  28481  oppgle  28783  resvplusg  28964  sqsscirc1  29082  nexple  29199  dya2iocucvr  29473  omssubadd  29495  omssubaddOLD  29499  oddpwdc  29554  eulerpartlemgc  29562  fibp1  29601  coinfliplem  29678  coinflipspace  29680  ballotlem2  29688  signstfveq0  29829  subfacp1lem1  30264  subfacp1lem5  30269  subfacval3  30274  problem2  30660  problem2OLD  30661  problem5  30664  circum  30669  nn0prpwlem  31325  dnibndlem10  31485  knoppcnlem2  31492  knoppcnlem4  31494  knoppcnlem10  31500  unbdqndv2lem1  31508  knoppndvlem1  31511  knoppndvlem10  31520  knoppndvlem11  31521  knoppndvlem12  31522  knoppndvlem14  31524  knoppndvlem15  31525  knoppndvlem17  31527  knoppndvlem18  31528  knoppndvlem19  31529  knoppndvlem20  31530  knoppndvlem21  31531  cnndvlem1  31536  taupi  32181  relowlpssretop  32223  sin2h  32463  cos2h  32464  tan2h  32465  poimirlem7  32480  poimirlem9  32482  opnmbllem0  32509  mblfinlem1  32510  mblfinlem2  32511  itg2addnclem  32525  isbnd2  32646  isbnd3  32647  heiborlem7  32680  rabren3dioph  36291  pellexlem2  36306  pellexlem5  36309  pell14qrgapw  36352  pellfundex  36362  rmspecsqrtnq  36382  rmspecsqrtnqOLD  36383  jm2.24nn  36438  jm2.17a  36439  jm2.17b  36440  jm2.17c  36441  acongrep  36459  acongeq  36462  jm2.22  36474  jm2.23  36475  jm2.20nn  36476  jm3.1lem2  36497  expdiophlem1  36500  imo72b2lem0  37388  lhe4.4ex1a  37451  isosctrlem1ALT  38093  sineq0ALT  38096  lt3addmuld  38358  suplesup  38399  infleinflem2  38431  infleinf  38432  sumnnodd  38600  0ellimcdiv  38620  sinaover2ne0  38655  stoweidlem13  38813  stoweidlem14  38814  stoweidlem26  38826  stoweidlem49  38849  stoweidlem52  38852  wallispilem4  38868  wallispilem5  38869  wallispi  38870  wallispi2lem1  38871  wallispi2lem2  38872  wallispi2  38873  stirlinglem1  38874  stirlinglem3  38876  stirlinglem5  38878  stirlinglem6  38879  stirlinglem7  38880  stirlinglem10  38883  stirlinglem11  38884  stirlinglem15  38888  stirlingr  38890  dirker2re  38892  dirkerval2  38894  dirkerre  38895  dirkerper  38896  dirkertrigeqlem1  38898  dirkertrigeqlem3  38900  dirkercncflem1  38903  dirkercncflem2  38904  dirkercncflem4  38906  fourierdlem24  38931  fourierdlem43  38952  fourierdlem44  38953  fourierdlem57  38965  fourierdlem58  38966  fourierdlem62  38970  fourierdlem66  38974  fourierdlem68  38976  fourierdlem72  38980  fourierdlem76  38984  fourierdlem78  38986  fourierdlem79  38987  fourierdlem94  39002  fourierdlem103  39011  fourierdlem104  39012  fourierdlem111  39019  fourierdlem113  39021  sqwvfoura  39030  sqwvfourb  39031  fourierswlem  39032  fouriersw  39033  etransclem23  39060  salexct2  39144  salexct3  39147  salgencntex  39148  salgensscntex  39149  sge0ad2en  39235  ovnsubaddlem1  39371  smfmullem4  39590  smf2id  39597  fmtnoge3  39892  fmtnof1  39897  fmtnoprmfac2lem1  39928  fmtno4prmfac  39934  fmtno4prm  39937  2pwp1prm  39953  31prm  39962  sfprmdvdsmersenne  39970  lighneallem2  39973  lighneallem4a  39975  lighneallem4b  39976  dfodd4  40021  oexpnegALTV  40038  nn0o1gt2ALTV  40055  nnoALTV  40056  nn0oALTV  40057  nn0e  40058  perfectALTVlem1  40076  perfectALTVlem2  40077  gbogt5  40096  sgoldbalt  40115  nnsum3primes4  40116  nnsum3primesgbe  40120  nnsum3primesle9  40122  nnsum4primesodd  40124  nnsum4primesoddALTV  40125  wtgoldbnnsum4prm  40130  bgoldbnnsum3prm  40132  pfx2  40187  2leaddle2  40278  p1lep2  40280  xnn0n0n1ge2b  40325  upgrfi  40426  umgrupgr  40437  umgrislfupgrlem  40456  umgrislfupgr  40457  lfgrnloop  40459  upgredg  40479  usgruspgr  40517  usgrislfuspgr  40523  lfuhgr1v0e  40589  nbusgrvtxm1  40716  vdegp1bi-av  40862  upgrewlkle2  40917  lfgrwlkprop  41005  upgr2pthnlp  41047  usgr2pthlem  41078  pthdlem1  41081  wwlksm1edg  41187  wwlksnextwrd  41212  wwlksnextfun  41213  wwlksnextinj  41214  wwlksnextproplem3  41226  clwlkclwwlklem2a1  41310  clwlkclwwlklem2a2  41311  clwlkclwwlklem2fv1  41313  clwlkclwwlklem2fv2  41314  clwlkclwwlklem2a4  41315  clwlkclwwlklem2a  41316  clwlkclwwlklem2  41318  clwlkclwwlk2  41321  clwwlksext2edg  41339  clwlksfclwwlk  41378  konigsbergiedgw  41525  konigsbergiedgwOLD  41526  konigsbergssiedgw  41528  konigsberglem1  41531  konigsberglem2  41532  konigsberglem3  41533  konigsberg-av  41536  frgrwopreglem2  41591  av-extwwlkfablem2  41619  av-numclwwlkovf2ex  41626  av-frgrareggt1  41656  plusgndxnmulrndx  41852  cznnring  41857  nn0le2is012  42047  ply1mulgsumlem2  42078  zlmodzxznm  42189  zlmodzxzldeplem  42190  difmodm1lt  42220  nn0eo  42225  flnn0div2ge  42230  rege1logbzge0  42260  fldivexpfllog2  42266  logbpw2m1  42268  fllog2  42269  blenpw2m1  42280  nnpw2blen  42281  nnolog2flm1  42291  blennngt2o2  42293  dig2nn1st  42306  dig2nn0  42312  dig2bits  42315  dignn0flhalflem1  42316  dignn0flhalflem2  42317  dignn0flhalf  42319  nn0sumshdiglemA  42320
  Copyright terms: Public domain W3C validator