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

Theorem 2re 12093
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 12082 . 2 2 = (1 + 1)
2 1re 11021 . . 3 1 ∈ ℝ
32, 2readdcli 11036 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2833 1 2 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2104  (class class class)co 7307  cr 10916  1c1 10918   + caddc 10920  2c2 12074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-1cn 10975  ax-icn 10976  ax-addcl 10977  ax-addrcl 10978  ax-mulcl 10979  ax-mulrcl 10980  ax-i2m1 10985  ax-1ne0 10986  ax-rrecex 10989  ax-cnre 10990
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-ov 7310  df-2 12082
This theorem is referenced by:  2cnALT  12095  3re  12099  2ne0  12123  3pos  12124  2lt3  12191  1lt3  12192  2lt4  12194  1lt4  12195  2lt5  12198  2lt6  12203  1lt6  12204  2lt7  12209  1lt7  12210  2lt8  12216  1lt8  12217  2lt9  12224  1lt9  12225  1le2  12228  2rene0  12230  halfre  12233  halfgt0  12235  halflt1  12237  rehalfcl  12245  halfpos2  12248  halfnneg2  12250  addltmul  12255  nominpos  12256  avglt1  12257  avglt2  12258  div4p1lem1div2  12274  nn0lele2xi  12334  nn0n0n1ge2b  12347  nn0ge2m1nn  12348  nn0le2is012  12430  halfnz  12444  3halfnz  12445  2lt10  12621  1lt10  12622  eluz4eluz2  12671  uzuzle23  12675  uz3m2nn  12677  2rp  12781  xnn0n0n1ge2b  12913  fztpval  13364  fz0to4untppr  13405  fzo0to42pr  13520  flhalf  13596  fldiv4p1lem1div2  13601  2txmodxeq0  13697  expubnd  13941  expmulnbnd  13996  nn0opthlem2  14029  faclbnd2  14051  faclbnd4lem1  14053  faclbnd5  14058  4bc2eq6  14089  hashgt23el  14184  hashfun  14197  hashge2el2dif  14239  hashge2el2difr  14240  wrdlenge2n0  14300  f1oun2prg  14675  sqrlem7  15005  sqrt4  15029  sqrt2gt1lt2  15031  abstri  15087  sqreulem  15116  amgm2  15126  caucvgrlem  15429  climcndslem1  15606  climcndslem2  15607  climcnds  15608  efcllem  15832  ege2le3  15844  ef01bndlem  15938  cos01bnd  15940  cos2bnd  15942  cos01gt0  15945  sin02gt0  15946  sincos2sgn  15948  sin4lt0  15949  eirrlem  15958  egt2lt3  15960  epos  15961  ene1  15964  sqrt2re  16004  mod2eq1n2dvds  16101  oddge22np1  16103  evennn2n  16105  nn0o1gt2  16135  nno  16136  nn0o  16137  nnoddm1d2  16140  bitsp1o  16185  bitsfzolem  16186  bitsfzo  16187  bitsfi  16189  6gcd4e2  16291  2mulprm  16443  ge2nprmge4  16451  isprm7  16458  3lcm2e6  16481  prmreclem2  16663  prmreclem6  16667  4sqlem11  16701  4sqlem12  16702  prmgaplem7  16803  2expltfac  16839  plusgndxnmulrndx  17052  starvndxnplusgndx  17060  scandxnplusgndx  17072  vscandxnplusgndx  17077  ipndxnplusgndx  17088  tsetndxnplusgndx  17112  plendxnplusgndx  17126  dsndxnplusgndx  17145  slotsdifunifndx  17156  oppgtsetOLD  19004  efgredleme  19394  mgpscaOLD  19774  mgptsetOLD  19776  mgpdsOLD  19779  rmodislmodOLD  20237  cnfldfunALTOLD  20656  zringndrg  20735  chfacfscmul0  22052  chfacfpmmul0  22056  psmetge0  23510  xmetge0  23542  bl2in  23598  metnrmlem3  24069  iihalf1  24139  iihalf2  24141  pcoass  24232  tcphcphlem1  24444  csbren  24608  trirn  24609  minveclem2  24635  minveclem4  24641  pjthlem1  24646  ovolunlem1a  24705  dyadss  24803  opnmbllem  24810  vitalilem2  24818  vitalilem4  24820  mbfi1fseqlem5  24929  lhop1lem  25222  aaliou3lem2  25548  aaliou3lem8  25550  pilem2  25656  pilem3  25657  pipos  25662  sinhalfpilem  25665  sincosq1lem  25699  sincosq4sgn  25703  tangtx  25707  sinq12gt0  25709  sincos4thpi  25715  tan4thpi  25716  sincos6thpi  25717  sineq0  25725  cos02pilt1  25727  cosq34lt1  25728  cosordlem  25731  cos0pilt1  25733  tanord1  25738  efif1olem1  25743  efif1olem2  25744  efif1olem4  25746  efif1o  25747  efifo  25748  2irrexpq  25930  cxpcn3lem  25945  root1id  25952  root1eq1  25953  root1cj  25954  cxpeq  25955  2logb9irr  25990  2logb3irr  25992  ang180lem1  26004  ang180lem2  26005  chordthmlem2  26028  1cubrlem  26036  atancj  26105  atantan  26118  atanbndlem  26120  atans2  26126  leibpi  26137  log2tlbnd  26140  log2ublem2  26142  log2ub  26144  divsqrtsumlem  26174  harmonicbnd3  26202  zetacvg  26209  lgamgulmlem2  26224  lgamgulmlem3  26225  lgamgulmlem4  26226  lgamgulmlem6  26228  lgamucov  26232  basellem1  26275  basellem2  26276  basellem3  26277  basellem5  26279  chtdif  26352  ppidif  26357  ppinncl  26368  chtrpcl  26369  ppieq0  26370  ppiltx  26371  ppiublem1  26395  ppiub  26397  chpeq0  26401  chteq0  26402  chtublem  26404  chtub  26405  chpval2  26411  chpub  26413  mersenne  26420  perfectlem1  26422  perfectlem2  26423  dchrptlem1  26457  dchrptlem2  26458  bcmono  26470  bclbnd  26473  bpos1lem  26475  bposlem1  26477  bposlem2  26478  bposlem3  26479  bposlem4  26480  bposlem5  26481  bposlem6  26482  bposlem7  26483  bposlem8  26484  bposlem9  26485  lgslem1  26490  lgsdirprm  26524  gausslemma2dlem0c  26551  gausslemma2dlem1a  26558  gausslemma2dlem2  26560  gausslemma2dlem3  26561  lgseisenlem1  26568  lgseisenlem2  26569  lgseisenlem3  26570  lgseisen  26572  lgsquadlem1  26573  lgsquadlem2  26574  m1lgs  26581  2lgslem1a1  26582  2lgslem1a2  26583  2lgslem1c  26586  2lgslem4  26599  2sqlem11  26622  2sq2  26626  2sqreultlem  26640  2sqreunnltlem  26643  chebbnd1lem1  26662  chebbnd1lem2  26663  chebbnd1lem3  26664  chebbnd1  26665  chtppilimlem1  26666  chtppilimlem2  26667  chtppilim  26668  chto1ub  26669  chebbnd2  26670  chto1lb  26671  chpchtlim  26672  chpo1ub  26673  chpo1ubb  26674  rplogsumlem1  26677  rplogsumlem2  26678  dchrisumlem2  26683  dchrisumlem3  26684  dchrvmasumiflem1  26694  dchrisum0fno1  26704  dchrisum0re  26706  dchrisum0lem1b  26708  dchrisum0lem1  26709  dchrisum0lem2  26711  rplogsum  26720  mulog2sumlem1  26727  mulog2sumlem2  26728  log2sumbnd  26737  selberglem2  26739  selbergb  26742  selberg2b  26745  chpdifbndlem1  26746  logdivbnd  26749  selberg3lem1  26750  selberg3  26752  selberg4lem1  26753  selberg4  26754  pntrmax  26757  pntrsumbnd2  26760  selberg3r  26762  selberg4r  26763  selberg34r  26764  pntrlog2bndlem2  26771  pntrlog2bndlem3  26772  pntrlog2bndlem4  26773  pntrlog2bndlem5  26774  pntrlog2bndlem6  26776  pntrlog2bnd  26777  pntpbnd1a  26778  pntpbnd1  26779  pntpbnd2  26780  pntpbnd  26781  pntibndlem2  26784  pntibndlem3  26785  pntibnd  26786  pntlemb  26790  pntlemg  26791  pntlemh  26792  pntlemr  26795  pntlemk  26799  pntlemo  26800  pnt2  26806  pnt  26807  ostth2lem1  26811  ostth3  26831  slotsinbpsd  26847  slotslnbpsd  26848  istrkg3ld  26867  tgldimor  26908  trgcgrg  26921  tgcgr4  26937  axlowdimlem6  27360  axlowdimlem16  27370  axlowdimlem17  27371  axlowdim  27374  upgrfi  27506  umgrupgr  27518  umgrislfupgrlem  27537  umgrislfupgr  27538  lfgrnloop  27540  usgruspgr  27593  usgrislfuspgr  27599  lfuhgr1v0e  27666  usgrexmpldifpr  27670  usgrexmplef  27671  nbusgrvtxm1  27791  vdegp1bi  27949  upgrewlkle2  28018  lfgrwlkprop  28100  upgr2pthnlp  28145  usgr2pthlem  28176  pthdlem1  28179  wwlksm1edg  28291  wwlksnextwrd  28307  wwlksnextfun  28308  wwlksnextinj  28309  wwlksnextproplem3  28321  clwlkclwwlklem2a1  28401  clwlkclwwlklem2a2  28402  clwlkclwwlklem2fv1  28404  clwlkclwwlklem2fv2  28405  clwlkclwwlklem2a4  28406  clwlkclwwlklem2a  28407  clwlkclwwlklem2  28409  clwlkclwwlk2  28412  clwlkclwwlkf  28417  clwwlkext2edg  28465  konigsbergiedgw  28657  konigsbergssiedgw  28659  konigsberglem1  28661  konigsberglem2  28662  konigsberglem3  28663  konigsberg  28666  frgrreggt1  28802  ex-pss  28837  ex-res  28850  ex-fv  28852  ex-fl  28856  ex-mod  28858  ex-abs  28864  ipidsq  29117  minvecolem2  29282  minvecolem4  29287  normlem7  29523  norm-ii-i  29544  norm3lemt  29559  normpar2i  29563  bcsiALT  29586  pjhthlem1  29798  opsqrlem6  30552  cdj3lem1  30841  addltmulALT  30853  threehalves  31234  pfx1s2  31258  wrdt2ind  31270  oppgleOLD  31284  cyc3conja  31469  resvplusgOLD  31580  sqsscirc1  31903  nexple  32022  dya2iocucvr  32296  omssubadd  32312  oddpwdc  32366  eulerpartlemgc  32374  fibp1  32413  coinfliplem  32490  coinflipspace  32492  ballotlem2  32500  signstfveq0  32601  prodfzo03  32628  hgt750lemd  32673  logdivsqrle  32675  hgt750lem  32676  hgt750lem2  32677  hgt750leme  32683  lfuhgr2  33125  usgrcyclgt2v  33138  acycgr2v  33157  subfacp1lem1  33186  subfacp1lem5  33191  subfacval3  33196  problem2  33669  problem5  33672  circum  33677  nn0prpwlem  34556  dnibndlem10  34712  knoppcnlem2  34719  knoppcnlem4  34721  knoppcnlem10  34727  unbdqndv2lem1  34734  knoppndvlem1  34737  knoppndvlem10  34746  knoppndvlem11  34747  knoppndvlem12  34748  knoppndvlem14  34750  knoppndvlem15  34751  knoppndvlem17  34753  knoppndvlem18  34754  knoppndvlem19  34755  knoppndvlem20  34756  knoppndvlem21  34757  cnndvlem1  34762  taupi  35538  iccioo01  35542  relowlpssretop  35579  sin2h  35811  cos2h  35812  tan2h  35813  poimirlem7  35828  poimirlem9  35830  opnmbllem0  35857  mblfinlem1  35858  mblfinlem2  35859  itg2addnclem  35872  isbnd2  35985  isbnd3  35986  heiborlem7  36019  12gcd5e1  40053  lcm2un  40064  lcmineqlem19  40097  lcmineqlem20  40098  lcmineqlem22  40100  3lexlogpow5ineq2  40105  3lexlogpow5ineq4  40106  3lexlogpow5ineq3  40107  3lexlogpow2ineq1  40108  3lexlogpow2ineq2  40109  3lexlogpow5ineq5  40110  aks4d1lem1  40112  aks4d1p1p3  40119  aks4d1p1p2  40120  aks4d1p1p4  40121  aks4d1p1p6  40123  aks4d1p1p7  40124  aks4d1p1p5  40125  aks4d1p1  40126  aks4d1p2  40127  aks4d1p3  40128  aks4d1p5  40130  aks4d1p6  40131  aks4d1p7d1  40132  aks4d1p7  40133  aks4d1p8  40137  aks4d1p9  40138  2np3bcnp1  40142  2ap1caineq  40143  2xp3dxp2ge1d  40204  oexpreposd  40358  remul02  40425  sn-0ne2  40426  remul01  40427  flt4lem7  40533  rabren3dioph  40674  pellexlem2  40689  pellexlem5  40692  pell14qrgapw  40735  pellfundex  40745  rmspecsqrtnq  40765  jm2.24nn  40819  jm2.17a  40820  jm2.17b  40821  jm2.17c  40822  acongrep  40840  acongeq  40843  jm2.22  40855  jm2.23  40856  jm2.20nn  40857  jm3.1lem2  40878  expdiophlem1  40881  sqrtcval  41287  imo72b2lem0  41814  mnringaddgdOLD  41874  lhe4.4ex1a  41985  isosctrlem1ALT  42592  sineq0ALT  42595  lt3addmuld  42888  suplesup  42926  infleinflem2  42958  infleinf  42959  sumnnodd  43220  0ellimcdiv  43239  sinaover2ne0  43458  stoweidlem13  43603  stoweidlem14  43604  stoweidlem26  43616  stoweidlem49  43639  stoweidlem52  43642  wallispilem4  43658  wallispilem5  43659  wallispi  43660  wallispi2lem1  43661  wallispi2lem2  43662  wallispi2  43663  stirlinglem1  43664  stirlinglem3  43666  stirlinglem5  43668  stirlinglem6  43669  stirlinglem7  43670  stirlinglem10  43673  stirlinglem11  43674  stirlinglem15  43678  stirlingr  43680  dirker2re  43682  dirkerval2  43684  dirkerre  43685  dirkerper  43686  dirkertrigeqlem1  43688  dirkertrigeqlem3  43690  dirkercncflem1  43693  dirkercncflem2  43694  dirkercncflem4  43696  fourierdlem24  43721  fourierdlem43  43740  fourierdlem44  43741  fourierdlem57  43753  fourierdlem58  43754  fourierdlem62  43758  fourierdlem66  43762  fourierdlem68  43764  fourierdlem72  43768  fourierdlem76  43772  fourierdlem78  43774  fourierdlem79  43775  fourierdlem94  43790  fourierdlem103  43799  fourierdlem104  43800  fourierdlem111  43807  fourierdlem113  43809  sqwvfoura  43818  sqwvfourb  43819  fourierswlem  43820  fouriersw  43821  etransclem23  43847  salexct2  43927  salexct3  43930  salgencntex  43931  salgensscntex  43932  sge0ad2en  44019  ovnsubaddlem1  44158  smfmullem4  44382  smf2id  44389  2leaddle2  44848  p1lep2  44850  fmtnoge3  45040  fmtnof1  45045  fmtnoprmfac2lem1  45076  fmtno4prmfac  45082  fmtno4prm  45085  2pwp1prm  45099  31prm  45107  sfprmdvdsmersenne  45113  lighneallem2  45116  lighneallem4a  45118  lighneallem4b  45119  requad01  45131  requad1  45132  requad2  45133  dfodd4  45169  nn0o1gt2ALTV  45204  nnoALTV  45205  nn0oALTV  45206  nn0e  45207  nneven  45208  perfectALTVlem1  45231  perfectALTVlem2  45232  341fppr2  45244  9fppr8  45247  fpprel2  45251  nfermltl2rev  45253  gbowgt5  45272  sbgoldbalt  45291  sgoldbeven3prm  45293  mogoldbb  45295  nnsum3primes4  45298  nnsum3primesgbe  45302  nnsum3primesle9  45304  nnsum4primesodd  45306  nnsum4primesoddALTV  45307  wtgoldbnnsum4prm  45312  bgoldbnnsum3prm  45314  cznnring  45572  ply1mulgsumlem2  45786  zlmodzxznm  45896  zlmodzxzldeplem  45897  difmodm1lt  45926  nn0eo  45932  flnn0div2ge  45937  rege1logbzge0  45963  fldivexpfllog2  45969  logbpw2m1  45971  fllog2  45972  blenpw2m1  45983  nnpw2blen  45984  nnolog2flm1  45994  blennngt2o2  45996  dig2nn1st  46009  dig2nn0  46015  dig2bits  46018  dignn0flhalflem1  46019  dignn0flhalflem2  46020  dignn0flhalf  46022  nn0sumshdiglemA  46023  ackval42  46100  rrx2xpref1o  46122  itscnhlc0yqe  46163  itsclquadb  46180  2itscp  46185  itscnhlinecirc02p  46189  sepfsepc  46279
  Copyright terms: Public domain W3C validator