Theorem 2re 12036

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 12025	. 2 ⊢ 2 = (1 + 1)
2		1re 10964	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 10979	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2835	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7269  ℝcr 10859  1c1 10861   + caddc 10863  2c2 12017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-1cn 10918  ax-icn 10919  ax-addcl 10920  ax-addrcl 10921  ax-mulcl 10922  ax-mulrcl 10923  ax-i2m1 10928  ax-1ne0 10929  ax-rrecex 10932  ax-cnre 10933

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-iota 6386  df-fv 6436  df-ov 7272  df-2 12025

This theorem is referenced by:  2cnALT  12038  3re  12042  2ne0  12066  3pos  12067  2lt3  12134  1lt3  12135  2lt4  12137  1lt4  12138  2lt5  12141  2lt6  12146  1lt6  12147  2lt7  12152  1lt7  12153  2lt8  12159  1lt8  12160  2lt9  12167  1lt9  12168  1le2  12171  2rene0  12173  halfre  12176  halfgt0  12178  halflt1  12180  rehalfcl  12188  halfpos2  12191  halfnneg2  12193  addltmul  12198  nominpos  12199  avglt1  12200  avglt2  12201  div4p1lem1div2  12217  nn0lele2xi  12277  nn0n0n1ge2b  12290  nn0ge2m1nn  12291  nn0le2is012  12373  halfnz  12387  3halfnz  12388  2lt10  12564  1lt10  12565  eluz4eluz2  12614  uzuzle23  12618  uz3m2nn  12620  2rp  12724  xnn0n0n1ge2b  12856  fztpval  13307  fz0to4untppr  13348  fzo0to42pr  13463  flhalf  13539  fldiv4p1lem1div2  13544  2txmodxeq0  13640  expubnd  13884  expmulnbnd  13939  nn0opthlem2  13972  faclbnd2  13994  faclbnd4lem1  13996  faclbnd5  14001  4bc2eq6  14032  hashgt23el  14128  hashfun  14141  hashge2el2dif  14183  hashge2el2difr  14184  wrdlenge2n0  14244  f1oun2prg  14619  sqrlem7  14949  sqrt4  14973  sqrt2gt1lt2  14975  abstri  15031  sqreulem  15060  amgm2  15070  caucvgrlem  15373  climcndslem1  15550  climcndslem2  15551  climcnds  15552  efcllem  15776  ege2le3  15788  ef01bndlem  15882  cos01bnd  15884  cos2bnd  15886  cos01gt0  15889  sin02gt0  15890  sincos2sgn  15892  sin4lt0  15893  eirrlem  15902  egt2lt3  15904  epos  15905  ene1  15908  sqrt2re  15948  mod2eq1n2dvds  16045  oddge22np1  16047  evennn2n  16049  nn0o1gt2  16079  nno  16080  nn0o  16081  nnoddm1d2  16084  bitsp1o  16129  bitsfzolem  16130  bitsfzo  16131  bitsfi  16133  6gcd4e2  16235  2mulprm  16387  ge2nprmge4  16395  isprm7  16402  3lcm2e6  16425  prmreclem2  16607  prmreclem6  16611  4sqlem11  16645  4sqlem12  16646  prmgaplem7  16747  2expltfac  16783  plusgndxnmulrndx  16996  starvndxnplusgndx  17004  scandxnplusgndx  17016  vscandxnplusgndx  17021  ipndxnplusgndx  17032  tsetndxnplusgndx  17056  plendxnplusgndx  17070  dsndxnplusgndx  17089  slotsdifunifndx  17100  oppgtsetOLD  18948  efgredleme  19338  mgpscaOLD  19718  mgptsetOLD  19720  mgpdsOLD  19723  rmodislmodOLD  20181  cnfldfunALTOLD  20600  zringndrg  20679  chfacfscmul0  21996  chfacfpmmul0  22000  psmetge0  23454  xmetge0  23486  bl2in  23542  metnrmlem3  24013  iihalf1  24083  iihalf2  24085  pcoass  24176  tcphcphlem1  24388  csbren  24552  trirn  24553  minveclem2  24579  minveclem4  24585  pjthlem1  24590  ovolunlem1a  24649  dyadss  24747  opnmbllem  24754  vitalilem2  24762  vitalilem4  24764  mbfi1fseqlem5  24873  lhop1lem  25166  aaliou3lem2  25492  aaliou3lem8  25494  pilem2  25600  pilem3  25601  pipos  25606  sinhalfpilem  25609  sincosq1lem  25643  sincosq4sgn  25647  tangtx  25651  sinq12gt0  25653  sincos4thpi  25659  tan4thpi  25660  sincos6thpi  25661  sineq0  25669  cos02pilt1  25671  cosq34lt1  25672  cosordlem  25675  cos0pilt1  25677  tanord1  25682  efif1olem1  25687  efif1olem2  25688  efif1olem4  25690  efif1o  25691  efifo  25692  2irrexpq  25874  cxpcn3lem  25889  root1id  25896  root1eq1  25897  root1cj  25898  cxpeq  25899  2logb9irr  25934  2logb3irr  25936  ang180lem1  25948  ang180lem2  25949  chordthmlem2  25972  1cubrlem  25980  atancj  26049  atantan  26062  atanbndlem  26064  atans2  26070  leibpi  26081  log2tlbnd  26084  log2ublem2  26086  log2ub  26088  divsqrtsumlem  26118  harmonicbnd3  26146  zetacvg  26153  lgamgulmlem2  26168  lgamgulmlem3  26169  lgamgulmlem4  26170  lgamgulmlem6  26172  lgamucov  26176  basellem1  26219  basellem2  26220  basellem3  26221  basellem5  26223  chtdif  26296  ppidif  26301  ppinncl  26312  chtrpcl  26313  ppieq0  26314  ppiltx  26315  ppiublem1  26339  ppiub  26341  chpeq0  26345  chteq0  26346  chtublem  26348  chtub  26349  chpval2  26355  chpub  26357  mersenne  26364  perfectlem1  26366  perfectlem2  26367  dchrptlem1  26401  dchrptlem2  26402  bcmono  26414  bclbnd  26417  bpos1lem  26419  bposlem1  26421  bposlem2  26422  bposlem3  26423  bposlem4  26424  bposlem5  26425  bposlem6  26426  bposlem7  26427  bposlem8  26428  bposlem9  26429  lgslem1  26434  lgsdirprm  26468  gausslemma2dlem0c  26495  gausslemma2dlem1a  26502  gausslemma2dlem2  26504  gausslemma2dlem3  26505  lgseisenlem1  26512  lgseisenlem2  26513  lgseisenlem3  26514  lgseisen  26516  lgsquadlem1  26517  lgsquadlem2  26518  m1lgs  26525  2lgslem1a1  26526  2lgslem1a2  26527  2lgslem1c  26530  2lgslem4  26543  2sqlem11  26566  2sq2  26570  2sqreultlem  26584  2sqreunnltlem  26587  chebbnd1lem1  26606  chebbnd1lem2  26607  chebbnd1lem3  26608  chebbnd1  26609  chtppilimlem1  26610  chtppilimlem2  26611  chtppilim  26612  chto1ub  26613  chebbnd2  26614  chto1lb  26615  chpchtlim  26616  chpo1ub  26617  chpo1ubb  26618  rplogsumlem1  26621  rplogsumlem2  26622  dchrisumlem2  26627  dchrisumlem3  26628  dchrvmasumiflem1  26638  dchrisum0fno1  26648  dchrisum0re  26650  dchrisum0lem1b  26652  dchrisum0lem1  26653  dchrisum0lem2  26655  rplogsum  26664  mulog2sumlem1  26671  mulog2sumlem2  26672  log2sumbnd  26681  selberglem2  26683  selbergb  26686  selberg2b  26689  chpdifbndlem1  26690  logdivbnd  26693  selberg3lem1  26694  selberg3  26696  selberg4lem1  26697  selberg4  26698  pntrmax  26701  pntrsumbnd2  26704  selberg3r  26706  selberg4r  26707  selberg34r  26708  pntrlog2bndlem2  26715  pntrlog2bndlem3  26716  pntrlog2bndlem4  26717  pntrlog2bndlem5  26718  pntrlog2bndlem6  26720  pntrlog2bnd  26721  pntpbnd1a  26722  pntpbnd1  26723  pntpbnd2  26724  pntpbnd  26725  pntibndlem2  26728  pntibndlem3  26729  pntibnd  26730  pntlemb  26734  pntlemg  26735  pntlemh  26736  pntlemr  26739  pntlemk  26743  pntlemo  26744  pnt2  26750  pnt  26751  ostth2lem1  26755  ostth3  26775  slotsinbpsd  26791  slotslnbpsd  26792  istrkg3ld  26811  tgldimor  26852  trgcgrg  26865  tgcgr4  26881  axlowdimlem6  27304  axlowdimlem16  27314  axlowdimlem17  27315  axlowdim  27318  upgrfi  27450  umgrupgr  27462  umgrislfupgrlem  27481  umgrislfupgr  27482  lfgrnloop  27484  usgruspgr  27537  usgrislfuspgr  27543  lfuhgr1v0e  27610  usgrexmpldifpr  27614  usgrexmplef  27615  nbusgrvtxm1  27735  vdegp1bi  27893  upgrewlkle2  27962  lfgrwlkprop  28043  upgr2pthnlp  28087  usgr2pthlem  28118  pthdlem1  28121  wwlksm1edg  28233  wwlksnextwrd  28249  wwlksnextfun  28250  wwlksnextinj  28251  wwlksnextproplem3  28263  clwlkclwwlklem2a1  28343  clwlkclwwlklem2a2  28344  clwlkclwwlklem2fv1  28346  clwlkclwwlklem2fv2  28347  clwlkclwwlklem2a4  28348  clwlkclwwlklem2a  28349  clwlkclwwlklem2  28351  clwlkclwwlk2  28354  clwlkclwwlkf  28359  clwwlkext2edg  28407  konigsbergiedgw  28599  konigsbergssiedgw  28601  konigsberglem1  28603  konigsberglem2  28604  konigsberglem3  28605  konigsberg  28608  frgrreggt1  28744  ex-pss  28779  ex-res  28792  ex-fv  28794  ex-fl  28798  ex-mod  28800  ex-abs  28806  ipidsq  29059  minvecolem2  29224  minvecolem4  29229  normlem7  29465  norm-ii-i  29486  norm3lemt  29501  normpar2i  29505  bcsiALT  29528  pjhthlem1  29740  opsqrlem6  30494  cdj3lem1  30783  addltmulALT  30795  threehalves  31176  pfx1s2  31200  wrdt2ind  31212  oppgleOLD  31226  cyc3conja  31411  resvplusgOLD  31522  sqsscirc1  31845  nexple  31964  dya2iocucvr  32238  omssubadd  32254  oddpwdc  32308  eulerpartlemgc  32316  fibp1  32355  coinfliplem  32432  coinflipspace  32434  ballotlem2  32442  signstfveq0  32543  prodfzo03  32570  hgt750lemd  32615  logdivsqrle  32617  hgt750lem  32618  hgt750lem2  32619  hgt750leme  32625  lfuhgr2  33067  usgrcyclgt2v  33080  acycgr2v  33099  subfacp1lem1  33128  subfacp1lem5  33133  subfacval3  33138  problem2  33611  problem5  33614  circum  33619  nn0prpwlem  34498  dnibndlem10  34654  knoppcnlem2  34661  knoppcnlem4  34663  knoppcnlem10  34669  unbdqndv2lem1  34676  knoppndvlem1  34679  knoppndvlem10  34688  knoppndvlem11  34689  knoppndvlem12  34690  knoppndvlem14  34692  knoppndvlem15  34693  knoppndvlem17  34695  knoppndvlem18  34696  knoppndvlem19  34697  knoppndvlem20  34698  knoppndvlem21  34699  cnndvlem1  34704  taupi  35481  iccioo01  35485  relowlpssretop  35522  sin2h  35754  cos2h  35755  tan2h  35756  poimirlem7  35771  poimirlem9  35773  opnmbllem0  35800  mblfinlem1  35801  mblfinlem2  35802  itg2addnclem  35815  isbnd2  35928  isbnd3  35929  heiborlem7  35962  12gcd5e1  39998  lcm2un  40009  lcmineqlem19  40042  lcmineqlem20  40043  lcmineqlem22  40045  3lexlogpow5ineq2  40050  3lexlogpow5ineq4  40051  3lexlogpow5ineq3  40052  3lexlogpow2ineq1  40053  3lexlogpow2ineq2  40054  3lexlogpow5ineq5  40055  aks4d1lem1  40057  aks4d1p1p3  40064  aks4d1p1p2  40065  aks4d1p1p4  40066  aks4d1p1p6  40068  aks4d1p1p7  40069  aks4d1p1p5  40070  aks4d1p1  40071  aks4d1p2  40072  aks4d1p3  40073  aks4d1p5  40075  aks4d1p6  40076  aks4d1p7d1  40077  aks4d1p7  40078  aks4d1p8  40082  aks4d1p9  40083  2np3bcnp1  40087  2ap1caineq  40088  2xp3dxp2ge1d  40149  oexpreposd  40308  remul02  40375  sn-0ne2  40376  remul01  40377  flt4lem7  40483  rabren3dioph  40624  pellexlem2  40639  pellexlem5  40642  pell14qrgapw  40685  pellfundex  40695  rmspecsqrtnq  40715  jm2.24nn  40768  jm2.17a  40769  jm2.17b  40770  jm2.17c  40771  acongrep  40789  acongeq  40792  jm2.22  40804  jm2.23  40805  jm2.20nn  40806  jm3.1lem2  40827  expdiophlem1  40830  sqrtcval  41209  imo72b2lem0  41736  mnringaddgdOLD  41796  lhe4.4ex1a  41907  isosctrlem1ALT  42514  sineq0ALT  42517  lt3addmuld  42800  suplesup  42838  infleinflem2  42870  infleinf  42871  sumnnodd  43131  0ellimcdiv  43150  sinaover2ne0  43369  stoweidlem13  43514  stoweidlem14  43515  stoweidlem26  43527  stoweidlem49  43550  stoweidlem52  43553  wallispilem4  43569  wallispilem5  43570  wallispi  43571  wallispi2lem1  43572  wallispi2lem2  43573  wallispi2  43574  stirlinglem1  43575  stirlinglem3  43577  stirlinglem5  43579  stirlinglem6  43580  stirlinglem7  43581  stirlinglem10  43584  stirlinglem11  43585  stirlinglem15  43589  stirlingr  43591  dirker2re  43593  dirkerval2  43595  dirkerre  43596  dirkerper  43597  dirkertrigeqlem1  43599  dirkertrigeqlem3  43601  dirkercncflem1  43604  dirkercncflem2  43605  dirkercncflem4  43607  fourierdlem24  43632  fourierdlem43  43651  fourierdlem44  43652  fourierdlem57  43664  fourierdlem58  43665  fourierdlem62  43669  fourierdlem66  43673  fourierdlem68  43675  fourierdlem72  43679  fourierdlem76  43683  fourierdlem78  43685  fourierdlem79  43686  fourierdlem94  43701  fourierdlem103  43710  fourierdlem104  43711  fourierdlem111  43718  fourierdlem113  43720  sqwvfoura  43729  sqwvfourb  43730  fourierswlem  43731  fouriersw  43732  etransclem23  43758  salexct2  43838  salexct3  43841  salgencntex  43842  salgensscntex  43843  sge0ad2en  43929  ovnsubaddlem1  44068  smfmullem4  44285  smf2id  44292  2leaddle2  44747  p1lep2  44749  fmtnoge3  44939  fmtnof1  44944  fmtnoprmfac2lem1  44975  fmtno4prmfac  44981  fmtno4prm  44984  2pwp1prm  44998  31prm  45006  sfprmdvdsmersenne  45012  lighneallem2  45015  lighneallem4a  45017  lighneallem4b  45018  requad01  45030  requad1  45031  requad2  45032  dfodd4  45068  nn0o1gt2ALTV  45103  nnoALTV  45104  nn0oALTV  45105  nn0e  45106  nneven  45107  perfectALTVlem1  45130  perfectALTVlem2  45131  341fppr2  45143  9fppr8  45146  fpprel2  45150  nfermltl2rev  45152  gbowgt5  45171  sbgoldbalt  45190  sgoldbeven3prm  45192  mogoldbb  45194  nnsum3primes4  45197  nnsum3primesgbe  45201  nnsum3primesle9  45203  nnsum4primesodd  45205  nnsum4primesoddALTV  45206  wtgoldbnnsum4prm  45211  bgoldbnnsum3prm  45213  cznnring  45471  ply1mulgsumlem2  45685  zlmodzxznm  45795  zlmodzxzldeplem  45796  difmodm1lt  45825  nn0eo  45831  flnn0div2ge  45836  rege1logbzge0  45862  fldivexpfllog2  45868  logbpw2m1  45870  fllog2  45871  blenpw2m1  45882  nnpw2blen  45883  nnolog2flm1  45893  blennngt2o2  45895  dig2nn1st  45908  dig2nn0  45914  dig2bits  45917  dignn0flhalflem1  45918  dignn0flhalflem2  45919  dignn0flhalf  45921  nn0sumshdiglemA  45922  ackval42  45999  rrx2xpref1o  46021  itscnhlc0yqe  46062  itsclquadb  46079  2itscp  46084  itscnhlinecirc02p  46088  sepfsepc  46178