Theorem 2re 12030

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	⊢ 2 ∈ ℝ

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 12019	. 2 ⊢ 2 = (1 + 1)
2		1re 10959	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 10974	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2836	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7268  ℝcr 10854  1c1 10856   + caddc 10858  2c2 12011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-i2m1 10923  ax-1ne0 10924  ax-rrecex 10927  ax-cnre 10928

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271  df-2 12019

This theorem is referenced by:  2cnALT  12032  3re  12036  2ne0  12060  3pos  12061  2lt3  12128  1lt3  12129  2lt4  12131  1lt4  12132  2lt5  12135  2lt6  12140  1lt6  12141  2lt7  12146  1lt7  12147  2lt8  12153  1lt8  12154  2lt9  12161  1lt9  12162  1le2  12165  2rene0  12167  halfre  12170  halfgt0  12172  halflt1  12174  rehalfcl  12182  halfpos2  12185  halfnneg2  12187  addltmul  12192  nominpos  12193  avglt1  12194  avglt2  12195  div4p1lem1div2  12211  nn0lele2xi  12271  nn0n0n1ge2b  12284  nn0ge2m1nn  12285  nn0le2is012  12367  halfnz  12381  3halfnz  12382  2lt10  12557  1lt10  12558  eluz4eluz2  12607  uzuzle23  12611  uz3m2nn  12613  2rp  12717  xnn0n0n1ge2b  12849  fztpval  13300  fz0to4untppr  13341  fzo0to42pr  13455  flhalf  13531  fldiv4p1lem1div2  13536  2txmodxeq0  13632  expubnd  13876  expmulnbnd  13931  nn0opthlem2  13964  faclbnd2  13986  faclbnd4lem1  13988  faclbnd5  13993  4bc2eq6  14024  hashgt23el  14120  hashfun  14133  hashge2el2dif  14175  hashge2el2difr  14176  wrdlenge2n0  14236  f1oun2prg  14611  sqrlem7  14941  sqrt4  14965  sqrt2gt1lt2  14967  abstri  15023  sqreulem  15052  amgm2  15062  caucvgrlem  15365  climcndslem1  15542  climcndslem2  15543  climcnds  15544  efcllem  15768  ege2le3  15780  ef01bndlem  15874  cos01bnd  15876  cos2bnd  15878  cos01gt0  15881  sin02gt0  15882  sincos2sgn  15884  sin4lt0  15885  eirrlem  15894  egt2lt3  15896  epos  15897  ene1  15900  sqrt2re  15940  mod2eq1n2dvds  16037  oddge22np1  16039  evennn2n  16041  nn0o1gt2  16071  nno  16072  nn0o  16073  nnoddm1d2  16076  bitsp1o  16121  bitsfzolem  16122  bitsfzo  16123  bitsfi  16125  6gcd4e2  16227  2mulprm  16379  ge2nprmge4  16387  isprm7  16394  3lcm2e6  16417  prmreclem2  16599  prmreclem6  16603  4sqlem11  16637  4sqlem12  16638  prmgaplem7  16739  2expltfac  16775  plusgndxnmulrndx  16988  starvndxnplusgndx  16996  scandxnplusgndx  17008  vscandxnplusgndx  17013  ipndxnplusgndx  17024  tsetndxnplusgndx  17048  plendxnplusgndx  17062  dsndxnplusgndx  17081  slotsdifunifndx  17092  oppgtsetOLD  18940  efgredleme  19330  mgpscaOLD  19710  mgptsetOLD  19712  mgpdsOLD  19715  rmodislmodOLD  20173  cnfldfunOLD  20591  zringndrg  20671  chfacfscmul0  21988  chfacfpmmul0  21992  psmetge0  23446  xmetge0  23478  bl2in  23534  metnrmlem3  24005  iihalf1  24075  iihalf2  24077  pcoass  24168  tcphcphlem1  24380  csbren  24544  trirn  24545  minveclem2  24571  minveclem4  24577  pjthlem1  24582  ovolunlem1a  24641  dyadss  24739  opnmbllem  24746  vitalilem2  24754  vitalilem4  24756  mbfi1fseqlem5  24865  lhop1lem  25158  aaliou3lem2  25484  aaliou3lem8  25486  pilem2  25592  pilem3  25593  pipos  25598  sinhalfpilem  25601  sincosq1lem  25635  sincosq4sgn  25639  tangtx  25643  sinq12gt0  25645  sincos4thpi  25651  tan4thpi  25652  sincos6thpi  25653  sineq0  25661  cos02pilt1  25663  cosq34lt1  25664  cosordlem  25667  cos0pilt1  25669  tanord1  25674  efif1olem1  25679  efif1olem2  25680  efif1olem4  25682  efif1o  25683  efifo  25684  2irrexpq  25866  cxpcn3lem  25881  root1id  25888  root1eq1  25889  root1cj  25890  cxpeq  25891  2logb9irr  25926  2logb3irr  25928  ang180lem1  25940  ang180lem2  25941  chordthmlem2  25964  1cubrlem  25972  atancj  26041  atantan  26054  atanbndlem  26056  atans2  26062  leibpi  26073  log2tlbnd  26076  log2ublem2  26078  log2ub  26080  divsqrtsumlem  26110  harmonicbnd3  26138  zetacvg  26145  lgamgulmlem2  26160  lgamgulmlem3  26161  lgamgulmlem4  26162  lgamgulmlem6  26164  lgamucov  26168  basellem1  26211  basellem2  26212  basellem3  26213  basellem5  26215  chtdif  26288  ppidif  26293  ppinncl  26304  chtrpcl  26305  ppieq0  26306  ppiltx  26307  ppiublem1  26331  ppiub  26333  chpeq0  26337  chteq0  26338  chtublem  26340  chtub  26341  chpval2  26347  chpub  26349  mersenne  26356  perfectlem1  26358  perfectlem2  26359  dchrptlem1  26393  dchrptlem2  26394  bcmono  26406  bclbnd  26409  bpos1lem  26411  bposlem1  26413  bposlem2  26414  bposlem3  26415  bposlem4  26416  bposlem5  26417  bposlem6  26418  bposlem7  26419  bposlem8  26420  bposlem9  26421  lgslem1  26426  lgsdirprm  26460  gausslemma2dlem0c  26487  gausslemma2dlem1a  26494  gausslemma2dlem2  26496  gausslemma2dlem3  26497  lgseisenlem1  26504  lgseisenlem2  26505  lgseisenlem3  26506  lgseisen  26508  lgsquadlem1  26509  lgsquadlem2  26510  m1lgs  26517  2lgslem1a1  26518  2lgslem1a2  26519  2lgslem1c  26522  2lgslem4  26535  2sqlem11  26558  2sq2  26562  2sqreultlem  26576  2sqreunnltlem  26579  chebbnd1lem1  26598  chebbnd1lem2  26599  chebbnd1lem3  26600  chebbnd1  26601  chtppilimlem1  26602  chtppilimlem2  26603  chtppilim  26604  chto1ub  26605  chebbnd2  26606  chto1lb  26607  chpchtlim  26608  chpo1ub  26609  chpo1ubb  26610  rplogsumlem1  26613  rplogsumlem2  26614  dchrisumlem2  26619  dchrisumlem3  26620  dchrvmasumiflem1  26630  dchrisum0fno1  26640  dchrisum0re  26642  dchrisum0lem1b  26644  dchrisum0lem1  26645  dchrisum0lem2  26647  rplogsum  26656  mulog2sumlem1  26663  mulog2sumlem2  26664  log2sumbnd  26673  selberglem2  26675  selbergb  26678  selberg2b  26681  chpdifbndlem1  26682  logdivbnd  26685  selberg3lem1  26686  selberg3  26688  selberg4lem1  26689  selberg4  26690  pntrmax  26693  pntrsumbnd2  26696  selberg3r  26698  selberg4r  26699  selberg34r  26700  pntrlog2bndlem2  26707  pntrlog2bndlem3  26708  pntrlog2bndlem4  26709  pntrlog2bndlem5  26710  pntrlog2bndlem6  26712  pntrlog2bnd  26713  pntpbnd1a  26714  pntpbnd1  26715  pntpbnd2  26716  pntpbnd  26717  pntibndlem2  26720  pntibndlem3  26721  pntibnd  26722  pntlemb  26726  pntlemg  26727  pntlemh  26728  pntlemr  26731  pntlemk  26735  pntlemo  26736  pnt2  26742  pnt  26743  ostth2lem1  26747  ostth3  26767  slotsinbpsd  26783  slotslnbpsd  26784  istrkg3ld  26803  tgldimor  26844  trgcgrg  26857  tgcgr4  26873  axlowdimlem6  27296  axlowdimlem16  27306  axlowdimlem17  27307  axlowdim  27310  upgrfi  27442  umgrupgr  27454  umgrislfupgrlem  27473  umgrislfupgr  27474  lfgrnloop  27476  usgruspgr  27529  usgrislfuspgr  27535  lfuhgr1v0e  27602  usgrexmpldifpr  27606  usgrexmplef  27607  nbusgrvtxm1  27727  vdegp1bi  27885  upgrewlkle2  27954  lfgrwlkprop  28035  upgr2pthnlp  28079  usgr2pthlem  28110  pthdlem1  28113  wwlksm1edg  28225  wwlksnextwrd  28241  wwlksnextfun  28242  wwlksnextinj  28243  wwlksnextproplem3  28255  clwlkclwwlklem2a1  28335  clwlkclwwlklem2a2  28336  clwlkclwwlklem2fv1  28338  clwlkclwwlklem2fv2  28339  clwlkclwwlklem2a4  28340  clwlkclwwlklem2a  28341  clwlkclwwlklem2  28343  clwlkclwwlk2  28346  clwlkclwwlkf  28351  clwwlkext2edg  28399  konigsbergiedgw  28591  konigsbergssiedgw  28593  konigsberglem1  28595  konigsberglem2  28596  konigsberglem3  28597  konigsberg  28600  frgrreggt1  28736  ex-pss  28771  ex-res  28784  ex-fv  28786  ex-fl  28790  ex-mod  28792  ex-abs  28798  ipidsq  29051  minvecolem2  29216  minvecolem4  29221  normlem7  29457  norm-ii-i  29478  norm3lemt  29493  normpar2i  29497  bcsiALT  29520  pjhthlem1  29732  opsqrlem6  30486  cdj3lem1  30775  addltmulALT  30787  threehalves  31168  pfx1s2  31192  wrdt2ind  31204  oppgleOLD  31218  cyc3conja  31403  resvplusgOLD  31514  sqsscirc1  31837  nexple  31956  dya2iocucvr  32230  omssubadd  32246  oddpwdc  32300  eulerpartlemgc  32308  fibp1  32347  coinfliplem  32424  coinflipspace  32426  ballotlem2  32434  signstfveq0  32535  prodfzo03  32562  hgt750lemd  32607  logdivsqrle  32609  hgt750lem  32610  hgt750lem2  32611  hgt750leme  32617  lfuhgr2  33059  usgrcyclgt2v  33072  acycgr2v  33091  subfacp1lem1  33120  subfacp1lem5  33125  subfacval3  33130  problem2  33603  problem5  33606  circum  33611  nn0prpwlem  34490  dnibndlem10  34646  knoppcnlem2  34653  knoppcnlem4  34655  knoppcnlem10  34661  unbdqndv2lem1  34668  knoppndvlem1  34671  knoppndvlem10  34680  knoppndvlem11  34681  knoppndvlem12  34682  knoppndvlem14  34684  knoppndvlem15  34685  knoppndvlem17  34687  knoppndvlem18  34688  knoppndvlem19  34689  knoppndvlem20  34690  knoppndvlem21  34691  cnndvlem1  34696  taupi  35473  iccioo01  35477  relowlpssretop  35514  sin2h  35746  cos2h  35747  tan2h  35748  poimirlem7  35763  poimirlem9  35765  opnmbllem0  35792  mblfinlem1  35793  mblfinlem2  35794  itg2addnclem  35807  isbnd2  35920  isbnd3  35921  heiborlem7  35954  12gcd5e1  39991  lcm2un  40002  lcmineqlem19  40035  lcmineqlem20  40036  lcmineqlem22  40038  3lexlogpow5ineq2  40043  3lexlogpow5ineq4  40044  3lexlogpow5ineq3  40045  3lexlogpow2ineq1  40046  3lexlogpow2ineq2  40047  3lexlogpow5ineq5  40048  aks4d1lem1  40050  aks4d1p1p3  40057  aks4d1p1p2  40058  aks4d1p1p4  40059  aks4d1p1p6  40061  aks4d1p1p7  40062  aks4d1p1p5  40063  aks4d1p1  40064  aks4d1p2  40065  aks4d1p3  40066  aks4d1p5  40068  aks4d1p6  40069  aks4d1p7d1  40070  aks4d1p7  40071  aks4d1p8  40075  aks4d1p9  40076  2np3bcnp1  40080  2ap1caineq  40081  2xp3dxp2ge1d  40142  oexpreposd  40301  remul02  40368  sn-0ne2  40369  remul01  40370  flt4lem7  40476  rabren3dioph  40617  pellexlem2  40632  pellexlem5  40635  pell14qrgapw  40678  pellfundex  40688  rmspecsqrtnq  40708  jm2.24nn  40761  jm2.17a  40762  jm2.17b  40763  jm2.17c  40764  acongrep  40782  acongeq  40785  jm2.22  40797  jm2.23  40798  jm2.20nn  40799  jm3.1lem2  40820  expdiophlem1  40823  sqrtcval  41202  imo72b2lem0  41729  mnringaddgdOLD  41789  lhe4.4ex1a  41900  isosctrlem1ALT  42507  sineq0ALT  42510  lt3addmuld  42794  suplesup  42832  infleinflem2  42864  infleinf  42865  sumnnodd  43125  0ellimcdiv  43144  sinaover2ne0  43363  stoweidlem13  43508  stoweidlem14  43509  stoweidlem26  43521  stoweidlem49  43544  stoweidlem52  43547  wallispilem4  43563  wallispilem5  43564  wallispi  43565  wallispi2lem1  43566  wallispi2lem2  43567  wallispi2  43568  stirlinglem1  43569  stirlinglem3  43571  stirlinglem5  43573  stirlinglem6  43574  stirlinglem7  43575  stirlinglem10  43578  stirlinglem11  43579  stirlinglem15  43583  stirlingr  43585  dirker2re  43587  dirkerval2  43589  dirkerre  43590  dirkerper  43591  dirkertrigeqlem1  43593  dirkertrigeqlem3  43595  dirkercncflem1  43598  dirkercncflem2  43599  dirkercncflem4  43601  fourierdlem24  43626  fourierdlem43  43645  fourierdlem44  43646  fourierdlem57  43658  fourierdlem58  43659  fourierdlem62  43663  fourierdlem66  43667  fourierdlem68  43669  fourierdlem72  43673  fourierdlem76  43677  fourierdlem78  43679  fourierdlem79  43680  fourierdlem94  43695  fourierdlem103  43704  fourierdlem104  43705  fourierdlem111  43712  fourierdlem113  43714  sqwvfoura  43723  sqwvfourb  43724  fourierswlem  43725  fouriersw  43726  etransclem23  43752  salexct2  43832  salexct3  43835  salgencntex  43836  salgensscntex  43837  sge0ad2en  43923  ovnsubaddlem1  44062  smfmullem4  44279  smf2id  44286  2leaddle2  44742  p1lep2  44744  fmtnoge3  44934  fmtnof1  44939  fmtnoprmfac2lem1  44970  fmtno4prmfac  44976  fmtno4prm  44979  2pwp1prm  44993  31prm  45001  sfprmdvdsmersenne  45007  lighneallem2  45010  lighneallem4a  45012  lighneallem4b  45013  requad01  45025  requad1  45026  requad2  45027  dfodd4  45063  nn0o1gt2ALTV  45098  nnoALTV  45099  nn0oALTV  45100  nn0e  45101  nneven  45102  perfectALTVlem1  45125  perfectALTVlem2  45126  341fppr2  45138  9fppr8  45141  fpprel2  45145  nfermltl2rev  45147  gbowgt5  45166  sbgoldbalt  45185  sgoldbeven3prm  45187  mogoldbb  45189  nnsum3primes4  45192  nnsum3primesgbe  45196  nnsum3primesle9  45198  nnsum4primesodd  45200  nnsum4primesoddALTV  45201  wtgoldbnnsum4prm  45206  bgoldbnnsum3prm  45208  cznnring  45466  ply1mulgsumlem2  45680  zlmodzxznm  45790  zlmodzxzldeplem  45791  difmodm1lt  45820  nn0eo  45826  flnn0div2ge  45831  rege1logbzge0  45857  fldivexpfllog2  45863  logbpw2m1  45865  fllog2  45866  blenpw2m1  45877  nnpw2blen  45878  nnolog2flm1  45888  blennngt2o2  45890  dig2nn1st  45903  dig2nn0  45909  dig2bits  45912  dignn0flhalflem1  45913  dignn0flhalflem2  45914  dignn0flhalf  45916  nn0sumshdiglemA  45917  ackval42  45994  rrx2xpref1o  46016  itscnhlc0yqe  46057  itsclquadb  46074  2itscp  46079  itscnhlinecirc02p  46083  sepfsepc  46173