Theorem 2re 12231

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 12220	. 2 ⊢ 2 = (1 + 1)
2		1re 11144	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11159	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2833	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℝcr 11037  1c1 11039   + caddc 11041  2c2 12212

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-2 12220

This theorem is referenced by:  2cnALT  12233  3re  12237  3pos  12262  2lt3  12324  1lt3  12325  2lt4  12327  1lt4  12328  2lt5  12331  2lt6  12336  1lt6  12337  2lt7  12342  1lt7  12343  2lt8  12349  1lt8  12350  2lt9  12357  1lt9  12358  1le2  12361  2rene0  12363  halfre  12366  halfgt0  12368  halflt1  12370  rehalfcl  12380  halfpos2  12382  halfnneg2  12384  addltmul  12389  nominpos  12390  avglt1  12391  avglt2  12392  div4p1lem1div2  12408  nn0lele2xi  12469  nn0n0n1ge2b  12482  nn0ge2m1nn  12483  nn0le2is012  12568  halfnz  12582  3halfnz  12583  2lt10  12757  1lt10  12758  uzuzle23  12809  uzuzle24  12810  uz3m2nn  12819  2rp  12922  ge2halflem1  13034  xnn0n0n1ge2b  13058  fztpval  13514  fz0to4untppr  13558  fz0to5un2tp  13559  fzo0to42pr  13681  flhalf  13762  fldiv4p1lem1div2  13767  2txmodxeq0  13866  expubnd  14113  expmulnbnd  14170  nn0opthlem2  14204  faclbnd2  14226  faclbnd4lem1  14228  faclbnd5  14233  4bc2eq6  14264  hashgt23el  14359  hashfun  14372  hashge2el2dif  14415  hashge2el2difr  14416  hash3tpde  14428  wrdlenge2n0  14487  f1oun2prg  14852  01sqrexlem7  15183  sqrt4  15207  sqrt2gt1lt2  15209  abstri  15266  sqreulem  15295  amgm2  15305  caucvgrlem  15608  climcndslem1  15784  climcndslem2  15785  climcnds  15786  efcllem  16012  ege2le3  16025  ef01bndlem  16121  cos01bnd  16123  cos2bnd  16125  cos01gt0  16128  sin02gt0  16129  sincos2sgn  16131  sin4lt0  16132  eirrlem  16141  egt2lt3  16143  epos  16144  ene1  16147  sqrt2re  16187  mod2eq1n2dvds  16286  oddge22np1  16288  evennn2n  16290  nn0o1gt2  16320  nno  16321  nn0o  16322  nnoddm1d2  16325  bitsp1o  16372  bitsfzolem  16373  bitsfzo  16374  bitsfi  16376  6gcd4e2  16477  2mulprm  16632  ge2nprmge4  16640  isprm7  16647  3lcm2e6  16671  prmreclem2  16857  prmreclem6  16861  4sqlem11  16895  4sqlem12  16896  prmgaplem7  16997  2expltfac  17032  plusgndxnmulrndx  17229  starvndxnplusgndx  17237  scandxnplusgndx  17249  vscandxnplusgndx  17254  ipndxnplusgndx  17265  tsetndxnplusgndx  17289  plendxnplusgndx  17303  dsndxnplusgndx  17322  slotsdifunifndx  17333  efgredleme  19684  zringndrg  21435  chfacfscmul0  22814  chfacfpmmul0  22818  psmetge0  24268  xmetge0  24300  bl2in  24356  metnrmlem3  24818  iihalf1  24893  iihalf2  24896  pcoass  24992  tcphcphlem1  25203  csbren  25367  trirn  25368  minveclem2  25394  minveclem4  25400  pjthlem1  25405  ovolunlem1a  25465  dyadss  25563  opnmbllem  25570  vitalilem2  25578  vitalilem4  25580  mbfi1fseqlem5  25688  lhop1lem  25986  aaliou3lem2  26319  aaliou3lem8  26321  pilem2  26430  pilem3  26431  pipos  26436  sinhalfpilem  26440  sincosq1lem  26474  sincosq4sgn  26478  tangtx  26482  sinq12gt0  26484  sincos4thpi  26490  tan4thpi  26491  tan4thpiOLD  26492  sincos6thpi  26493  sineq0  26501  cos02pilt1  26503  cosq34lt1  26504  cosordlem  26507  cos0pilt1  26509  tanord1  26514  efif1olem1  26519  efif1olem2  26520  efif1olem4  26522  efif1o  26523  efifo  26524  2irrexpq  26708  cxpcn3lem  26725  root1id  26732  root1eq1  26733  root1cj  26734  cxpeq  26735  2logb9irr  26773  2logb3irr  26775  ang180lem1  26787  ang180lem2  26788  chordthmlem2  26811  1cubrlem  26819  atancj  26888  atantan  26901  atanbndlem  26903  atans2  26909  leibpi  26920  log2tlbnd  26923  log2ublem2  26925  log2ub  26927  divsqrtsumlem  26958  harmonicbnd3  26986  zetacvg  26993  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem4  27010  lgamgulmlem6  27012  lgamucov  27016  basellem1  27059  basellem2  27060  basellem3  27061  basellem5  27063  chtdif  27136  ppidif  27141  ppinncl  27152  chtrpcl  27153  ppieq0  27154  ppiltx  27155  ppiublem1  27181  ppiub  27183  chpeq0  27187  chteq0  27188  chtublem  27190  chtub  27191  chpval2  27197  chpub  27199  mersenne  27206  perfectlem1  27208  perfectlem2  27209  dchrptlem1  27243  dchrptlem2  27244  bcmono  27256  bclbnd  27259  bpos1lem  27261  bposlem1  27263  bposlem2  27264  bposlem3  27265  bposlem4  27266  bposlem5  27267  bposlem6  27268  bposlem7  27269  bposlem8  27270  bposlem9  27271  lgslem1  27276  lgsdirprm  27310  gausslemma2dlem0c  27337  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  gausslemma2dlem3  27347  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisen  27358  lgsquadlem1  27359  lgsquadlem2  27360  m1lgs  27367  2lgslem1a1  27368  2lgslem1a2  27369  2lgslem1c  27372  2lgslem4  27385  2sqlem11  27408  2sq2  27412  2sqreultlem  27426  2sqreunnltlem  27429  chebbnd1lem1  27448  chebbnd1lem2  27449  chebbnd1lem3  27450  chebbnd1  27451  chtppilimlem1  27452  chtppilimlem2  27453  chtppilim  27454  chto1ub  27455  chebbnd2  27456  chto1lb  27457  chpchtlim  27458  chpo1ub  27459  chpo1ubb  27460  rplogsumlem1  27463  rplogsumlem2  27464  dchrisumlem2  27469  dchrisumlem3  27470  dchrvmasumiflem1  27480  dchrisum0fno1  27490  dchrisum0re  27492  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2  27497  rplogsum  27506  mulog2sumlem1  27513  mulog2sumlem2  27514  log2sumbnd  27523  selberglem2  27525  selbergb  27528  selberg2b  27531  chpdifbndlem1  27532  logdivbnd  27535  selberg3lem1  27536  selberg3  27538  selberg4lem1  27539  selberg4  27540  pntrmax  27543  pntrsumbnd2  27546  selberg3r  27548  selberg4r  27549  selberg34r  27550  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntpbnd  27567  pntibndlem2  27570  pntibndlem3  27571  pntibnd  27572  pntlemb  27576  pntlemg  27577  pntlemh  27578  pntlemr  27581  pntlemk  27585  pntlemo  27586  pnt2  27592  pnt  27593  ostth2lem1  27597  ostth3  27617  slotsinbpsd  28525  slotslnbpsd  28526  istrkg3ld  28545  tgldimor  28586  trgcgrg  28599  tgcgr4  28615  axlowdimlem6  29032  axlowdimlem16  29042  axlowdimlem17  29043  axlowdim  29046  upgrfi  29176  umgrupgr  29188  umgrislfupgrlem  29207  umgrislfupgr  29208  lfgrnloop  29210  usgruspgr  29265  usgrislfuspgr  29272  lfuhgr1v0e  29339  usgrexmpldifpr  29343  usgrexmplef  29344  nbusgrvtxm1  29464  vdegp1bi  29623  upgrewlkle2  29692  lfgrwlkprop  29771  upgr2pthnlp  29817  usgr2pthlem  29848  pthdlem1  29851  wwlksm1edg  29966  wwlksnextwrd  29982  wwlksnextfun  29983  wwlksnextinj  29984  wwlksnextproplem3  29996  clwlkclwwlklem2a1  30079  clwlkclwwlklem2a2  30080  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwlkclwwlk2  30090  clwlkclwwlkf  30095  clwwlkext2edg  30143  konigsbergiedgw  30335  konigsbergssiedgw  30337  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  konigsberg  30344  frgrreggt1  30480  ex-pss  30515  ex-res  30528  ex-fv  30530  ex-fl  30534  ex-mod  30536  ex-abs  30542  nrt2irr  30560  ipidsq  30798  minvecolem2  30963  minvecolem4  30968  normlem7  31204  norm-ii-i  31225  norm3lemt  31240  normpar2i  31244  bcsiALT  31267  pjhthlem1  31479  opsqrlem6  32233  cdj3lem1  32522  addltmulALT  32534  nexple  32936  2exple2exp  32937  threehalves  33007  pfx1s2  33032  wrdt2ind  33046  cyc3conja  33251  drngidlhash  33527  evl1deg3  33671  rtelextdg2lem  33904  fldext2chn  33906  constraddcl  33940  iconstr  33944  2sqr3minply  33958  2sqr3nconstr  33959  cos9thpinconstrlem1  33967  cos9thpinconstrlem2  33968  sqsscirc1  34086  dya2iocucvr  34462  omssubadd  34478  oddpwdc  34532  eulerpartlemgc  34540  fibp1  34579  coinfliplem  34657  coinflipspace  34659  ballotlem2  34667  signstfveq0  34755  prodfzo03  34781  hgt750lemd  34826  logdivsqrle  34828  hgt750lem  34829  hgt750lem2  34830  hgt750leme  34836  lfuhgr2  35335  usgrcyclgt2v  35347  acycgr2v  35366  subfacp1lem1  35395  subfacp1lem5  35400  subfacval3  35405  problem2  35882  problem5  35885  circum  35890  nn0prpwlem  36538  dnibndlem10  36709  knoppcnlem2  36716  knoppcnlem4  36718  knoppcnlem10  36724  unbdqndv2lem1  36731  knoppndvlem1  36734  knoppndvlem10  36743  knoppndvlem11  36744  knoppndvlem12  36745  knoppndvlem14  36747  knoppndvlem15  36748  knoppndvlem17  36750  knoppndvlem18  36751  knoppndvlem19  36752  knoppndvlem20  36753  knoppndvlem21  36754  cnndvlem1  36759  taupi  37578  iccioo01  37582  relowlpssretop  37619  sin2h  37861  cos2h  37862  tan2h  37863  poimirlem7  37878  poimirlem9  37880  opnmbllem0  37907  mblfinlem1  37908  mblfinlem2  37909  itg2addnclem  37922  isbnd2  38034  isbnd3  38035  heiborlem7  38068  12gcd5e1  42373  lcm2un  42384  lcmineqlem19  42417  lcmineqlem20  42418  lcmineqlem22  42420  3lexlogpow5ineq2  42425  3lexlogpow5ineq4  42426  3lexlogpow5ineq3  42427  3lexlogpow2ineq1  42428  3lexlogpow2ineq2  42429  3lexlogpow5ineq5  42430  aks4d1lem1  42432  aks4d1p1p3  42439  aks4d1p1p2  42440  aks4d1p1p4  42441  aks4d1p1p6  42443  aks4d1p1p7  42444  aks4d1p1p5  42445  aks4d1p1  42446  aks4d1p2  42447  aks4d1p3  42448  aks4d1p5  42450  aks4d1p6  42451  aks4d1p7d1  42452  aks4d1p7  42453  aks4d1p8  42457  aks4d1p9  42458  posbezout  42470  aks6d1c3  42493  2np3bcnp1  42514  2ap1caineq  42515  aks6d1c6lem4  42543  aks6d1c7lem1  42550  aks6d1c7lem2  42551  oexpreposd  42692  asin1half  42727  remul02  42775  sn-0ne2  42776  remul01  42777  flt4lem7  43017  rabren3dioph  43172  pellexlem2  43187  pellexlem5  43190  pell14qrgapw  43233  pellfundex  43243  rmspecsqrtnq  43263  jm2.24nn  43316  jm2.17a  43317  jm2.17b  43318  jm2.17c  43319  acongrep  43337  acongeq  43340  jm2.22  43352  jm2.23  43353  jm2.20nn  43354  jm3.1lem2  43375  expdiophlem1  43378  sqrtcval  43997  imo72b2lem0  44521  lhe4.4ex1a  44685  isosctrlem1ALT  45289  sineq0ALT  45292  lt3addmuld  45663  suplesup  45698  infleinflem2  45729  infleinf  45730  sumnnodd  45990  0ellimcdiv  46007  sinaover2ne0  46226  stoweidlem13  46371  stoweidlem14  46372  stoweidlem26  46384  stoweidlem49  46407  stoweidlem52  46410  wallispilem4  46426  wallispilem5  46427  wallispi  46428  wallispi2lem1  46429  wallispi2lem2  46430  wallispi2  46431  stirlinglem1  46432  stirlinglem3  46434  stirlinglem5  46436  stirlinglem6  46437  stirlinglem7  46438  stirlinglem10  46441  stirlinglem11  46442  stirlinglem15  46446  stirlingr  46448  dirker2re  46450  dirkerval2  46452  dirkerre  46453  dirkerper  46454  dirkertrigeqlem1  46456  dirkertrigeqlem3  46458  dirkercncflem1  46461  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem24  46489  fourierdlem43  46508  fourierdlem44  46509  fourierdlem57  46521  fourierdlem58  46522  fourierdlem62  46526  fourierdlem66  46530  fourierdlem68  46532  fourierdlem72  46536  fourierdlem76  46540  fourierdlem78  46542  fourierdlem79  46543  fourierdlem94  46558  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  fourierdlem113  46577  sqwvfoura  46586  sqwvfourb  46587  fourierswlem  46588  fouriersw  46589  etransclem23  46615  salexct2  46697  salexct3  46700  salgencntex  46701  salgensscntex  46702  sge0ad2en  46789  ovnsubaddlem1  46928  smfmullem4  47152  smf2id  47159  nthrucw  47244  2leaddle2  47658  p1lep2  47660  2ltceilhalf  47688  ceilhalfgt1  47689  2tceilhalfelfzo1  47692  rehalfge1  47695  ceilhalfnn  47696  ceil5half3  47700  difmodm1lt  47719  fmtnoge3  47890  fmtnof1  47895  fmtnoprmfac2lem1  47926  fmtno4prmfac  47932  fmtno4prm  47935  2pwp1prm  47949  31prm  47957  sfprmdvdsmersenne  47963  lighneallem2  47966  lighneallem4a  47968  lighneallem4b  47969  requad01  47981  requad1  47982  requad2  47983  dfodd4  48019  nn0o1gt2ALTV  48054  nnoALTV  48055  nn0oALTV  48056  nn0e  48057  nneven  48058  perfectALTVlem1  48081  perfectALTVlem2  48082  341fppr2  48094  9fppr8  48097  fpprel2  48101  nfermltl2rev  48103  gbowgt5  48122  sbgoldbalt  48141  sgoldbeven3prm  48143  mogoldbb  48145  nnsum3primes4  48148  nnsum3primesgbe  48152  nnsum3primesle9  48154  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  cycl3grtri  48307  usgrexmpl1lem  48381  usgrexmpl2lem  48386  usgrexmpl2nb2  48393  usgrexmpl2nb3  48394  usgrexmpl2nb4  48395  usgrexmpl2nb5  48396  usgrexmpl2trifr  48397  gpgprismgrusgra  48418  gpg5nbgrvtx13starlem2  48432  gpg3nbgrvtx0  48436  gpg3kgrtriexlem1  48443  cznnring  48622  ply1mulgsumlem2  48747  zlmodzxznm  48857  zlmodzxzldeplem  48858  nn0eo  48888  flnn0div2ge  48893  rege1logbzge0  48919  fldivexpfllog2  48925  logbpw2m1  48927  fllog2  48928  blenpw2m1  48939  nnpw2blen  48940  nnolog2flm1  48950  blennngt2o2  48952  dig2nn1st  48965  dig2nn0  48971  dig2bits  48974  dignn0flhalflem1  48975  dignn0flhalflem2  48976  dignn0flhalf  48978  nn0sumshdiglemA  48979  ackval42  49056  rrx2xpref1o  49078  itscnhlc0yqe  49119  itsclquadb  49136  2itscp  49141  itscnhlinecirc02p  49145  sepfsepc  49287