Theorem 2re 10967

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 10956	. 2 ⊢ 2 = (1 + 1)
2		1re 9918	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 9932	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2684	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 1977  (class class class)co 6549  ℝcr 9814  1c1 9816   + caddc 9818  2c2 10947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-2 10956

This theorem is referenced by:  2cn  10968  3re  10971  2ne0  10990  3pos  10991  2lt3  11072  1lt3  11073  2lt4  11075  1lt4  11076  2lt5  11079  2lt6  11084  1lt6  11085  2lt7  11090  1lt7  11091  2lt8  11097  1lt8  11098  2lt9  11105  1lt9  11106  2lt10OLD  11114  1lt10OLD  11115  1le2  11118  2rene0  11120  halfre  11123  halfgt0  11125  halflt1  11127  rehalfcl  11135  halfpos2  11138  halfnneg2  11140  addltmul  11145  nominpos  11146  avglt1  11147  avglt2  11148  div4p1lem1div2  11164  nn0lele2xi  11225  nn0n0n1ge2b  11236  nn0ge2m1nn  11237  halfnz  11331  3halfnz  11332  2lt10  11556  1lt10  11557  uzuzle23  11605  uz3m2nn  11607  2rp  11713  zgt1rpn0n1  11747  xnn0n0n1ge2b  11841  fztpval  12272  fz0to4untppr  12311  fzo0to42pr  12422  2tnp1ge0ge0  12492  flhalf  12493  fldiv4p1lem1div2  12498  fldiv4lem1div2uz2  12499  2txmodxeq0  12592  expubnd  12783  expmulnbnd  12858  nn0opthlem2  12918  faclbnd2  12940  faclbnd4lem1  12942  faclbnd5  12947  4bc2eq6  12978  hashfun  13084  hashge2el2dif  13117  hashge2el2difr  13118  wrdlenge2n0  13196  f1oun2prg  13512  2swrd2eqwrdeq  13544  sqrlem7  13837  sqrt4  13861  sqrt2gt1lt2  13863  abstri  13918  sqreulem  13947  amgm2  13957  caucvgrlem  14251  iseralt  14263  climcndslem1  14420  climcndslem2  14421  climcnds  14422  geoihalfsum  14453  efcllem  14647  ege2le3  14659  ef01bndlem  14753  cos01bnd  14755  cos2bnd  14757  cos01gt0  14760  sin02gt0  14761  sincos2sgn  14763  sin4lt0  14764  eirrlem  14771  egt2lt3  14773  epos  14774  ene1  14777  sqrt2re  14818  oexpneg  14907  mod2eq1n2dvds  14909  oddge22np1  14911  evennn02n  14912  evennn2n  14913  nn0ehalf  14933  nn0o1gt2  14935  nno  14936  nn0o  14937  nn0oddm1d2  14939  nnoddm1d2  14940  n2dvds1  14942  flodddiv4t2lthalf  14978  bitsp1o  14993  bitsfzolem  14994  bitsfzo  14995  bitsfi  14997  6gcd4e2  15093  isprm7  15258  3lcm2e6  15278  oddprm  15353  iserodd  15378  prmreclem2  15459  prmreclem6  15463  4sqlem11  15497  4sqlem12  15498  prmgaplem7  15599  2expltfac  15637  oppgtset  17605  efgredleme  17979  mgpsca  18319  mgptset  18320  mgpds  18322  zringndrg  19657  matplusg  20039  chfacfscmul0  20482  chfacfpmmul0  20486  psmetge0  21927  xmetge0  21959  bl2in  22015  metnrmlem3  22472  iihalf1  22538  iihalf2  22540  pcoass  22632  tchcphlem1  22842  csbren  22990  trirn  22991  minveclem2  23005  minveclem4  23011  pjthlem1  23016  ovolunlem1a  23071  dyadss  23168  opnmbllem  23175  vitalilem2  23184  vitalilem4  23186  mbfi1fseqlem5  23292  lhop1lem  23580  aaliou3lem2  23902  aaliou3lem8  23904  pilem2  24010  pilem3  24011  pipos  24016  sinhalfpilem  24019  sincosq1lem  24053  sincosq4sgn  24057  tangtx  24061  sinq12gt0  24063  sincos4thpi  24069  tan4thpi  24070  sincos6thpi  24071  sineq0  24077  cosordlem  24081  tanord1  24087  efif1olem1  24092  efif1olem2  24093  efif1olem4  24095  efif1o  24096  efifo  24097  cxpcn3lem  24288  root1id  24295  root1eq1  24296  root1cj  24297  cxpeq  24298  logblog  24330  ang180lem1  24339  ang180lem2  24340  chordthmlem2  24360  1cubrlem  24368  atancj  24437  atantan  24450  atanbndlem  24452  atans2  24458  leibpilem1  24467  leibpi  24469  log2tlbnd  24472  log2ublem2  24474  log2ub  24476  divsqrtsumlem  24506  harmonicbnd3  24534  zetacvg  24541  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem6  24560  lgamucov  24564  basellem1  24607  basellem2  24608  basellem3  24609  basellem5  24611  chtdif  24684  ppidif  24689  ppinncl  24700  chtrpcl  24701  ppieq0  24702  ppiltx  24703  ppiublem1  24727  ppiub  24729  chpeq0  24733  chteq0  24734  chtublem  24736  chtub  24737  chpval2  24743  chpub  24745  mersenne  24752  perfectlem1  24754  perfectlem2  24755  dchrptlem1  24789  dchrptlem2  24790  bcmono  24802  bclbnd  24805  bpos1lem  24807  bposlem1  24809  bposlem2  24810  bposlem3  24811  bposlem4  24812  bposlem5  24813  bposlem6  24814  bposlem7  24815  bposlem8  24816  bposlem9  24817  lgslem1  24822  lgsdirprm  24856  gausslemma2dlem0c  24883  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  gausslemma2dlem3  24893  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisen  24904  lgsquadlem1  24905  lgsquadlem2  24906  m1lgs  24913  2lgslem1a1  24914  2lgslem1a2  24915  2lgslem1c  24918  2lgslem4  24931  2sqlem11  24954  chebbnd1lem1  24958  chebbnd1lem2  24959  chebbnd1lem3  24960  chebbnd1  24961  chtppilimlem1  24962  chtppilimlem2  24963  chtppilim  24964  chto1ub  24965  chebbnd2  24966  chto1lb  24967  chpchtlim  24968  chpo1ub  24969  chpo1ubb  24970  rplogsumlem1  24973  rplogsumlem2  24974  dchrisumlem2  24979  dchrisumlem3  24980  dchrvmasumiflem1  24990  dchrisum0fno1  25000  dchrisum0re  25002  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2  25007  rplogsum  25016  mulog2sumlem1  25023  mulog2sumlem2  25024  log2sumbnd  25033  selberglem2  25035  selbergb  25038  selberg2b  25041  chpdifbndlem1  25042  logdivbnd  25045  selberg3lem1  25046  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrmax  25053  pntrsumbnd2  25056  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntpbnd  25077  pntibndlem2  25080  pntibndlem3  25081  pntibnd  25082  pntlemb  25086  pntlemg  25087  pntlemh  25088  pntlemr  25091  pntlemk  25095  pntlemo  25096  pnt2  25102  pnt  25103  ostth2lem1  25107  ostth3  25127  istrkg3ld  25160  tgldimor  25197  trgcgrg  25210  tgcgr4  25226  axlowdimlem6  25627  axlowdimlem16  25637  axlowdimlem17  25638  axlowdim  25641  upgrfi  25758  umgrupgr  25769  umgrislfupgrlem  25788  umgrislfupgr  25789  lfgrnloop  25791  upgredg  25811  umgrafi  25851  usisuslgra  25894  usgraex2elv  25926  usgraexmpldifpr  25928  constr3lem4  26175  constr3trllem3  26180  constr3pthlem1  26183  constr3pthlem3  26185  wwlkextwrd  26256  wwlkextfun  26257  wwlkextinj  26258  wwlkm1edg  26263  wwlkextproplem3  26271  clwwlkgt0  26299  clwwlkn0  26302  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2a2  26308  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwlkisclwwlk2  26318  clwwlkext2edg  26330  usg2cwwkdifex  26349  clwlkfclwwlk  26371  konigsberg  26514  vdgfrgragt2  26554  extwwlkfablem2  26605  numclwwlkovf2ex  26613  frgrareggt1  26643  frgrareg  26644  frgraregord013  26645  ex-pss  26677  ex-res  26690  ex-fv  26692  ex-fl  26696  ex-mod  26698  ex-abs  26704  nvge0  26912  ipidsq  26949  minvecolem2  27115  minvecolem4  27120  normlem7  27357  norm-ii-i  27378  norm3lemt  27393  normpar2i  27397  bcsiALT  27420  pjhthlem1  27634  opsqrlem6  28388  cdj3lem1  28677  addltmulALT  28689  oppgle  28984  resvplusg  29164  sqsscirc1  29282  nexple  29399  dya2iocucvr  29673  omssubadd  29689  oddpwdc  29743  eulerpartlemgc  29751  fibp1  29790  coinfliplem  29867  coinflipspace  29869  ballotlem2  29877  signstfveq0  29980  subfacp1lem1  30415  subfacp1lem5  30420  subfacval3  30425  problem2  30813  problem2OLD  30814  problem5  30817  circum  30822  nn0prpwlem  31487  dnibndlem10  31647  knoppcnlem2  31654  knoppcnlem4  31656  knoppcnlem10  31662  unbdqndv2lem1  31670  knoppndvlem1  31673  knoppndvlem10  31682  knoppndvlem11  31683  knoppndvlem12  31684  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem18  31690  knoppndvlem19  31691  knoppndvlem20  31692  knoppndvlem21  31693  cnndvlem1  31698  taupi  32346  relowlpssretop  32388  sin2h  32569  cos2h  32570  tan2h  32571  poimirlem7  32586  poimirlem9  32588  opnmbllem0  32615  mblfinlem1  32616  mblfinlem2  32617  itg2addnclem  32631  isbnd2  32752  isbnd3  32753  heiborlem7  32786  rabren3dioph  36397  pellexlem2  36412  pellexlem5  36415  pell14qrgapw  36458  pellfundex  36468  rmspecsqrtnq  36488  rmspecsqrtnqOLD  36489  jm2.24nn  36544  jm2.17a  36545  jm2.17b  36546  jm2.17c  36547  acongrep  36565  acongeq  36568  jm2.22  36580  jm2.23  36581  jm2.20nn  36582  jm3.1lem2  36603  expdiophlem1  36606  imo72b2lem0  37487  lhe4.4ex1a  37550  isosctrlem1ALT  38192  sineq0ALT  38195  lt3addmuld  38456  suplesup  38496  infleinflem2  38528  infleinf  38529  sumnnodd  38697  0ellimcdiv  38716  sinaover2ne0  38751  stoweidlem13  38906  stoweidlem14  38907  stoweidlem26  38919  stoweidlem49  38942  stoweidlem52  38945  wallispilem4  38961  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  wallispi2  38966  stirlinglem1  38967  stirlinglem3  38969  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem11  38977  stirlinglem15  38981  stirlingr  38983  dirker2re  38985  dirkerval2  38987  dirkerre  38988  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem3  38993  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem24  39024  fourierdlem43  39043  fourierdlem44  39044  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  fourierdlem66  39065  fourierdlem68  39067  fourierdlem72  39071  fourierdlem76  39075  fourierdlem78  39077  fourierdlem79  39078  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem113  39112  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  etransclem23  39150  salexct2  39233  salexct3  39236  salgencntex  39237  salgensscntex  39238  sge0ad2en  39324  ovnsubaddlem1  39460  smfmullem4  39679  smf2id  39686  fmtnoge3  39980  fmtnof1  39985  fmtnoprmfac2lem1  40016  fmtno4prmfac  40022  fmtno4prm  40025  2pwp1prm  40041  31prm  40050  sfprmdvdsmersenne  40058  lighneallem2  40061  lighneallem4a  40063  lighneallem4b  40064  dfodd4  40109  oexpnegALTV  40126  nn0o1gt2ALTV  40143  nnoALTV  40144  nn0oALTV  40145  nn0e  40146  perfectALTVlem1  40164  perfectALTVlem2  40165  gbogt5  40184  sgoldbalt  40203  nnsum3primes4  40204  nnsum3primesgbe  40208  nnsum3primesle9  40210  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  pfx2  40275  2leaddle2  40344  p1lep2  40346  usgruspgr  40408  usgrislfuspgr  40414  lfuhgr1v0e  40480  nbusgrvtxm1  40607  vdegp1bi-av  40753  upgrewlkle2  40808  lfgrwlkprop  40896  upgr2pthnlp  40938  usgr2pthlem  40969  pthdlem1  40972  wwlksm1edg  41078  wwlksnextwrd  41103  wwlksnextfun  41104  wwlksnextinj  41105  wwlksnextproplem3  41117  clwlkclwwlklem2a1  41201  clwlkclwwlklem2a2  41202  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwlkclwwlk2  41212  clwwlksext2edg  41230  clwlksfclwwlk  41269  konigsbergiedgw  41416  konigsbergiedgwOLD  41417  konigsbergssiedgw  41419  konigsberglem1  41422  konigsberglem2  41423  konigsberglem3  41424  konigsberg-av  41427  frgrwopreglem2  41482  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  av-frgrareggt1  41547  plusgndxnmulrndx  41743  cznnring  41748  nn0le2is012  41938  ply1mulgsumlem2  41969  zlmodzxznm  42080  zlmodzxzldeplem  42081  difmodm1lt  42111  nn0eo  42116  flnn0div2ge  42121  rege1logbzge0  42151  fldivexpfllog2  42157  logbpw2m1  42159  fllog2  42160  blenpw2m1  42171  nnpw2blen  42172  nnolog2flm1  42182  blennngt2o2  42184  dig2nn1st  42197  dig2nn0  42203  dig2bits  42206  dignn0flhalflem1  42207  dignn0flhalflem2  42208  dignn0flhalf  42210  nn0sumshdiglemA  42211