Theorem 2re 12319

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 12308	. 2 ⊢ 2 = (1 + 1)
2		1re 11246	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11261	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2821	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2098  (class class class)co 7419  ℝcr 11139  1c1 11141   + caddc 11143  2c2 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-i2m1 11208  ax-1ne0 11209  ax-rrecex 11212  ax-cnre 11213

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-2 12308

This theorem is referenced by:  2cnALT  12321  3re  12325  2ne0  12349  3pos  12350  2lt3  12417  1lt3  12418  2lt4  12420  1lt4  12421  2lt5  12424  2lt6  12429  1lt6  12430  2lt7  12435  1lt7  12436  2lt8  12442  1lt8  12443  2lt9  12450  1lt9  12451  1le2  12454  2rene0  12456  halfre  12459  halfgt0  12461  halflt1  12463  rehalfcl  12471  halfpos2  12474  halfnneg2  12476  addltmul  12481  nominpos  12482  avglt1  12483  avglt2  12484  div4p1lem1div2  12500  nn0lele2xi  12560  nn0n0n1ge2b  12573  nn0ge2m1nn  12574  nn0le2is012  12659  halfnz  12673  3halfnz  12674  2lt10  12848  1lt10  12849  eluz4eluz2  12902  uzuzle23  12906  uz3m2nn  12908  2rp  13014  xnn0n0n1ge2b  13146  fztpval  13598  fz0to4untppr  13639  fzo0to42pr  13754  flhalf  13831  fldiv4p1lem1div2  13836  2txmodxeq0  13932  expubnd  14177  expmulnbnd  14233  nn0opthlem2  14264  faclbnd2  14286  faclbnd4lem1  14288  faclbnd5  14293  4bc2eq6  14324  hashgt23el  14419  hashfun  14432  hashge2el2dif  14477  hashge2el2difr  14478  wrdlenge2n0  14538  f1oun2prg  14904  01sqrexlem7  15231  sqrt4  15255  sqrt2gt1lt2  15257  abstri  15313  sqreulem  15342  amgm2  15352  caucvgrlem  15655  climcndslem1  15831  climcndslem2  15832  climcnds  15833  efcllem  16057  ege2le3  16070  ef01bndlem  16164  cos01bnd  16166  cos2bnd  16168  cos01gt0  16171  sin02gt0  16172  sincos2sgn  16174  sin4lt0  16175  eirrlem  16184  egt2lt3  16186  epos  16187  ene1  16190  sqrt2re  16230  mod2eq1n2dvds  16327  oddge22np1  16329  evennn2n  16331  nn0o1gt2  16361  nno  16362  nn0o  16363  nnoddm1d2  16366  bitsp1o  16411  bitsfzolem  16412  bitsfzo  16413  bitsfi  16415  6gcd4e2  16517  2mulprm  16667  ge2nprmge4  16675  isprm7  16682  3lcm2e6  16707  prmreclem2  16889  prmreclem6  16893  4sqlem11  16927  4sqlem12  16928  prmgaplem7  17029  2expltfac  17065  plusgndxnmulrndx  17281  starvndxnplusgndx  17289  scandxnplusgndx  17301  vscandxnplusgndx  17306  ipndxnplusgndx  17317  tsetndxnplusgndx  17341  plendxnplusgndx  17355  dsndxnplusgndx  17374  slotsdifunifndx  17385  oppgtsetOLD  19318  efgredleme  19710  mgpscaOLD  20095  mgptsetOLD  20097  mgpdsOLD  20100  rmodislmodOLD  20826  cnfldfunALTOLDOLD  21325  zringndrg  21411  chfacfscmul0  22804  chfacfpmmul0  22808  psmetge0  24262  xmetge0  24294  bl2in  24350  metnrmlem3  24821  iihalf1  24896  iihalf2  24899  pcoass  24995  tcphcphlem1  25207  csbren  25371  trirn  25372  minveclem2  25398  minveclem4  25404  pjthlem1  25409  ovolunlem1a  25469  dyadss  25567  opnmbllem  25574  vitalilem2  25582  vitalilem4  25584  mbfi1fseqlem5  25693  lhop1lem  25990  aaliou3lem2  26323  aaliou3lem8  26325  pilem2  26434  pilem3  26435  pipos  26440  sinhalfpilem  26443  sincosq1lem  26477  sincosq4sgn  26481  tangtx  26485  sinq12gt0  26487  sincos4thpi  26493  tan4thpi  26494  sincos6thpi  26495  sineq0  26503  cos02pilt1  26505  cosq34lt1  26506  cosordlem  26509  cos0pilt1  26511  tanord1  26516  efif1olem1  26521  efif1olem2  26522  efif1olem4  26524  efif1o  26525  efifo  26526  2irrexpq  26710  cxpcn3lem  26727  root1id  26734  root1eq1  26735  root1cj  26736  cxpeq  26737  2logb9irr  26772  2logb3irr  26774  ang180lem1  26786  ang180lem2  26787  chordthmlem2  26810  1cubrlem  26818  atancj  26887  atantan  26900  atanbndlem  26902  atans2  26908  leibpi  26919  log2tlbnd  26922  log2ublem2  26924  log2ub  26926  divsqrtsumlem  26957  harmonicbnd3  26985  zetacvg  26992  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem4  27009  lgamgulmlem6  27011  lgamucov  27015  basellem1  27058  basellem2  27059  basellem3  27060  basellem5  27062  chtdif  27135  ppidif  27140  ppinncl  27151  chtrpcl  27152  ppieq0  27153  ppiltx  27154  ppiublem1  27180  ppiub  27182  chpeq0  27186  chteq0  27187  chtublem  27189  chtub  27190  chpval2  27196  chpub  27198  mersenne  27205  perfectlem1  27207  perfectlem2  27208  dchrptlem1  27242  dchrptlem2  27243  bcmono  27255  bclbnd  27258  bpos1lem  27260  bposlem1  27262  bposlem2  27263  bposlem3  27264  bposlem4  27265  bposlem5  27266  bposlem6  27267  bposlem7  27268  bposlem8  27269  bposlem9  27270  lgslem1  27275  lgsdirprm  27309  gausslemma2dlem0c  27336  gausslemma2dlem1a  27343  gausslemma2dlem2  27345  gausslemma2dlem3  27346  lgseisenlem1  27353  lgseisenlem2  27354  lgseisenlem3  27355  lgseisen  27357  lgsquadlem1  27358  lgsquadlem2  27359  m1lgs  27366  2lgslem1a1  27367  2lgslem1a2  27368  2lgslem1c  27371  2lgslem4  27384  2sqlem11  27407  2sq2  27411  2sqreultlem  27425  2sqreunnltlem  27428  chebbnd1lem1  27447  chebbnd1lem2  27448  chebbnd1lem3  27449  chebbnd1  27450  chtppilimlem1  27451  chtppilimlem2  27452  chtppilim  27453  chto1ub  27454  chebbnd2  27455  chto1lb  27456  chpchtlim  27457  chpo1ub  27458  chpo1ubb  27459  rplogsumlem1  27462  rplogsumlem2  27463  dchrisumlem2  27468  dchrisumlem3  27469  dchrvmasumiflem1  27479  dchrisum0fno1  27489  dchrisum0re  27491  dchrisum0lem1b  27493  dchrisum0lem1  27494  dchrisum0lem2  27496  rplogsum  27505  mulog2sumlem1  27512  mulog2sumlem2  27513  log2sumbnd  27522  selberglem2  27524  selbergb  27527  selberg2b  27530  chpdifbndlem1  27531  logdivbnd  27534  selberg3lem1  27535  selberg3  27537  selberg4lem1  27538  selberg4  27539  pntrmax  27542  pntrsumbnd2  27545  selberg3r  27547  selberg4r  27548  selberg34r  27549  pntrlog2bndlem2  27556  pntrlog2bndlem3  27557  pntrlog2bndlem4  27558  pntrlog2bndlem5  27559  pntrlog2bndlem6  27561  pntrlog2bnd  27562  pntpbnd1a  27563  pntpbnd1  27564  pntpbnd2  27565  pntpbnd  27566  pntibndlem2  27569  pntibndlem3  27570  pntibnd  27571  pntlemb  27575  pntlemg  27576  pntlemh  27577  pntlemr  27580  pntlemk  27584  pntlemo  27585  pnt2  27591  pnt  27592  ostth2lem1  27596  ostth3  27616  slotsinbpsd  28317  slotslnbpsd  28318  istrkg3ld  28337  tgldimor  28378  trgcgrg  28391  tgcgr4  28407  axlowdimlem6  28830  axlowdimlem16  28840  axlowdimlem17  28841  axlowdim  28844  upgrfi  28976  umgrupgr  28988  umgrislfupgrlem  29007  umgrislfupgr  29008  lfgrnloop  29010  usgruspgr  29065  usgrislfuspgr  29072  lfuhgr1v0e  29139  usgrexmpldifpr  29143  usgrexmplef  29144  nbusgrvtxm1  29264  vdegp1bi  29423  upgrewlkle2  29492  lfgrwlkprop  29573  upgr2pthnlp  29618  usgr2pthlem  29649  pthdlem1  29652  wwlksm1edg  29764  wwlksnextwrd  29780  wwlksnextfun  29781  wwlksnextinj  29782  wwlksnextproplem3  29794  clwlkclwwlklem2a1  29874  clwlkclwwlklem2a2  29875  clwlkclwwlklem2fv1  29877  clwlkclwwlklem2fv2  29878  clwlkclwwlklem2a4  29879  clwlkclwwlklem2a  29880  clwlkclwwlklem2  29882  clwlkclwwlk2  29885  clwlkclwwlkf  29890  clwwlkext2edg  29938  konigsbergiedgw  30130  konigsbergssiedgw  30132  konigsberglem1  30134  konigsberglem2  30135  konigsberglem3  30136  konigsberg  30139  frgrreggt1  30275  ex-pss  30310  ex-res  30323  ex-fv  30325  ex-fl  30329  ex-mod  30331  ex-abs  30337  nrt2irr  30355  ipidsq  30592  minvecolem2  30757  minvecolem4  30762  normlem7  30998  norm-ii-i  31019  norm3lemt  31034  normpar2i  31038  bcsiALT  31061  pjhthlem1  31273  opsqrlem6  32027  cdj3lem1  32316  addltmulALT  32328  threehalves  32723  pfx1s2  32749  wrdt2ind  32763  oppgleOLD  32777  cyc3conja  32970  resvplusgOLD  33146  drngidlhash  33246  sqsscirc1  33640  nexple  33759  dya2iocucvr  34035  omssubadd  34051  oddpwdc  34105  eulerpartlemgc  34113  fibp1  34152  coinfliplem  34229  coinflipspace  34231  ballotlem2  34239  signstfveq0  34340  prodfzo03  34366  hgt750lemd  34411  logdivsqrle  34413  hgt750lem  34414  hgt750lem2  34415  hgt750leme  34421  lfuhgr2  34859  usgrcyclgt2v  34872  acycgr2v  34891  subfacp1lem1  34920  subfacp1lem5  34925  subfacval3  34930  problem2  35401  problem5  35404  circum  35409  nn0prpwlem  35937  dnibndlem10  36093  knoppcnlem2  36100  knoppcnlem4  36102  knoppcnlem10  36108  unbdqndv2lem1  36115  knoppndvlem1  36118  knoppndvlem10  36127  knoppndvlem11  36128  knoppndvlem12  36129  knoppndvlem14  36131  knoppndvlem15  36132  knoppndvlem17  36134  knoppndvlem18  36135  knoppndvlem19  36136  knoppndvlem20  36137  knoppndvlem21  36138  cnndvlem1  36143  taupi  36933  iccioo01  36937  relowlpssretop  36974  sin2h  37214  cos2h  37215  tan2h  37216  poimirlem7  37231  poimirlem9  37233  opnmbllem0  37260  mblfinlem1  37261  mblfinlem2  37262  itg2addnclem  37275  isbnd2  37387  isbnd3  37388  heiborlem7  37421  12gcd5e1  41606  lcm2un  41617  lcmineqlem19  41650  lcmineqlem20  41651  lcmineqlem22  41653  3lexlogpow5ineq2  41658  3lexlogpow5ineq4  41659  3lexlogpow5ineq3  41660  3lexlogpow2ineq1  41661  3lexlogpow2ineq2  41662  3lexlogpow5ineq5  41663  aks4d1lem1  41665  aks4d1p1p3  41672  aks4d1p1p2  41673  aks4d1p1p4  41674  aks4d1p1p6  41676  aks4d1p1p7  41677  aks4d1p1p5  41678  aks4d1p1  41679  aks4d1p2  41680  aks4d1p3  41681  aks4d1p5  41683  aks4d1p6  41684  aks4d1p7d1  41685  aks4d1p7  41686  aks4d1p8  41690  aks4d1p9  41691  posbezout  41703  aks6d1c3  41726  2np3bcnp1  41747  2ap1caineq  41748  aks6d1c6lem4  41776  aks6d1c7lem1  41783  aks6d1c7lem2  41784  2xp3dxp2ge1d  41827  oexpreposd  42016  remul02  42095  sn-0ne2  42096  remul01  42097  flt4lem7  42218  rabren3dioph  42377  pellexlem2  42392  pellexlem5  42395  pell14qrgapw  42438  pellfundex  42448  rmspecsqrtnq  42468  jm2.24nn  42522  jm2.17a  42523  jm2.17b  42524  jm2.17c  42525  acongrep  42543  acongeq  42546  jm2.22  42558  jm2.23  42559  jm2.20nn  42560  jm3.1lem2  42581  expdiophlem1  42584  sqrtcval  43213  imo72b2lem0  43737  mnringaddgdOLD  43797  lhe4.4ex1a  43908  isosctrlem1ALT  44515  sineq0ALT  44518  lt3addmuld  44821  suplesup  44859  infleinflem2  44891  infleinf  44892  sumnnodd  45156  0ellimcdiv  45175  sinaover2ne0  45394  stoweidlem13  45539  stoweidlem14  45540  stoweidlem26  45552  stoweidlem49  45575  stoweidlem52  45578  wallispilem4  45594  wallispilem5  45595  wallispi  45596  wallispi2lem1  45597  wallispi2lem2  45598  wallispi2  45599  stirlinglem1  45600  stirlinglem3  45602  stirlinglem5  45604  stirlinglem6  45605  stirlinglem7  45606  stirlinglem10  45609  stirlinglem11  45610  stirlinglem15  45614  stirlingr  45616  dirker2re  45618  dirkerval2  45620  dirkerre  45621  dirkerper  45622  dirkertrigeqlem1  45624  dirkertrigeqlem3  45626  dirkercncflem1  45629  dirkercncflem2  45630  dirkercncflem4  45632  fourierdlem24  45657  fourierdlem43  45676  fourierdlem44  45677  fourierdlem57  45689  fourierdlem58  45690  fourierdlem62  45694  fourierdlem66  45698  fourierdlem68  45700  fourierdlem72  45704  fourierdlem76  45708  fourierdlem78  45710  fourierdlem79  45711  fourierdlem94  45726  fourierdlem103  45735  fourierdlem104  45736  fourierdlem111  45743  fourierdlem113  45745  sqwvfoura  45754  sqwvfourb  45755  fourierswlem  45756  fouriersw  45757  etransclem23  45783  salexct2  45865  salexct3  45868  salgencntex  45869  salgensscntex  45870  sge0ad2en  45957  ovnsubaddlem1  46096  smfmullem4  46320  smf2id  46327  2leaddle2  46816  p1lep2  46818  fmtnoge3  47007  fmtnof1  47012  fmtnoprmfac2lem1  47043  fmtno4prmfac  47049  fmtno4prm  47052  2pwp1prm  47066  31prm  47074  sfprmdvdsmersenne  47080  lighneallem2  47083  lighneallem4a  47085  lighneallem4b  47086  requad01  47098  requad1  47099  requad2  47100  dfodd4  47136  nn0o1gt2ALTV  47171  nnoALTV  47172  nn0oALTV  47173  nn0e  47174  nneven  47175  perfectALTVlem1  47198  perfectALTVlem2  47199  341fppr2  47211  9fppr8  47214  fpprel2  47218  nfermltl2rev  47220  gbowgt5  47239  sbgoldbalt  47258  sgoldbeven3prm  47260  mogoldbb  47262  nnsum3primes4  47265  nnsum3primesgbe  47269  nnsum3primesle9  47271  nnsum4primesodd  47273  nnsum4primesoddALTV  47274  wtgoldbnnsum4prm  47279  bgoldbnnsum3prm  47281  cznnring  47510  ply1mulgsumlem2  47641  zlmodzxznm  47751  zlmodzxzldeplem  47752  difmodm1lt  47781  nn0eo  47787  flnn0div2ge  47792  rege1logbzge0  47818  fldivexpfllog2  47824  logbpw2m1  47826  fllog2  47827  blenpw2m1  47838  nnpw2blen  47839  nnolog2flm1  47849  blennngt2o2  47851  dig2nn1st  47864  dig2nn0  47870  dig2bits  47873  dignn0flhalflem1  47874  dignn0flhalflem2  47875  dignn0flhalf  47877  nn0sumshdiglemA  47878  ackval42  47955  rrx2xpref1o  47977  itscnhlc0yqe  48018  itsclquadb  48035  2itscp  48040  itscnhlinecirc02p  48044  sepfsepc  48132