Theorem 2re 12303

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 12291	. 2 ⊢ 2 = (1 + 1)
2		1re 11196	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11212	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2861	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2145  (class class class)co 7400  ℝcr 11087  1c1 11089   + caddc 11091  2c2 12283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-i2m1 11156  ax-1ne0 11157  ax-rrecex 11160  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-iota 6481  df-fv 6533  df-ov 7403  df-2 12291

This theorem is referenced by:  2cnALT  12305  3re  12309  0le2  12331  2lt3  12402  2le3  12403  1lt3  12404  2lt4  12406  1lt4  12407  2lt5  12410  2lt6  12415  1lt6  12416  2lt7  12421  1lt7  12422  2lt8  12428  1lt8  12429  2lt9  12436  1lt9  12437  1le2  12440  2rene0  12442  halfre  12445  halfgt0  12447  halflt1  12449  rehalfcl  12459  halfpos2  12461  halfnneg2  12463  addltmul  12468  nominpos  12469  avglt1  12470  avglt2  12471  div4p1lem1div2  12487  nn0lele2xi  12548  nn0n0n1ge2b  12561  nn0ge2m1nn  12562  nn0le2is012  12648  halfnz  12662  3halfnz  12663  2lt10  12843  1lt10OLD  12845  uzuzle23  12896  uzuzle24  12897  uz3m2nn  12906  2rp  13009  ge2halflem1  13121  xnn0n0n1ge2b  13145  fztpval  13602  fz0to4untppr  13646  fz0to5un2tp  13647  fzo0to42pr  13770  flhalf  13851  fldiv4p1lem1div2  13856  2txmodxeq0  13955  expubnd  14202  expmulnbnd  14259  nn0opthlem2  14293  faclbnd2  14315  faclbnd4lem1  14317  faclbnd5  14322  4bc2eq6  14353  hashgt23el  14449  hashfun  14462  hashge2el2dif  14505  hashge2el2difr  14506  hash3tpde  14518  wrdlenge2n0  14577  f1oun2prg  14942  01sqrexlem7  15287  sqrt4  15311  sqrt2gt1lt2  15313  abstri  15370  sqreulem  15399  amgm2  15409  caucvgrlem  15712  climcndslem1  15891  climcndslem2  15892  climcnds  15893  efcllem  16119  ege2le3  16132  ef01bndlem  16228  cos01bnd  16230  cos2bnd  16232  cos01gt0  16235  sin02gt0  16236  sincos2sgn  16238  sin4lt0  16239  eirrlem  16248  egt2lt3  16250  epos  16251  ene1  16254  sqrt2re  16294  mod2eq1n2dvds  16393  oddge22np1  16395  evennn2n  16397  nn0o1gt2  16427  nno  16428  nn0o  16429  nnoddm1d2  16432  bitsp1o  16479  bitsfzolem  16480  bitsfzo  16481  bitsfi  16483  6gcd4e2  16584  2mulprm  16739  ge2nprmge4  16748  isprm7  16755  3lcm2e6  16779  prmreclem2  16965  prmreclem6  16969  4sqlem11  17003  4sqlem12  17004  prmgaplem7  17105  2expltfac  17140  plusgndxnmulrndx  17338  starvndxnplusgndx  17346  scandxnplusgndx  17358  vscandxnplusgndx  17363  ipndxnplusgndx  17374  tsetndxnplusgndx  17398  plendxnplusgndx  17412  dsndxnplusgndx  17431  slotsdifunifndx  17442  efgredleme  19801  zringndrg  21575  chfacfscmul0  22972  chfacfpmmul0  22976  psmetge0  24426  xmetge0  24458  bl2in  24514  metnrmlem3  24976  iihalf1  25047  iihalf2  25049  pcoass  25140  tcphcphlem1  25351  csbren  25515  trirn  25516  minveclem2  25542  minveclem4  25548  pjthlem1  25553  ovolunlem1a  25612  dyadss  25710  opnmbllem  25717  vitalilem2  25725  vitalilem4  25727  mbfi1fseqlem5  25835  lhop1lem  26129  aaliou3lem2  26461  aaliou3lem8  26463  pilem2  26569  pilem3  26570  2pire  26574  pipos  26577  sinhalfpilem  26582  sincosq1lem  26616  sincosq4sgn  26620  tangtx  26624  sinq12gt0  26626  sincos4thpi  26632  tan4thpi  26633  tan4thpiOLD  26634  sincos6thpi  26635  sineq0  26643  cos02pilt1  26645  cosq34lt1  26646  cosordlem  26649  cos0pilt1  26651  tanord1  26656  efif1olem1  26661  efif1olem2  26662  efif1olem4  26664  efif1o  26665  efifo  26666  2irrexpq  26850  cxpcn3lem  26866  root1id  26873  root1eq1  26874  root1cj  26875  cxpeq  26876  2logb9irr  26914  2logb3irr  26916  ang180lem1  26928  ang180lem2  26929  chordthmlem2  26952  1cubrlem  26960  atancj  27029  atantan  27042  atanbndlem  27044  atans2  27050  leibpi  27061  log2tlbnd  27064  log2ublem2  27066  log2ub  27068  divsqrtsumlem  27098  harmonicbnd3  27126  zetacvg  27133  lgamgulmlem2  27148  lgamgulmlem3  27149  lgamgulmlem4  27150  lgamgulmlem6  27152  lgamucov  27156  basellem1  27199  basellem2  27200  basellem3  27201  basellem5  27203  chtdif  27276  ppidif  27281  ppinncl  27292  chtrpcl  27293  ppieq0  27294  ppiltx  27295  ppiublem1  27320  ppiub  27322  chpeq0  27326  chteq0  27327  chtublem  27329  chtub  27330  chpval2  27336  chpub  27338  mersenne  27345  perfectlem1  27347  perfectlem2  27348  dchrptlem1  27382  dchrptlem2  27383  bcmono  27395  bclbnd  27398  bpos1lem  27400  bposlem1  27402  bposlem2  27403  bposlem3  27404  bposlem4  27405  bposlem5  27406  bposlem6  27407  bposlem7  27408  bposlem8  27409  bposlem9  27410  lgslem1  27415  lgsdirprm  27449  gausslemma2dlem0c  27476  gausslemma2dlem1a  27483  gausslemma2dlem2  27485  gausslemma2dlem3  27486  lgseisenlem1  27493  lgseisenlem2  27494  lgseisenlem3  27495  lgseisen  27497  lgsquadlem1  27498  lgsquadlem2  27499  m1lgs  27506  2lgslem1a1  27507  2lgslem1a2  27508  2lgslem1c  27511  2lgslem4  27524  2sqlem11  27547  2sq2  27551  2sqreultlem  27565  2sqreunnltlem  27568  chebbnd1lem1  27587  chebbnd1lem2  27588  chebbnd1lem3  27589  chebbnd1  27590  chtppilimlem1  27591  chtppilimlem2  27592  chtppilim  27593  chto1ub  27594  chebbnd2  27595  chto1lb  27596  chpchtlim  27597  chpo1ub  27598  chpo1ubb  27599  rplogsumlem1  27602  rplogsumlem2  27603  dchrisumlem2  27608  dchrisumlem3  27609  dchrvmasumiflem1  27619  dchrisum0fno1  27629  dchrisum0re  27631  dchrisum0lem1b  27633  dchrisum0lem1  27634  dchrisum0lem2  27636  rplogsum  27645  mulog2sumlem1  27652  mulog2sumlem2  27653  log2sumbnd  27662  selberglem2  27664  selbergb  27667  selberg2b  27670  chpdifbndlem1  27671  logdivbnd  27674  selberg3lem1  27675  selberg3  27677  selberg4lem1  27678  selberg4  27679  pntrmax  27682  pntrsumbnd2  27685  selberg3r  27687  selberg4r  27688  selberg34r  27689  pntrlog2bndlem2  27696  pntrlog2bndlem3  27697  pntrlog2bndlem4  27698  pntrlog2bndlem5  27699  pntrlog2bndlem6  27701  pntrlog2bnd  27702  pntpbnd1a  27703  pntpbnd1  27704  pntpbnd2  27705  pntpbnd  27706  pntibndlem2  27709  pntibndlem3  27710  pntibnd  27711  pntlemb  27715  pntlemg  27716  pntlemh  27717  pntlemr  27720  pntlemk  27724  pntlemo  27725  pnt2  27731  pnt  27732  ostth2lem1  27736  ostth3  27756  slotsinbpsd  28664  slotslnbpsd  28665  istrkg3ld  28684  tgldimor  28725  trgcgrg  28738  tgcgr4  28754  axlowdimlem6  29202  axlowdimlem16  29212  axlowdimlem17  29213  axlowdim  29216  upgrfi  29346  umgrupgr  29358  umgrislfupgrlem  29377  umgrislfupgr  29378  lfgrnloop  29380  usgruspgr  29435  usgrislfuspgr  29442  lfuhgr1v0e  29509  usgrexmpldifpr  29513  usgrexmplef  29514  nbusgrvtxm1  29634  vdegp1bi  29792  upgrewlkle2  29861  lfgrwlkprop  29940  upgr2pthnlp  29986  usgr2pthlem  30017  pthdlem1  30020  wwlksm1edg  30135  wwlksnextwrd  30151  wwlksnextfun  30152  wwlksnextinj  30153  wwlksnextproplem3  30165  clwlkclwwlklem2a1  30248  clwlkclwwlklem2a2  30249  clwlkclwwlklem2fv1  30251  clwlkclwwlklem2fv2  30252  clwlkclwwlklem2a4  30253  clwlkclwwlklem2a  30254  clwlkclwwlklem2  30256  clwlkclwwlk2  30259  clwlkclwwlkf  30264  clwwlkext2edg  30312  konigsbergiedgw  30504  konigsbergssiedgw  30506  konigsberglem1  30508  konigsberglem2  30509  konigsberglem3  30510  konigsberg  30513  frgrreggt1  30649  ex-pss  30684  ex-res  30697  ex-fv  30699  ex-fl  30703  ex-mod  30705  ex-abs  30711  nrt2irr  30729  ipidsq  30967  minvecolem2  31132  minvecolem4  31137  normlem7  31373  norm-ii-i  31394  norm3lemt  31409  normpar2i  31413  bcsiALT  31436  pjhthlem1  31648  opsqrlem6  32402  cdj3lem1  32691  addltmulALT  32703  nexple  33085  2exple2exp  33086  threehalves  33142  pfx1s2  33167  wrdt2ind  33181  cyc3conja  33385  drngidlhash  33653  evl1deg3  33780  rtelextdg2lem  34028  fldext2chn  34030  constraddcl  34064  iconstr  34068  2sqr3minply  34082  2sqr3nconstr  34083  cos9thpinconstrlem1  34091  cos9thpinconstrlem2  34092  sqsscirc1  34210  dya2iocucvr  34586  omssubadd  34602  oddpwdc  34656  eulerpartlemgc  34664  fibp1  34703  coinfliplem  34781  coinflipspace  34783  ballotlem2  34791  signstfveq0  34876  prodfzo03  34902  hgt750lemd  34947  logdivsqrle  34949  hgt750lem  34950  hgt750lem2  34951  hgt750leme  34957  lfuhgr2  35477  usgrcyclgt2v  35489  acycgr2v  35508  subfacp1lem1  35537  subfacp1lem5  35542  subfacval3  35547  problem2  36024  problem5  36027  circum  36032  nn0prpwlem  36690  dnibndlem10  36933  knoppcnlem2  36940  knoppcnlem4  36942  knoppcnlem10  36948  unbdqndv2lem1  36955  knoppndvlem1  36958  knoppndvlem10  36967  knoppndvlem11  36968  knoppndvlem12  36969  knoppndvlem14  36971  knoppndvlem15  36972  knoppndvlem17  36974  knoppndvlem18  36975  knoppndvlem19  36976  knoppndvlem20  36977  knoppndvlem21  36978  cnndvlem1  36983  taupi  37822  iccioo01  37828  relowlpssretop  37865  sin2h  38116  cos2h  38117  tan2h  38118  poimirlem7  38133  poimirlem9  38135  opnmbllem0  38162  mblfinlem1  38163  mblfinlem2  38164  itg2addnclem  38177  isbnd2  38289  isbnd3  38290  heiborlem7  38323  12gcd5e1  42627  lcm2un  42638  lcmineqlem19  42671  lcmineqlem20  42672  lcmineqlem22  42674  3lexlogpow5ineq2  42679  3lexlogpow5ineq4  42680  3lexlogpow5ineq3  42681  3lexlogpow2ineq1  42682  3lexlogpow2ineq2  42683  3lexlogpow5ineq5  42684  aks4d1lem1  42686  aks4d1p1p3  42693  aks4d1p1p2  42694  aks4d1p1p4  42695  aks4d1p1p6  42697  aks4d1p1p7  42698  aks4d1p1p5  42699  aks4d1p1  42700  aks4d1p2  42701  aks4d1p3  42702  aks4d1p5  42704  aks4d1p6  42705  aks4d1p7d1  42706  aks4d1p7  42707  aks4d1p8  42711  aks4d1p9  42712  posbezout  42724  aks6d1c3  42747  2np3bcnp1  42768  2ap1caineq  42769  aks6d1c6lem4  42797  aks6d1c7lem1  42804  aks6d1c7lem2  42805  oexpreposd  42938  asin1half  42973  remul02  43021  sn-0ne2  43022  remul01  43023  flt4lem7  43248  rabren3dioph  43399  pellexlem2  43414  pellexlem5  43417  pell14qrgapw  43460  pellfundex  43470  rmspecsqrtnq  43490  jm2.24nn  43543  jm2.17a  43544  jm2.17b  43545  jm2.17c  43546  acongrep  43564  acongeq  43567  jm2.22  43579  jm2.23  43580  jm3.1lem2  43602  expdiophlem1  43605  sqrtcval  44224  imo72b2lem0  44748  lhe4.4ex1a  44898  isosctrlem1ALT  45501  sineq0ALT  45504  lt3addmuld  45879  suplesup  45914  infleinflem2  45945  infleinf  45946  sumnnodd  46205  0ellimcdiv  46222  sinaover2ne0  46441  stoweidlem13  46586  stoweidlem14  46587  stoweidlem26  46599  stoweidlem49  46622  stoweidlem52  46625  wallispilem4  46641  wallispilem5  46642  wallispi  46643  wallispi2lem1  46644  wallispi2lem2  46645  wallispi2  46646  stirlinglem1  46647  stirlinglem3  46649  stirlinglem5  46651  stirlinglem6  46652  stirlinglem7  46653  stirlinglem10  46656  stirlinglem11  46657  stirlinglem15  46661  stirlingr  46663  dirker2re  46665  dirkerval2  46667  dirkerre  46668  dirkertrigeqlem1  46671  dirkertrigeqlem3  46673  dirkercncflem1  46676  dirkercncflem4  46679  fourierdlem24  46704  fourierdlem43  46723  fourierdlem44  46724  fourierdlem57  46736  fourierdlem58  46737  fourierdlem62  46741  fourierdlem66  46745  fourierdlem68  46747  fourierdlem72  46751  fourierdlem76  46755  fourierdlem78  46757  fourierdlem79  46758  fourierdlem94  46773  fourierdlem103  46782  fourierdlem104  46783  fourierdlem111  46790  sqwvfoura  46801  sqwvfourb  46802  fourierswlem  46803  fouriersw  46804  etransclem23  46830  salexct2  46912  salexct3  46915  salgencntex  46916  salgensscntex  46917  sge0ad2en  47004  ovnsubaddlem1  47143  smfmullem4  47367  smf2id  47374  nthrucw  47461  goldrarr  47474  goldrapos  47476  2leaddle2  47891  p1lep2  47893  2ltceilhalf  47925  ceilhalfgt1  47926  2tceilhalfelfzo1  47929  rehalfge1  47932  ceilhalfnn  47933  ceil5half3  47939  difmodm1lt  47958  2timesltsq  47971  2timesltsqm1  47972  fmtnoge3  48138  fmtnof1  48143  fmtnoprmfac2lem1  48174  fmtno4prmfac  48180  fmtno4prm  48183  2pwp1prm  48197  31prm  48205  sfprmdvdsmersenne  48211  lighneallem2  48214  lighneallem4a  48216  lighneallem4b  48217  nprmdvdsfacm1lem2  48229  nprmdvdsfacm1lem4  48231  ppivalnnnprmge6  48234  requad01  48242  requad1  48243  requad2  48244  dfodd4  48280  nn0o1gt2ALTV  48315  nnoALTV  48316  nn0oALTV  48317  nn0e  48318  nneven  48319  perfectALTVlem1  48342  perfectALTVlem2  48343  341fppr2  48355  9fppr8  48358  fpprel2  48362  nfermltl2rev  48364  gbowgt5  48383  sbgoldbalt  48402  sgoldbeven3prm  48404  mogoldbb  48406  nnsum3primes4  48409  nnsum3primesgbe  48413  nnsum3primesle9  48415  nnsum4primesodd  48417  nnsum4primesoddALTV  48418  wtgoldbnnsum4prm  48423  bgoldbnnsum3prm  48425  cycl3grtri  48568  usgrexmpl1lem  48642  usgrexmpl2lem  48647  usgrexmpl2nb2  48654  usgrexmpl2nb3  48655  usgrexmpl2nb4  48656  usgrexmpl2nb5  48657  usgrexmpl2trifr  48658  gpgprismgrusgra  48679  gpg5nbgrvtx13starlem2  48693  gpg3nbgrvtx0  48697  gpg3kgrtriexlem1  48704  cznnring  48883  ply1mulgsumlem2  49019  zlmodzxznm  49129  zlmodzxzldeplem  49130  nn0eo  49160  flnn0div2ge  49165  rege1logbzge0  49191  fldivexpfllog2  49197  logbpw2m1  49199  fllog2  49200  blenpw2m1  49211  nnpw2blen  49212  nnolog2flm1  49222  blennngt2o2  49224  dig2nn1st  49237  dig2nn0  49243  dig2bits  49246  dignn0flhalflem1  49247  dignn0flhalflem2  49248  dignn0flhalf  49250  nn0sumshdiglemA  49251  ackval42  49328  rrx2xpref1o  49350  itscnhlc0yqe  49391  itsclquadb  49408  2itscp  49413  itscnhlinecirc02p  49417  sepfsepc  49558