Theorem 2re 12340

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

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  ℝcr 11154  1c1 11156   + caddc 11158  2c2 12321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-2 12329

This theorem is referenced by:  2cnALT  12342  3re  12346  2ne0  12370  3pos  12371  2lt3  12438  1lt3  12439  2lt4  12441  1lt4  12442  2lt5  12445  2lt6  12450  1lt6  12451  2lt7  12456  1lt7  12457  2lt8  12463  1lt8  12464  2lt9  12471  1lt9  12472  1le2  12475  2rene0  12477  halfre  12480  halfgt0  12482  halflt1  12484  rehalfcl  12492  halfpos2  12495  halfnneg2  12497  addltmul  12502  nominpos  12503  avglt1  12504  avglt2  12505  div4p1lem1div2  12521  nn0lele2xi  12582  nn0n0n1ge2b  12595  nn0ge2m1nn  12596  nn0le2is012  12682  halfnz  12696  3halfnz  12697  2lt10  12871  1lt10  12872  eluz4eluz2  12925  uzuzle23  12931  uz3m2nn  12933  2rp  13039  ge2halflem1  13150  xnn0n0n1ge2b  13174  fztpval  13626  fz0to4untppr  13670  fz0to5un2tp  13671  fzo0to42pr  13792  flhalf  13870  fldiv4p1lem1div2  13875  2txmodxeq0  13972  expubnd  14217  expmulnbnd  14274  nn0opthlem2  14308  faclbnd2  14330  faclbnd4lem1  14332  faclbnd5  14337  4bc2eq6  14368  hashgt23el  14463  hashfun  14476  hashge2el2dif  14519  hashge2el2difr  14520  hash3tpde  14532  wrdlenge2n0  14590  f1oun2prg  14956  01sqrexlem7  15287  sqrt4  15311  sqrt2gt1lt2  15313  abstri  15369  sqreulem  15398  amgm2  15408  caucvgrlem  15709  climcndslem1  15885  climcndslem2  15886  climcnds  15887  efcllem  16113  ege2le3  16126  ef01bndlem  16220  cos01bnd  16222  cos2bnd  16224  cos01gt0  16227  sin02gt0  16228  sincos2sgn  16230  sin4lt0  16231  eirrlem  16240  egt2lt3  16242  epos  16243  ene1  16246  sqrt2re  16286  mod2eq1n2dvds  16384  oddge22np1  16386  evennn2n  16388  nn0o1gt2  16418  nno  16419  nn0o  16420  nnoddm1d2  16423  bitsp1o  16470  bitsfzolem  16471  bitsfzo  16472  bitsfi  16474  6gcd4e2  16575  2mulprm  16730  ge2nprmge4  16738  isprm7  16745  3lcm2e6  16769  prmreclem2  16955  prmreclem6  16959  4sqlem11  16993  4sqlem12  16994  prmgaplem7  17095  2expltfac  17130  plusgndxnmulrndx  17341  starvndxnplusgndx  17349  scandxnplusgndx  17361  vscandxnplusgndx  17366  ipndxnplusgndx  17377  tsetndxnplusgndx  17401  plendxnplusgndx  17415  dsndxnplusgndx  17434  slotsdifunifndx  17445  efgredleme  19761  cnfldfunALTOLDOLD  21393  zringndrg  21479  chfacfscmul0  22864  chfacfpmmul0  22868  psmetge0  24322  xmetge0  24354  bl2in  24410  metnrmlem3  24883  iihalf1  24958  iihalf2  24961  pcoass  25057  tcphcphlem1  25269  csbren  25433  trirn  25434  minveclem2  25460  minveclem4  25466  pjthlem1  25471  ovolunlem1a  25531  dyadss  25629  opnmbllem  25636  vitalilem2  25644  vitalilem4  25646  mbfi1fseqlem5  25754  lhop1lem  26052  aaliou3lem2  26385  aaliou3lem8  26387  pilem2  26496  pilem3  26497  pipos  26502  sinhalfpilem  26505  sincosq1lem  26539  sincosq4sgn  26543  tangtx  26547  sinq12gt0  26549  sincos4thpi  26555  tan4thpi  26556  tan4thpiOLD  26557  sincos6thpi  26558  sineq0  26566  cos02pilt1  26568  cosq34lt1  26569  cosordlem  26572  cos0pilt1  26574  tanord1  26579  efif1olem1  26584  efif1olem2  26585  efif1olem4  26587  efif1o  26588  efifo  26589  2irrexpq  26773  cxpcn3lem  26790  root1id  26797  root1eq1  26798  root1cj  26799  cxpeq  26800  2logb9irr  26838  2logb3irr  26840  ang180lem1  26852  ang180lem2  26853  chordthmlem2  26876  1cubrlem  26884  atancj  26953  atantan  26966  atanbndlem  26968  atans2  26974  leibpi  26985  log2tlbnd  26988  log2ublem2  26990  log2ub  26992  divsqrtsumlem  27023  harmonicbnd3  27051  zetacvg  27058  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem6  27077  lgamucov  27081  basellem1  27124  basellem2  27125  basellem3  27126  basellem5  27128  chtdif  27201  ppidif  27206  ppinncl  27217  chtrpcl  27218  ppieq0  27219  ppiltx  27220  ppiublem1  27246  ppiub  27248  chpeq0  27252  chteq0  27253  chtublem  27255  chtub  27256  chpval2  27262  chpub  27264  mersenne  27271  perfectlem1  27273  perfectlem2  27274  dchrptlem1  27308  dchrptlem2  27309  bcmono  27321  bclbnd  27324  bpos1lem  27326  bposlem1  27328  bposlem2  27329  bposlem3  27330  bposlem4  27331  bposlem5  27332  bposlem6  27333  bposlem7  27334  bposlem8  27335  bposlem9  27336  lgslem1  27341  lgsdirprm  27375  gausslemma2dlem0c  27402  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  gausslemma2dlem3  27412  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisen  27423  lgsquadlem1  27424  lgsquadlem2  27425  m1lgs  27432  2lgslem1a1  27433  2lgslem1a2  27434  2lgslem1c  27437  2lgslem4  27450  2sqlem11  27473  2sq2  27477  2sqreultlem  27491  2sqreunnltlem  27494  chebbnd1lem1  27513  chebbnd1lem2  27514  chebbnd1lem3  27515  chebbnd1  27516  chtppilimlem1  27517  chtppilimlem2  27518  chtppilim  27519  chto1ub  27520  chebbnd2  27521  chto1lb  27522  chpchtlim  27523  chpo1ub  27524  chpo1ubb  27525  rplogsumlem1  27528  rplogsumlem2  27529  dchrisumlem2  27534  dchrisumlem3  27535  dchrvmasumiflem1  27545  dchrisum0fno1  27555  dchrisum0re  27557  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2  27562  rplogsum  27571  mulog2sumlem1  27578  mulog2sumlem2  27579  log2sumbnd  27588  selberglem2  27590  selbergb  27593  selberg2b  27596  chpdifbndlem1  27597  logdivbnd  27600  selberg3lem1  27601  selberg3  27603  selberg4lem1  27604  selberg4  27605  pntrmax  27608  pntrsumbnd2  27611  selberg3r  27613  selberg4r  27614  selberg34r  27615  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntpbnd  27632  pntibndlem2  27635  pntibndlem3  27636  pntibnd  27637  pntlemb  27641  pntlemg  27642  pntlemh  27643  pntlemr  27646  pntlemk  27650  pntlemo  27651  pnt2  27657  pnt  27658  ostth2lem1  27662  ostth3  27682  slotsinbpsd  28449  slotslnbpsd  28450  istrkg3ld  28469  tgldimor  28510  trgcgrg  28523  tgcgr4  28539  axlowdimlem6  28962  axlowdimlem16  28972  axlowdimlem17  28973  axlowdim  28976  upgrfi  29108  umgrupgr  29120  umgrislfupgrlem  29139  umgrislfupgr  29140  lfgrnloop  29142  usgruspgr  29197  usgrislfuspgr  29204  lfuhgr1v0e  29271  usgrexmpldifpr  29275  usgrexmplef  29276  nbusgrvtxm1  29396  vdegp1bi  29555  upgrewlkle2  29624  lfgrwlkprop  29705  upgr2pthnlp  29752  usgr2pthlem  29783  pthdlem1  29786  wwlksm1edg  29901  wwlksnextwrd  29917  wwlksnextfun  29918  wwlksnextinj  29919  wwlksnextproplem3  29931  clwlkclwwlklem2a1  30011  clwlkclwwlklem2a2  30012  clwlkclwwlklem2fv1  30014  clwlkclwwlklem2fv2  30015  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwlkclwwlk2  30022  clwlkclwwlkf  30027  clwwlkext2edg  30075  konigsbergiedgw  30267  konigsbergssiedgw  30269  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273  konigsberg  30276  frgrreggt1  30412  ex-pss  30447  ex-res  30460  ex-fv  30462  ex-fl  30466  ex-mod  30468  ex-abs  30474  nrt2irr  30492  ipidsq  30729  minvecolem2  30894  minvecolem4  30899  normlem7  31135  norm-ii-i  31156  norm3lemt  31171  normpar2i  31175  bcsiALT  31198  pjhthlem1  31410  opsqrlem6  32164  cdj3lem1  32453  addltmulALT  32465  nexple  32833  2exple2exp  32834  threehalves  32897  pfx1s2  32923  wrdt2ind  32938  oppgleOLD  32952  cyc3conja  33177  resvplusgOLD  33362  drngidlhash  33462  evl1deg3  33603  rtelextdg2lem  33767  fldext2chn  33769  2sqr3minply  33791  sqsscirc1  33907  dya2iocucvr  34286  omssubadd  34302  oddpwdc  34356  eulerpartlemgc  34364  fibp1  34403  coinfliplem  34481  coinflipspace  34483  ballotlem2  34491  signstfveq0  34592  prodfzo03  34618  hgt750lemd  34663  logdivsqrle  34665  hgt750lem  34666  hgt750lem2  34667  hgt750leme  34673  lfuhgr2  35124  usgrcyclgt2v  35136  acycgr2v  35155  subfacp1lem1  35184  subfacp1lem5  35189  subfacval3  35194  problem2  35671  problem5  35674  circum  35679  nn0prpwlem  36323  dnibndlem10  36488  knoppcnlem2  36495  knoppcnlem4  36497  knoppcnlem10  36503  unbdqndv2lem1  36510  knoppndvlem1  36513  knoppndvlem10  36522  knoppndvlem11  36523  knoppndvlem12  36524  knoppndvlem14  36526  knoppndvlem15  36527  knoppndvlem17  36529  knoppndvlem18  36530  knoppndvlem19  36531  knoppndvlem20  36532  knoppndvlem21  36533  cnndvlem1  36538  taupi  37324  iccioo01  37328  relowlpssretop  37365  sin2h  37617  cos2h  37618  tan2h  37619  poimirlem7  37634  poimirlem9  37636  opnmbllem0  37663  mblfinlem1  37664  mblfinlem2  37665  itg2addnclem  37678  isbnd2  37790  isbnd3  37791  heiborlem7  37824  12gcd5e1  42004  lcm2un  42015  lcmineqlem19  42048  lcmineqlem20  42049  lcmineqlem22  42051  3lexlogpow5ineq2  42056  3lexlogpow5ineq4  42057  3lexlogpow5ineq3  42058  3lexlogpow2ineq1  42059  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1lem1  42063  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p2  42078  aks4d1p3  42079  aks4d1p5  42081  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8  42088  aks4d1p9  42089  posbezout  42101  aks6d1c3  42124  2np3bcnp1  42145  2ap1caineq  42146  aks6d1c6lem4  42174  aks6d1c7lem1  42181  aks6d1c7lem2  42182  2xp3dxp2ge1d  42242  oexpreposd  42357  asin1half  42387  remul02  42435  sn-0ne2  42436  remul01  42437  flt4lem7  42669  rabren3dioph  42826  pellexlem2  42841  pellexlem5  42844  pell14qrgapw  42887  pellfundex  42897  rmspecsqrtnq  42917  jm2.24nn  42971  jm2.17a  42972  jm2.17b  42973  jm2.17c  42974  acongrep  42992  acongeq  42995  jm2.22  43007  jm2.23  43008  jm2.20nn  43009  jm3.1lem2  43030  expdiophlem1  43033  sqrtcval  43654  imo72b2lem0  44178  mnringaddgdOLD  44237  lhe4.4ex1a  44348  isosctrlem1ALT  44954  sineq0ALT  44957  lt3addmuld  45313  suplesup  45350  infleinflem2  45382  infleinf  45383  sumnnodd  45645  0ellimcdiv  45664  sinaover2ne0  45883  stoweidlem13  46028  stoweidlem14  46029  stoweidlem26  46041  stoweidlem49  46064  stoweidlem52  46067  wallispilem4  46083  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem1  46089  stirlinglem3  46091  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem10  46098  stirlinglem11  46099  stirlinglem15  46103  stirlingr  46105  dirker2re  46107  dirkerval2  46109  dirkerre  46110  dirkerper  46111  dirkertrigeqlem1  46113  dirkertrigeqlem3  46115  dirkercncflem1  46118  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem24  46146  fourierdlem43  46165  fourierdlem44  46166  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  fourierdlem66  46187  fourierdlem68  46189  fourierdlem72  46193  fourierdlem76  46197  fourierdlem78  46199  fourierdlem79  46200  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem113  46234  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  etransclem23  46272  salexct2  46354  salexct3  46357  salgencntex  46358  salgensscntex  46359  sge0ad2en  46446  ovnsubaddlem1  46585  smfmullem4  46809  smf2id  46816  2leaddle2  47310  p1lep2  47312  ceil5half3  47342  fmtnoge3  47517  fmtnof1  47522  fmtnoprmfac2lem1  47553  fmtno4prmfac  47559  fmtno4prm  47562  2pwp1prm  47576  31prm  47584  sfprmdvdsmersenne  47590  lighneallem2  47593  lighneallem4a  47595  lighneallem4b  47596  requad01  47608  requad1  47609  requad2  47610  dfodd4  47646  nn0o1gt2ALTV  47681  nnoALTV  47682  nn0oALTV  47683  nn0e  47684  nneven  47685  perfectALTVlem1  47708  perfectALTVlem2  47709  341fppr2  47721  9fppr8  47724  fpprel2  47728  nfermltl2rev  47730  gbowgt5  47749  sbgoldbalt  47768  sgoldbeven3prm  47770  mogoldbb  47772  nnsum3primes4  47775  nnsum3primesgbe  47779  nnsum3primesle9  47781  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  cycl3grtri  47914  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  usgrexmpl2trifr  47996  2ltceilhalf  48015  2tceilhalfelfzo1  48018  gpg5nbgrvtx13starlem2  48028  gpg3nbgrvtx0  48032  gpg3kgrtriexlem1  48039  cznnring  48178  ply1mulgsumlem2  48304  zlmodzxznm  48414  zlmodzxzldeplem  48415  difmodm1lt  48443  nn0eo  48449  flnn0div2ge  48454  rege1logbzge0  48480  fldivexpfllog2  48486  logbpw2m1  48488  fllog2  48489  blenpw2m1  48500  nnpw2blen  48501  nnolog2flm1  48511  blennngt2o2  48513  dig2nn1st  48526  dig2nn0  48532  dig2bits  48535  dignn0flhalflem1  48536  dignn0flhalflem2  48537  dignn0flhalf  48539  nn0sumshdiglemA  48540  ackval42  48617  rrx2xpref1o  48639  itscnhlc0yqe  48680  itsclquadb  48697  2itscp  48702  itscnhlinecirc02p  48706  sepfsepc  48825