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

Theorem 2re 11706
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 11695 . 2 2 = (1 + 1)
2 1re 10635 . . 3 1 ∈ ℝ
32, 2readdcli 10650 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2912 1 2 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2115  (class class class)co 7146  cr 10530  1c1 10532   + caddc 10534  2c2 11687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-i2m1 10599  ax-1ne0 10600  ax-rrecex 10603  ax-cnre 10604
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-ne 3015  df-ral 3138  df-rex 3139  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4826  df-br 5054  df-iota 6303  df-fv 6352  df-ov 7149  df-2 11695
This theorem is referenced by:  2cnALT  11708  3re  11712  2ne0  11736  3pos  11737  2lt3  11804  1lt3  11805  2lt4  11807  1lt4  11808  2lt5  11811  2lt6  11816  1lt6  11817  2lt7  11822  1lt7  11823  2lt8  11829  1lt8  11830  2lt9  11837  1lt9  11838  1le2  11841  2rene0  11843  halfre  11846  halfgt0  11848  halflt1  11850  rehalfcl  11858  halfpos2  11861  halfnneg2  11863  addltmul  11868  nominpos  11869  avglt1  11870  avglt2  11871  div4p1lem1div2  11887  nn0lele2xi  11947  nn0n0n1ge2b  11958  nn0ge2m1nn  11959  nn0le2is012  12041  halfnz  12055  3halfnz  12056  2lt10  12231  1lt10  12232  eluz4eluz2  12280  uzuzle23  12284  uz3m2nn  12286  2rp  12389  xnn0n0n1ge2b  12521  fztpval  12971  fz0to4untppr  13012  fzo0to42pr  13126  flhalf  13202  fldiv4p1lem1div2  13207  2txmodxeq0  13301  expubnd  13544  expmulnbnd  13599  nn0opthlem2  13632  faclbnd2  13654  faclbnd4lem1  13656  faclbnd5  13661  4bc2eq6  13692  hashgt23el  13788  hashfun  13801  hashge2el2dif  13841  hashge2el2difr  13842  wrdlenge2n0  13902  f1oun2prg  14277  sqrlem7  14606  sqrt4  14630  sqrt2gt1lt2  14632  abstri  14688  sqreulem  14717  amgm2  14727  caucvgrlem  15027  climcndslem1  15202  climcndslem2  15203  climcnds  15204  efcllem  15429  ege2le3  15441  ef01bndlem  15535  cos01bnd  15537  cos2bnd  15539  cos01gt0  15542  sin02gt0  15543  sincos2sgn  15545  sin4lt0  15546  eirrlem  15555  egt2lt3  15557  epos  15558  ene1  15561  sqrt2re  15601  mod2eq1n2dvds  15694  oddge22np1  15696  evennn2n  15698  nn0o1gt2  15728  nno  15729  nn0o  15730  nnoddm1d2  15733  bitsp1o  15778  bitsfzolem  15779  bitsfzo  15780  bitsfi  15782  6gcd4e2  15882  2mulprm  16033  ge2nprmge4  16041  isprm7  16048  3lcm2e6  16068  prmreclem2  16249  prmreclem6  16253  4sqlem11  16287  4sqlem12  16288  prmgaplem7  16389  2expltfac  16424  plusgndxnmulrndx  16615  oppgtset  18478  efgredleme  18867  mgpsca  19244  mgptset  19245  mgpds  19247  rmodislmod  19697  cnfldfun  20552  zringndrg  20632  chfacfscmul0  21461  chfacfpmmul0  21465  psmetge0  22917  xmetge0  22949  bl2in  23005  metnrmlem3  23464  iihalf1  23534  iihalf2  23536  pcoass  23627  tcphcphlem1  23837  csbren  24001  trirn  24002  minveclem2  24028  minveclem4  24034  pjthlem1  24039  ovolunlem1a  24098  dyadss  24196  opnmbllem  24203  vitalilem2  24211  vitalilem4  24213  mbfi1fseqlem5  24321  lhop1lem  24614  aaliou3lem2  24937  aaliou3lem8  24939  pilem2  25045  pilem3  25046  pipos  25051  sinhalfpilem  25054  sincosq1lem  25088  sincosq4sgn  25092  tangtx  25096  sinq12gt0  25098  sincos4thpi  25104  tan4thpi  25105  sincos6thpi  25106  sineq0  25114  cos02pilt1  25116  cosq34lt1  25117  cosordlem  25120  cos0pilt1  25122  tanord1  25127  efif1olem1  25132  efif1olem2  25133  efif1olem4  25135  efif1o  25136  efifo  25137  2irrexpq  25319  cxpcn3lem  25334  root1id  25341  root1eq1  25342  root1cj  25343  cxpeq  25344  2logb9irr  25379  2logb3irr  25381  ang180lem1  25393  ang180lem2  25394  chordthmlem2  25417  1cubrlem  25425  atancj  25494  atantan  25507  atanbndlem  25509  atans2  25515  leibpi  25526  log2tlbnd  25529  log2ublem2  25531  log2ub  25533  divsqrtsumlem  25563  harmonicbnd3  25591  zetacvg  25598  lgamgulmlem2  25613  lgamgulmlem3  25614  lgamgulmlem4  25615  lgamgulmlem6  25617  lgamucov  25621  basellem1  25664  basellem2  25665  basellem3  25666  basellem5  25668  chtdif  25741  ppidif  25746  ppinncl  25757  chtrpcl  25758  ppieq0  25759  ppiltx  25760  ppiublem1  25784  ppiub  25786  chpeq0  25790  chteq0  25791  chtublem  25793  chtub  25794  chpval2  25800  chpub  25802  mersenne  25809  perfectlem1  25811  perfectlem2  25812  dchrptlem1  25846  dchrptlem2  25847  bcmono  25859  bclbnd  25862  bpos1lem  25864  bposlem1  25866  bposlem2  25867  bposlem3  25868  bposlem4  25869  bposlem5  25870  bposlem6  25871  bposlem7  25872  bposlem8  25873  bposlem9  25874  lgslem1  25879  lgsdirprm  25913  gausslemma2dlem0c  25940  gausslemma2dlem1a  25947  gausslemma2dlem2  25949  gausslemma2dlem3  25950  lgseisenlem1  25957  lgseisenlem2  25958  lgseisenlem3  25959  lgseisen  25961  lgsquadlem1  25962  lgsquadlem2  25963  m1lgs  25970  2lgslem1a1  25971  2lgslem1a2  25972  2lgslem1c  25975  2lgslem4  25988  2sqlem11  26011  2sq2  26015  2sqreultlem  26029  2sqreunnltlem  26032  chebbnd1lem1  26051  chebbnd1lem2  26052  chebbnd1lem3  26053  chebbnd1  26054  chtppilimlem1  26055  chtppilimlem2  26056  chtppilim  26057  chto1ub  26058  chebbnd2  26059  chto1lb  26060  chpchtlim  26061  chpo1ub  26062  chpo1ubb  26063  rplogsumlem1  26066  rplogsumlem2  26067  dchrisumlem2  26072  dchrisumlem3  26073  dchrvmasumiflem1  26083  dchrisum0fno1  26093  dchrisum0re  26095  dchrisum0lem1b  26097  dchrisum0lem1  26098  dchrisum0lem2  26100  rplogsum  26109  mulog2sumlem1  26116  mulog2sumlem2  26117  log2sumbnd  26126  selberglem2  26128  selbergb  26131  selberg2b  26134  chpdifbndlem1  26135  logdivbnd  26138  selberg3lem1  26139  selberg3  26141  selberg4lem1  26142  selberg4  26143  pntrmax  26146  pntrsumbnd2  26149  selberg3r  26151  selberg4r  26152  selberg34r  26153  pntrlog2bndlem2  26160  pntrlog2bndlem3  26161  pntrlog2bndlem4  26162  pntrlog2bndlem5  26163  pntrlog2bndlem6  26165  pntrlog2bnd  26166  pntpbnd1a  26167  pntpbnd1  26168  pntpbnd2  26169  pntpbnd  26170  pntibndlem2  26173  pntibndlem3  26174  pntibnd  26175  pntlemb  26179  pntlemg  26180  pntlemh  26181  pntlemr  26184  pntlemk  26188  pntlemo  26189  pnt2  26195  pnt  26196  ostth2lem1  26200  ostth3  26220  istrkg3ld  26253  tgldimor  26294  trgcgrg  26307  tgcgr4  26323  axlowdimlem6  26739  axlowdimlem16  26749  axlowdimlem17  26750  axlowdim  26753  upgrfi  26882  umgrupgr  26894  umgrislfupgrlem  26913  umgrislfupgr  26914  lfgrnloop  26916  usgruspgr  26969  usgrislfuspgr  26975  lfuhgr1v0e  27042  usgrexmpldifpr  27046  usgrexmplef  27047  nbusgrvtxm1  27167  vdegp1bi  27325  upgrewlkle2  27394  lfgrwlkprop  27475  upgr2pthnlp  27519  usgr2pthlem  27550  pthdlem1  27553  wwlksm1edg  27665  wwlksnextwrd  27681  wwlksnextfun  27682  wwlksnextinj  27683  wwlksnextproplem3  27695  clwlkclwwlklem2a1  27775  clwlkclwwlklem2a2  27776  clwlkclwwlklem2fv1  27778  clwlkclwwlklem2fv2  27779  clwlkclwwlklem2a4  27780  clwlkclwwlklem2a  27781  clwlkclwwlklem2  27783  clwlkclwwlk2  27786  clwlkclwwlkf  27791  clwwlkext2edg  27839  konigsbergiedgw  28031  konigsbergssiedgw  28033  konigsberglem1  28035  konigsberglem2  28036  konigsberglem3  28037  konigsberg  28040  frgrreggt1  28176  ex-pss  28211  ex-res  28224  ex-fv  28226  ex-fl  28230  ex-mod  28232  ex-abs  28238  ipidsq  28491  minvecolem2  28656  minvecolem4  28661  normlem7  28897  norm-ii-i  28918  norm3lemt  28933  normpar2i  28937  bcsiALT  28960  pjhthlem1  29172  opsqrlem6  29926  cdj3lem1  30215  addltmulALT  30227  threehalves  30597  pfx1s2  30621  wrdt2ind  30633  oppgle  30646  cyc3conja  30826  resvplusg  30933  sqsscirc1  31178  nexple  31295  dya2iocucvr  31569  omssubadd  31585  oddpwdc  31639  eulerpartlemgc  31647  fibp1  31686  coinfliplem  31763  coinflipspace  31765  ballotlem2  31773  signstfveq0  31874  prodfzo03  31901  hgt750lemd  31946  logdivsqrle  31948  hgt750lem  31949  hgt750lem2  31950  hgt750leme  31956  lfuhgr2  32392  usgrcyclgt2v  32405  acycgr2v  32424  subfacp1lem1  32453  subfacp1lem5  32458  subfacval3  32463  problem2  32936  problem5  32939  circum  32944  nn0prpwlem  33697  dnibndlem10  33853  knoppcnlem2  33860  knoppcnlem4  33862  knoppcnlem10  33868  unbdqndv2lem1  33875  knoppndvlem1  33878  knoppndvlem10  33887  knoppndvlem11  33888  knoppndvlem12  33889  knoppndvlem14  33891  knoppndvlem15  33892  knoppndvlem17  33894  knoppndvlem18  33895  knoppndvlem19  33896  knoppndvlem20  33897  knoppndvlem21  33898  cnndvlem1  33903  taupi  34652  relowlpssretop  34695  sin2h  34959  cos2h  34960  tan2h  34961  poimirlem7  34976  poimirlem9  34978  opnmbllem0  35005  mblfinlem1  35006  mblfinlem2  35007  itg2addnclem  35020  isbnd2  35133  isbnd3  35134  heiborlem7  35167  12gcd5e1  39199  lcm2un  39210  lcmineqlem19  39243  lcmineqlem20  39244  lcmineqlem22  39246  3lexlogpow5ineq1  39249  3lexlogpow5ineq2  39250  3lexlogpow5ineq3  39251  2xp3dxp2ge1d  39270  oexpreposd  39361  remul02  39417  sn-0ne2  39418  remul01  39419  rabren3dioph  39612  pellexlem2  39627  pellexlem5  39630  pell14qrgapw  39673  pellfundex  39683  rmspecsqrtnq  39703  jm2.24nn  39756  jm2.17a  39757  jm2.17b  39758  jm2.17c  39759  acongrep  39777  acongeq  39780  jm2.22  39792  jm2.23  39793  jm2.20nn  39794  jm3.1lem2  39815  expdiophlem1  39818  sqrtcval  40197  imo72b2lem0  40728  mnringaddgd  40788  lhe4.4ex1a  40893  isosctrlem1ALT  41500  sineq0ALT  41503  lt3addmuld  41799  suplesup  41837  infleinflem2  41869  infleinf  41870  sumnnodd  42138  0ellimcdiv  42157  sinaover2ne0  42376  stoweidlem13  42521  stoweidlem14  42522  stoweidlem26  42534  stoweidlem49  42557  stoweidlem52  42560  wallispilem4  42576  wallispilem5  42577  wallispi  42578  wallispi2lem1  42579  wallispi2lem2  42580  wallispi2  42581  stirlinglem1  42582  stirlinglem3  42584  stirlinglem5  42586  stirlinglem6  42587  stirlinglem7  42588  stirlinglem10  42591  stirlinglem11  42592  stirlinglem15  42596  stirlingr  42598  dirker2re  42600  dirkerval2  42602  dirkerre  42603  dirkerper  42604  dirkertrigeqlem1  42606  dirkertrigeqlem3  42608  dirkercncflem1  42611  dirkercncflem2  42612  dirkercncflem4  42614  fourierdlem24  42639  fourierdlem43  42658  fourierdlem44  42659  fourierdlem57  42671  fourierdlem58  42672  fourierdlem62  42676  fourierdlem66  42680  fourierdlem68  42682  fourierdlem72  42686  fourierdlem76  42690  fourierdlem78  42692  fourierdlem79  42693  fourierdlem94  42708  fourierdlem103  42717  fourierdlem104  42718  fourierdlem111  42725  fourierdlem113  42727  sqwvfoura  42736  sqwvfourb  42737  fourierswlem  42738  fouriersw  42739  etransclem23  42765  salexct2  42845  salexct3  42848  salgencntex  42849  salgensscntex  42850  sge0ad2en  42936  ovnsubaddlem1  43075  smfmullem4  43292  smf2id  43299  2leaddle2  43721  p1lep2  43723  fmtnoge3  43913  fmtnof1  43918  fmtnoprmfac2lem1  43949  fmtno4prmfac  43955  fmtno4prm  43958  2pwp1prm  43972  31prm  43980  sfprmdvdsmersenne  43987  lighneallem2  43990  lighneallem4a  43992  lighneallem4b  43993  requad01  44005  requad1  44006  requad2  44007  dfodd4  44043  nn0o1gt2ALTV  44078  nnoALTV  44079  nn0oALTV  44080  nn0e  44081  nneven  44082  perfectALTVlem1  44105  perfectALTVlem2  44106  341fppr2  44118  9fppr8  44121  fpprel2  44125  nfermltl2rev  44127  gbowgt5  44146  sbgoldbalt  44165  sgoldbeven3prm  44167  mogoldbb  44169  nnsum3primes4  44172  nnsum3primesgbe  44176  nnsum3primesle9  44178  nnsum4primesodd  44180  nnsum4primesoddALTV  44181  wtgoldbnnsum4prm  44186  bgoldbnnsum3prm  44188  cznnring  44446  ply1mulgsumlem2  44660  zlmodzxznm  44771  zlmodzxzldeplem  44772  difmodm1lt  44801  nn0eo  44807  flnn0div2ge  44812  rege1logbzge0  44838  fldivexpfllog2  44844  logbpw2m1  44846  fllog2  44847  blenpw2m1  44858  nnpw2blen  44859  nnolog2flm1  44869  blennngt2o2  44871  dig2nn1st  44884  dig2nn0  44890  dig2bits  44893  dignn0flhalflem1  44894  dignn0flhalflem2  44895  dignn0flhalf  44897  nn0sumshdiglemA  44898  ackval42  44964  rrx2xpref1o  44986  itscnhlc0yqe  45027  itsclquadb  45044  2itscp  45049  itscnhlinecirc02p  45053
  Copyright terms: Public domain W3C validator