Theorem 2re 12410

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 12398	. 2 ⊢ 2 = (1 + 1)
2		1re 11301	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11317	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2857	1 ⊢ 2 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7418  ℝcr 11192  1c1 11194   + caddc 11196  2c2 12390

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-i2m1 11261  ax-1ne0 11262  ax-rrecex 11265  ax-cnre 11266

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-ov 7421  df-2 12398

This theorem is used by:  2cnALT  12412  3re  12416  0le2  12438  2lt3  12509  2le3  12510  1lt3  12511  2lt4  12513  1lt4  12514  2lt5  12517  2lt6  12522  1lt6  12523  2lt7  12528  1lt7  12529  2lt8  12535  1lt8  12536  2lt9  12543  1lt9  12544  1le2  12547  2rene0  12549  halfre  12552  halfgt0  12554  halflt1  12556  rehalfcl  12566  halfpos2  12568  halfnneg2  12570  addltmul  12575  nominpos  12576  avglt1  12577  avglt2  12578  div4p1lem1div2  12594  nn0lele2xi  12655  nn0n0n1ge2b  12668  nn0ge2m1nn  12669  nn0le2is012  12756  halfnz  12770  3halfnz  12771  2lt10  12951  1lt10OLD  12953  uzuzle23  13004  uzuzle24  13005  uz3m2nn  13014  2rp  13118  ge2halflem1  13230  xnn0n0n1ge2b  13254  fztpval  13713  fz0to4untppr  13757  fz0to5un2tp  13758  fzo0to42pr  13881  flhalf  13963  fldiv4p1lem1div2  13968  2txmodxeq0  14067  expubnd  14314  expmulnbnd  14372  nn0opthlem2  14406  faclbnd2  14428  faclbnd4lem1  14430  faclbnd5  14435  4bc2eq6  14466  hashgt23el  14562  hashfun  14575  hashge2el2dif  14618  hashge2el2difr  14619  hash3tpde  14631  wrdlenge2n0  14690  f1oun2prg  15061  01sqrexlem7  15408  sqrt4  15432  sqrt2gt1lt2  15434  abstri  15491  sqreulem  15520  amgm2  15530  caucvgrlem  15833  climcndslem1  16011  climcndslem2  16012  climcnds  16013  efcllem  16236  ege2le3  16249  ef01bndlem  16345  cos01bnd  16347  cos2bnd  16349  cos01gt0  16352  sin02gt0  16353  sincos2sgn  16355  sin4lt0  16356  eirrlem  16365  egt2lt3  16367  epos  16368  ene1  16371  sqrt2re  16411  mod2eq1n2dvds  16510  oddge22np1  16512  evennn2n  16514  nn0o1gt2  16544  nno  16545  nn0o  16546  nnoddm1d2  16549  bitsp1o  16596  bitsfzolem  16597  bitsfzo  16598  bitsfi  16600  6gcd4e2  16704  2mulprm  16861  ge2nprmge4  16870  isprm7  16877  3lcm2e6  16901  prmreclem2  17088  prmreclem6  17092  4sqlem11  17126  4sqlem12  17127  prmgaplem7  17228  2expltfac  17263  plusgndxnmulrndx  17461  starvndxnplusgndx  17469  scandxnplusgndx  17481  vscandxnplusgndx  17486  ipndxnplusgndx  17497  tsetndxnplusgndx  17521  plendxnplusgndx  17535  dsndxnplusgndx  17554  slotsdifunifndx  17565  efgredleme  19950  zringndrg  21767  chfacfscmul0  23169  chfacfpmmul0  23173  psmetge0  24624  xmetge0  24656  bl2in  24712  metnrmlem3  25174  iihalf1  25245  iihalf2  25247  pcoass  25338  tcphcphlem1  25549  csbren  25713  trirn  25714  minveclem2  25740  minveclem4  25746  pjthlem1  25751  ovolunlem1a  25810  dyadss  25908  opnmbllem  25915  vitalilem2  25923  vitalilem4  25925  mbfi1fseqlem5  26033  lhop1lem  26326  aaliou3lem2  26663  aaliou3lem8  26665  pilem2  26772  pilem3  26773  2pire  26777  pipos  26780  sinhalfpilem  26785  sincosq1lem  26819  sincosq4sgn  26823  tangtx  26827  sinq12gt0  26829  sincos4thpi  26835  tan4thpi  26836  sincos6thpi  26837  sineq0  26845  cos02pilt1  26847  cosq34lt1  26848  cosordlem  26851  cos0pilt1  26853  tanord1  26858  efif1olem1  26863  efif1olem2  26864  efif1olem4  26866  efif1o  26867  efifo  26868  2irrexpq  27052  cxpcn3lem  27068  root1id  27075  root1eq1  27076  root1cj  27077  cxpeq  27078  2logb9irr  27116  2logb3irr  27118  ang180lem1  27130  ang180lem2  27131  chordthmlem2  27154  1cubrlem  27162  atancj  27231  atantan  27244  atanbndlem  27246  atans2  27252  leibpi  27263  log2tlbnd  27266  log2ublem2  27268  log2ub  27270  divsqrtsumlem  27300  harmonicbnd3  27328  zetacvg  27335  lgamgulmlem2  27350  lgamgulmlem3  27351  lgamgulmlem4  27352  lgamgulmlem6  27354  lgamucov  27358  basellem1  27401  basellem2  27402  basellem3  27403  basellem5  27405  chtdif  27478  ppidif  27483  ppinncl  27494  chtrpcl  27495  ppieq0  27496  ppiltx  27497  ppiublem1  27522  ppiub  27524  chpeq0  27528  chteq0  27529  chtublem  27531  chtub  27532  chpval2  27538  chpub  27540  mersenne  27547  perfectlem1  27549  perfectlem2  27550  dchrptlem1  27584  dchrptlem2  27585  bcmono  27597  bclbnd  27600  bpos1lem  27602  bposlem1  27604  bposlem2  27605  bposlem3  27606  bposlem4  27607  bposlem5  27608  bposlem6  27609  bposlem7  27610  bposlem8  27611  bposlem9  27612  lgslem1  27617  lgsdirprm  27651  gausslemma2dlem0c  27678  gausslemma2dlem1a  27685  gausslemma2dlem2  27687  gausslemma2dlem3  27688  lgseisenlem1  27695  lgseisenlem2  27696  lgseisenlem3  27697  lgseisen  27699  lgsquadlem1  27700  lgsquadlem2  27701  m1lgs  27708  2lgslem1a1  27709  2lgslem1a2  27710  2lgslem1c  27713  2lgslem4  27726  2sqlem11  27749  2sq2  27753  2sqreultlem  27767  2sqreunnltlem  27770  chebbnd1lem1  27789  chebbnd1lem2  27790  chebbnd1lem3  27791  chebbnd1  27792  chtppilimlem1  27793  chtppilimlem2  27794  chtppilim  27795  chto1ub  27796  chebbnd2  27797  chto1lb  27798  chpchtlim  27799  chpo1ub  27800  chpo1ubb  27801  rplogsumlem1  27804  rplogsumlem2  27805  dchrisumlem2  27810  dchrisumlem3  27811  dchrvmasumiflem1  27821  dchrisum0fno1  27831  dchrisum0re  27833  dchrisum0lem1b  27835  dchrisum0lem1  27836  dchrisum0lem2  27838  rplogsum  27847  mulog2sumlem1  27854  mulog2sumlem2  27855  log2sumbnd  27864  selberglem2  27866  selbergb  27869  selberg2b  27872  chpdifbndlem1  27873  logdivbnd  27876  selberg3lem1  27877  selberg3  27879  selberg4lem1  27880  selberg4  27881  pntrmax  27884  pntrsumbnd2  27887  selberg3r  27889  selberg4r  27890  selberg34r  27891  pntrlog2bndlem2  27898  pntrlog2bndlem3  27899  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntrlog2bndlem6  27903  pntrlog2bnd  27904  pntpbnd1a  27905  pntpbnd1  27906  pntpbnd2  27907  pntpbnd  27908  pntibndlem2  27911  pntibndlem3  27912  pntibnd  27913  pntlemb  27917  pntlemg  27918  pntlemh  27919  pntlemr  27922  pntlemk  27926  pntlemo  27927  pnt2  27933  pnt  27934  ostth2lem1  27938  ostth3  27958  flt4lem7  27982  fltoprmlem2  27987  slotsinbpsd  28896  slotslnbpsd  28897  istrkg3ld  28916  tgldimor  28958  trgcgrg  28971  tgcgr4  28987  axlowdimlem6  29518  axlowdimlem16  29528  axlowdimlem17  29529  axlowdim  29532  upgrfi  29662  umgrupgr  29674  umgrislfupgrlem  29693  umgrislfupgr  29694  lfgrnloop  29696  lfuhgr2  29720  usgruspgr  29754  usgrislfuspgr  29761  lfuhgr1v0e  29828  usgrexmpldifpr  29832  usgrexmplef  29833  nbusgrvtxm1  29953  vdegp1bi  30111  upgrewlkle2  30180  lfgrwlkprop  30263  upgr2pthnlp  30311  usgr2pthlem  30342  pthdlem1  30345  wwlksm1edg  30463  wwlksnextwrd  30479  wwlksnextfun  30480  wwlksnextinj  30481  wwlksnextproplem3  30493  clwlkclwwlklem2a1  30576  clwlkclwwlklem2a2  30577  clwlkclwwlklem2fv1  30579  clwlkclwwlklem2fv2  30580  clwlkclwwlklem2a4  30581  clwlkclwwlklem2a  30582  clwlkclwwlklem2  30584  clwlkclwwlk2  30587  clwlkclwwlkf  30592  clwwlkext2edg  30640  konigsbergiedgw  30842  konigsbergssiedgw  30844  konigsberglem1  30846  konigsberglem2  30847  konigsberglem3  30848  konigsberg  30851  frgrreggt1  30987  ex-pss  31022  ex-res  31035  ex-fv  31037  ex-fl  31041  ex-mod  31043  ex-abs  31049  nrt2irr  31067  ipidsq  31305  minvecolem2  31470  minvecolem4  31475  normlem7  31711  norm-ii-i  31732  norm3lemt  31747  normpar2i  31751  bcsiALT  31774  pjhthlem1  31986  opsqrlem6  32740  cdj3lem1  33029  addltmulALT  33041  nexple  33417  2exple2exp  33418  threehalves  33474  pfx1s2  33499  wrdt2ind  33509  cyc3conja  33711  drngidlhash  33976  evl1deg3  34103  rtelextdg2lem  34351  fldext2chn  34353  constraddcl  34387  iconstr  34391  2sqr3minply  34405  2sqr3nconstr  34406  cos9thpinconstrlem1  34414  cos9thpinconstrlem2  34415  sqsscirc1  34533  dya2iocucvr  34909  omssubadd  34925  oddpwdc  34979  eulerpartlemgc  34987  fibp1  35026  coinfliplem  35104  coinflipspace  35106  ballotlem2  35114  signstfveq0  35199  prodfzo03  35225  hgt750lemd  35270  logdivsqrle  35272  hgt750lem  35273  hgt750lem2  35274  hgt750leme  35280  usgrcyclgt2v  35889  acycgr2v  35894  subfacp1lem1  35923  subfacp1lem5  35928  subfacval3  35933  problem2  36410  problem5  36413  circum  36418  nn0prpwlem  37090  dnibndlem10  37333  knoppcnlem2  37340  knoppcnlem4  37342  knoppcnlem10  37348  unbdqndv2lem1  37355  knoppndvlem1  37358  knoppndvlem10  37367  knoppndvlem11  37368  knoppndvlem12  37369  knoppndvlem14  37371  knoppndvlem15  37372  knoppndvlem17  37374  knoppndvlem18  37375  knoppndvlem19  37376  knoppndvlem20  37377  knoppndvlem21  37378  cnndvlem1  37383  taupi  38224  iccioo01  38230  relowlpssretop  38267  sin2h  38513  cos2h  38514  tan2h  38515  poimirlem7  38525  poimirlem9  38527  opnmbllem0  38554  mblfinlem1  38555  mblfinlem2  38556  itg2addnclem  38569  isbnd2  38697  isbnd3  38698  heiborlem7  38731  12gcd5e1  43033  lcm2un  43044  lcmineqlem19  43077  lcmineqlem20  43078  lcmineqlem22  43080  3lexlogpow5ineq2  43085  3lexlogpow5ineq4  43086  3lexlogpow5ineq3  43087  3lexlogpow2ineq1  43088  3lexlogpow2ineq2  43089  3lexlogpow5ineq5  43090  aks4d1lem1  43092  aks4d1p1p3  43099  aks4d1p1p2  43100  aks4d1p1p4  43101  aks4d1p1p6  43103  aks4d1p1p7  43104  aks4d1p1p5  43105  aks4d1p1  43106  aks4d1p2  43107  aks4d1p3  43108  aks4d1p5  43110  aks4d1p6  43111  aks4d1p7d1  43112  aks4d1p7  43113  aks4d1p8  43117  aks4d1p9  43118  posbezout  43130  aks6d1c3  43153  2np3bcnp1  43174  2ap1caineq  43175  aks6d1c6lem4  43203  aks6d1c7lem1  43210  aks6d1c7lem2  43211  oexpreposd  43359  asin1half  43388  remul02  43436  sn-0ne2  43437  remul01  43438  rabren3dioph  43801  pellexlem2  43816  pellexlem5  43819  pell14qrgapw  43862  pellfundex  43872  rmspecsqrtnq  43892  jm2.24nn  43945  jm2.17a  43946  jm2.17b  43947  jm2.17c  43948  acongrep  43966  acongeq  43969  jm2.22  43981  jm2.23  43982  jm3.1lem2  44004  expdiophlem1  44007  sqrtcval  44626  imo72b2lem0  45150  lhe4.4ex1a  45298  isosctrlem1ALT  45901  sineq0ALT  45904  lt3addmuld  46286  suplesup  46320  infleinflem2  46351  infleinf  46352  sumnnodd  46611  0ellimcdiv  46628  sinaover2ne0  46847  stoweidlem13  46992  stoweidlem14  46993  stoweidlem26  47005  stoweidlem49  47028  stoweidlem52  47031  wallispilem4  47047  wallispilem5  47048  wallispi  47049  wallispi2lem1  47050  wallispi2lem2  47051  wallispi2  47052  stirlinglem1  47053  stirlinglem3  47055  stirlinglem5  47057  stirlinglem6  47058  stirlinglem7  47059  stirlinglem10  47062  stirlinglem11  47063  stirlinglem15  47067  stirlingr  47069  dirker2re  47071  dirkerval2  47073  dirkerre  47074  dirkertrigeqlem1  47077  dirkertrigeqlem3  47079  dirkercncflem1  47082  dirkercncflem4  47085  fourierdlem24  47110  fourierdlem43  47129  fourierdlem44  47130  fourierdlem57  47142  fourierdlem58  47143  fourierdlem62  47147  fourierdlem66  47151  fourierdlem68  47153  fourierdlem72  47157  fourierdlem76  47161  fourierdlem78  47163  fourierdlem79  47164  fourierdlem94  47179  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  sqwvfoura  47207  sqwvfourb  47208  fourierswlem  47209  fouriersw  47210  etransclem23  47236  salexct2  47318  salexct3  47321  salgencntex  47322  salgensscntex  47323  sge0ad2en  47410  ovnsubaddlem1  47549  smfmullem4  47773  smf2id  47780  goldrarr  47897  goldrapos  47899  goldratmolem4  47904  goldratval  47905  2leaddle2  48337  p1lep2  48339  2ltceilhalf  48371  ceilhalfgt1  48372  2tceilhalfelfzo1  48375  rehalfge1  48378  ceilhalfnn  48379  ceil5half3  48385  difmodm1lt  48404  2timesltsq  48417  2timesltsqm1  48418  fmtnoge3  48584  fmtnof1  48589  fmtnoprmfac2lem1  48620  fmtno4prmfac  48626  fmtno4prm  48629  2pwp1prm  48643  31prm  48651  sfprmdvdsmersenne  48657  lighneallem2  48660  lighneallem4a  48662  lighneallem4b  48663  nprmdvdsfacm1lem2  48675  nprmdvdsfacm1lem4  48677  ppivalnnnprmge6  48680  requad01  48688  requad1  48689  requad2  48690  dfodd4  48726  nn0o1gt2ALTV  48761  nnoALTV  48762  nn0oALTV  48763  nn0e  48764  nneven  48765  perfectALTVlem1  48788  perfectALTVlem2  48789  341fppr2  48801  9fppr8  48804  fpprel2  48808  nfermltl2rev  48810  gbowgt5  48829  sbgoldbalt  48848  sgoldbeven3prm  48850  mogoldbb  48852  nnsum3primes4  48855  nnsum3primesgbe  48859  nnsum3primesle9  48861  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  wtgoldbnnsum4prm  48869  bgoldbnnsum3prm  48871  cycl3grtri  49014  usgrexmpl1lem  49088  usgrexmpl2lem  49093  usgrexmpl2nb2  49100  usgrexmpl2nb3  49101  usgrexmpl2nb4  49102  usgrexmpl2nb5  49103  usgrexmpl2trifr  49104  gpgprismgrusgra  49125  gpg5nbgrvtx13starlem2  49139  gpg3nbgrvtx0  49143  gpg3kgrtriexlem1  49150  cznnring  49328  ply1mulgsumlem2  49468  zlmodzxznm  49578  zlmodzxzldeplem  49579  nn0eo  49609  flnn0div2ge  49614  rege1logbzge0  49640  fldivexpfllog2  49646  logbpw2m1  49648  fllog2  49649  blenpw2m1  49660  nnpw2blen  49661  nnolog2flm1  49671  blennngt2o2  49673  dig2nn1st  49686  dig2nn0  49692  dig2bits  49695  dignn0flhalflem1  49696  dignn0flhalflem2  49697  dignn0flhalf  49699  nn0sumshdiglemA  49700  ackval42  49777  rrx2xpref1o  49799  itscnhlc0yqe  49840  itsclquadb  49857  2itscp  49862  itscnhlinecirc02p  49866  sepfsepc  50005  2ne3  50911  veronesev2lem  50943  veronesev4lem  50945  veronesev5lem  50946  veronesev6lem  50947  veronesevrowd  50948  veroquadgsumlem  50952