Theorem 2re 12236

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 12225	. 2 ⊢ 2 = (1 + 1)
2		1re 11150	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11165	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2824	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043  1c1 11045   + caddc 11047  2c2 12217

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rrecex 11116  ax-cnre 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-2 12225

This theorem is referenced by:  2cnALT  12238  3re  12242  3pos  12267  2lt3  12329  1lt3  12330  2lt4  12332  1lt4  12333  2lt5  12336  2lt6  12341  1lt6  12342  2lt7  12347  1lt7  12348  2lt8  12354  1lt8  12355  2lt9  12362  1lt9  12363  1le2  12366  2rene0  12368  halfre  12371  halfgt0  12373  halflt1  12375  rehalfcl  12385  halfpos2  12387  halfnneg2  12389  addltmul  12394  nominpos  12395  avglt1  12396  avglt2  12397  div4p1lem1div2  12413  nn0lele2xi  12474  nn0n0n1ge2b  12487  nn0ge2m1nn  12488  nn0le2is012  12574  halfnz  12588  3halfnz  12589  2lt10  12763  1lt10  12764  uzuzle23  12819  uzuzle24  12820  uz3m2nn  12829  2rp  12932  ge2halflem1  13044  xnn0n0n1ge2b  13068  fztpval  13523  fz0to4untppr  13567  fz0to5un2tp  13568  fzo0to42pr  13690  flhalf  13768  fldiv4p1lem1div2  13773  2txmodxeq0  13872  expubnd  14119  expmulnbnd  14176  nn0opthlem2  14210  faclbnd2  14232  faclbnd4lem1  14234  faclbnd5  14239  4bc2eq6  14270  hashgt23el  14365  hashfun  14378  hashge2el2dif  14421  hashge2el2difr  14422  hash3tpde  14434  wrdlenge2n0  14493  f1oun2prg  14859  01sqrexlem7  15190  sqrt4  15214  sqrt2gt1lt2  15216  abstri  15273  sqreulem  15302  amgm2  15312  caucvgrlem  15615  climcndslem1  15791  climcndslem2  15792  climcnds  15793  efcllem  16019  ege2le3  16032  ef01bndlem  16128  cos01bnd  16130  cos2bnd  16132  cos01gt0  16135  sin02gt0  16136  sincos2sgn  16138  sin4lt0  16139  eirrlem  16148  egt2lt3  16150  epos  16151  ene1  16154  sqrt2re  16194  mod2eq1n2dvds  16293  oddge22np1  16295  evennn2n  16297  nn0o1gt2  16327  nno  16328  nn0o  16329  nnoddm1d2  16332  bitsp1o  16379  bitsfzolem  16380  bitsfzo  16381  bitsfi  16383  6gcd4e2  16484  2mulprm  16639  ge2nprmge4  16647  isprm7  16654  3lcm2e6  16678  prmreclem2  16864  prmreclem6  16868  4sqlem11  16902  4sqlem12  16903  prmgaplem7  17004  2expltfac  17039  plusgndxnmulrndx  17236  starvndxnplusgndx  17244  scandxnplusgndx  17256  vscandxnplusgndx  17261  ipndxnplusgndx  17272  tsetndxnplusgndx  17296  plendxnplusgndx  17310  dsndxnplusgndx  17329  slotsdifunifndx  17340  efgredleme  19649  zringndrg  21354  chfacfscmul0  22721  chfacfpmmul0  22725  psmetge0  24176  xmetge0  24208  bl2in  24264  metnrmlem3  24726  iihalf1  24801  iihalf2  24804  pcoass  24900  tcphcphlem1  25111  csbren  25275  trirn  25276  minveclem2  25302  minveclem4  25308  pjthlem1  25313  ovolunlem1a  25373  dyadss  25471  opnmbllem  25478  vitalilem2  25486  vitalilem4  25488  mbfi1fseqlem5  25596  lhop1lem  25894  aaliou3lem2  26227  aaliou3lem8  26229  pilem2  26338  pilem3  26339  pipos  26344  sinhalfpilem  26348  sincosq1lem  26382  sincosq4sgn  26386  tangtx  26390  sinq12gt0  26392  sincos4thpi  26398  tan4thpi  26399  tan4thpiOLD  26400  sincos6thpi  26401  sineq0  26409  cos02pilt1  26411  cosq34lt1  26412  cosordlem  26415  cos0pilt1  26417  tanord1  26422  efif1olem1  26427  efif1olem2  26428  efif1olem4  26430  efif1o  26431  efifo  26432  2irrexpq  26616  cxpcn3lem  26633  root1id  26640  root1eq1  26641  root1cj  26642  cxpeq  26643  2logb9irr  26681  2logb3irr  26683  ang180lem1  26695  ang180lem2  26696  chordthmlem2  26719  1cubrlem  26727  atancj  26796  atantan  26809  atanbndlem  26811  atans2  26817  leibpi  26828  log2tlbnd  26831  log2ublem2  26833  log2ub  26835  divsqrtsumlem  26866  harmonicbnd3  26894  zetacvg  26901  lgamgulmlem2  26916  lgamgulmlem3  26917  lgamgulmlem4  26918  lgamgulmlem6  26920  lgamucov  26924  basellem1  26967  basellem2  26968  basellem3  26969  basellem5  26971  chtdif  27044  ppidif  27049  ppinncl  27060  chtrpcl  27061  ppieq0  27062  ppiltx  27063  ppiublem1  27089  ppiub  27091  chpeq0  27095  chteq0  27096  chtublem  27098  chtub  27099  chpval2  27105  chpub  27107  mersenne  27114  perfectlem1  27116  perfectlem2  27117  dchrptlem1  27151  dchrptlem2  27152  bcmono  27164  bclbnd  27167  bpos1lem  27169  bposlem1  27171  bposlem2  27172  bposlem3  27173  bposlem4  27174  bposlem5  27175  bposlem6  27176  bposlem7  27177  bposlem8  27178  bposlem9  27179  lgslem1  27184  lgsdirprm  27218  gausslemma2dlem0c  27245  gausslemma2dlem1a  27252  gausslemma2dlem2  27254  gausslemma2dlem3  27255  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgseisen  27266  lgsquadlem1  27267  lgsquadlem2  27268  m1lgs  27275  2lgslem1a1  27276  2lgslem1a2  27277  2lgslem1c  27280  2lgslem4  27293  2sqlem11  27316  2sq2  27320  2sqreultlem  27334  2sqreunnltlem  27337  chebbnd1lem1  27356  chebbnd1lem2  27357  chebbnd1lem3  27358  chebbnd1  27359  chtppilimlem1  27360  chtppilimlem2  27361  chtppilim  27362  chto1ub  27363  chebbnd2  27364  chto1lb  27365  chpchtlim  27366  chpo1ub  27367  chpo1ubb  27368  rplogsumlem1  27371  rplogsumlem2  27372  dchrisumlem2  27377  dchrisumlem3  27378  dchrvmasumiflem1  27388  dchrisum0fno1  27398  dchrisum0re  27400  dchrisum0lem1b  27402  dchrisum0lem1  27403  dchrisum0lem2  27405  rplogsum  27414  mulog2sumlem1  27421  mulog2sumlem2  27422  log2sumbnd  27431  selberglem2  27433  selbergb  27436  selberg2b  27439  chpdifbndlem1  27440  logdivbnd  27443  selberg3lem1  27444  selberg3  27446  selberg4lem1  27447  selberg4  27448  pntrmax  27451  pntrsumbnd2  27454  selberg3r  27456  selberg4r  27457  selberg34r  27458  pntrlog2bndlem2  27465  pntrlog2bndlem3  27466  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  pntrlog2bndlem6  27470  pntrlog2bnd  27471  pntpbnd1a  27472  pntpbnd1  27473  pntpbnd2  27474  pntpbnd  27475  pntibndlem2  27478  pntibndlem3  27479  pntibnd  27480  pntlemb  27484  pntlemg  27485  pntlemh  27486  pntlemr  27489  pntlemk  27493  pntlemo  27494  pnt2  27500  pnt  27501  ostth2lem1  27505  ostth3  27525  slotsinbpsd  28344  slotslnbpsd  28345  istrkg3ld  28364  tgldimor  28405  trgcgrg  28418  tgcgr4  28434  axlowdimlem6  28850  axlowdimlem16  28860  axlowdimlem17  28861  axlowdim  28864  upgrfi  28994  umgrupgr  29006  umgrislfupgrlem  29025  umgrislfupgr  29026  lfgrnloop  29028  usgruspgr  29083  usgrislfuspgr  29090  lfuhgr1v0e  29157  usgrexmpldifpr  29161  usgrexmplef  29162  nbusgrvtxm1  29282  vdegp1bi  29441  upgrewlkle2  29510  lfgrwlkprop  29589  upgr2pthnlp  29635  usgr2pthlem  29666  pthdlem1  29669  wwlksm1edg  29784  wwlksnextwrd  29800  wwlksnextfun  29801  wwlksnextinj  29802  wwlksnextproplem3  29814  clwlkclwwlklem2a1  29894  clwlkclwwlklem2a2  29895  clwlkclwwlklem2fv1  29897  clwlkclwwlklem2fv2  29898  clwlkclwwlklem2a4  29899  clwlkclwwlklem2a  29900  clwlkclwwlklem2  29902  clwlkclwwlk2  29905  clwlkclwwlkf  29910  clwwlkext2edg  29958  konigsbergiedgw  30150  konigsbergssiedgw  30152  konigsberglem1  30154  konigsberglem2  30155  konigsberglem3  30156  konigsberg  30159  frgrreggt1  30295  ex-pss  30330  ex-res  30343  ex-fv  30345  ex-fl  30349  ex-mod  30351  ex-abs  30357  nrt2irr  30375  ipidsq  30612  minvecolem2  30777  minvecolem4  30782  normlem7  31018  norm-ii-i  31039  norm3lemt  31054  normpar2i  31058  bcsiALT  31081  pjhthlem1  31293  opsqrlem6  32047  cdj3lem1  32336  addltmulALT  32348  nexple  32742  2exple2exp  32743  threehalves  32808  pfx1s2  32833  wrdt2ind  32848  cyc3conja  33087  drngidlhash  33378  evl1deg3  33520  rtelextdg2lem  33689  fldext2chn  33691  constraddcl  33725  iconstr  33729  2sqr3minply  33743  2sqr3nconstr  33744  cos9thpinconstrlem1  33752  cos9thpinconstrlem2  33753  sqsscirc1  33871  dya2iocucvr  34248  omssubadd  34264  oddpwdc  34318  eulerpartlemgc  34326  fibp1  34365  coinfliplem  34443  coinflipspace  34445  ballotlem2  34453  signstfveq0  34541  prodfzo03  34567  hgt750lemd  34612  logdivsqrle  34614  hgt750lem  34615  hgt750lem2  34616  hgt750leme  34622  lfuhgr2  35079  usgrcyclgt2v  35091  acycgr2v  35110  subfacp1lem1  35139  subfacp1lem5  35144  subfacval3  35149  problem2  35626  problem5  35629  circum  35634  nn0prpwlem  36283  dnibndlem10  36448  knoppcnlem2  36455  knoppcnlem4  36457  knoppcnlem10  36463  unbdqndv2lem1  36470  knoppndvlem1  36473  knoppndvlem10  36482  knoppndvlem11  36483  knoppndvlem12  36484  knoppndvlem14  36486  knoppndvlem15  36487  knoppndvlem17  36489  knoppndvlem18  36490  knoppndvlem19  36491  knoppndvlem20  36492  knoppndvlem21  36493  cnndvlem1  36498  taupi  37284  iccioo01  37288  relowlpssretop  37325  sin2h  37577  cos2h  37578  tan2h  37579  poimirlem7  37594  poimirlem9  37596  opnmbllem0  37623  mblfinlem1  37624  mblfinlem2  37625  itg2addnclem  37638  isbnd2  37750  isbnd3  37751  heiborlem7  37784  12gcd5e1  41964  lcm2un  41975  lcmineqlem19  42008  lcmineqlem20  42009  lcmineqlem22  42011  3lexlogpow5ineq2  42016  3lexlogpow5ineq4  42017  3lexlogpow5ineq3  42018  3lexlogpow2ineq1  42019  3lexlogpow2ineq2  42020  3lexlogpow5ineq5  42021  aks4d1lem1  42023  aks4d1p1p3  42030  aks4d1p1p2  42031  aks4d1p1p4  42032  aks4d1p1p6  42034  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p1  42037  aks4d1p2  42038  aks4d1p3  42039  aks4d1p5  42041  aks4d1p6  42042  aks4d1p7d1  42043  aks4d1p7  42044  aks4d1p8  42048  aks4d1p9  42049  posbezout  42061  aks6d1c3  42084  2np3bcnp1  42105  2ap1caineq  42106  aks6d1c6lem4  42134  aks6d1c7lem1  42141  aks6d1c7lem2  42142  oexpreposd  42283  asin1half  42318  remul02  42366  sn-0ne2  42367  remul01  42368  flt4lem7  42620  rabren3dioph  42776  pellexlem2  42791  pellexlem5  42794  pell14qrgapw  42837  pellfundex  42847  rmspecsqrtnq  42867  jm2.24nn  42921  jm2.17a  42922  jm2.17b  42923  jm2.17c  42924  acongrep  42942  acongeq  42945  jm2.22  42957  jm2.23  42958  jm2.20nn  42959  jm3.1lem2  42980  expdiophlem1  42983  sqrtcval  43603  imo72b2lem0  44127  lhe4.4ex1a  44291  isosctrlem1ALT  44896  sineq0ALT  44899  lt3addmuld  45272  suplesup  45308  infleinflem2  45340  infleinf  45341  sumnnodd  45601  0ellimcdiv  45620  sinaover2ne0  45839  stoweidlem13  45984  stoweidlem14  45985  stoweidlem26  45997  stoweidlem49  46020  stoweidlem52  46023  wallispilem4  46039  wallispilem5  46040  wallispi  46041  wallispi2lem1  46042  wallispi2lem2  46043  wallispi2  46044  stirlinglem1  46045  stirlinglem3  46047  stirlinglem5  46049  stirlinglem6  46050  stirlinglem7  46051  stirlinglem10  46054  stirlinglem11  46055  stirlinglem15  46059  stirlingr  46061  dirker2re  46063  dirkerval2  46065  dirkerre  46066  dirkerper  46067  dirkertrigeqlem1  46069  dirkertrigeqlem3  46071  dirkercncflem1  46074  dirkercncflem2  46075  dirkercncflem4  46077  fourierdlem24  46102  fourierdlem43  46121  fourierdlem44  46122  fourierdlem57  46134  fourierdlem58  46135  fourierdlem62  46139  fourierdlem66  46143  fourierdlem68  46145  fourierdlem72  46149  fourierdlem76  46153  fourierdlem78  46155  fourierdlem79  46156  fourierdlem94  46171  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fourierdlem113  46190  sqwvfoura  46199  sqwvfourb  46200  fourierswlem  46201  fouriersw  46202  etransclem23  46228  salexct2  46310  salexct3  46313  salgencntex  46314  salgensscntex  46315  sge0ad2en  46402  ovnsubaddlem1  46541  smfmullem4  46765  smf2id  46772  2leaddle2  47272  p1lep2  47274  2ltceilhalf  47302  ceilhalfgt1  47303  2tceilhalfelfzo1  47306  rehalfge1  47309  ceilhalfnn  47310  ceil5half3  47314  difmodm1lt  47333  fmtnoge3  47504  fmtnof1  47509  fmtnoprmfac2lem1  47540  fmtno4prmfac  47546  fmtno4prm  47549  2pwp1prm  47563  31prm  47571  sfprmdvdsmersenne  47577  lighneallem2  47580  lighneallem4a  47582  lighneallem4b  47583  requad01  47595  requad1  47596  requad2  47597  dfodd4  47633  nn0o1gt2ALTV  47668  nnoALTV  47669  nn0oALTV  47670  nn0e  47671  nneven  47672  perfectALTVlem1  47695  perfectALTVlem2  47696  341fppr2  47708  9fppr8  47711  fpprel2  47715  nfermltl2rev  47717  gbowgt5  47736  sbgoldbalt  47755  sgoldbeven3prm  47757  mogoldbb  47759  nnsum3primes4  47762  nnsum3primesgbe  47766  nnsum3primesle9  47768  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  cycl3grtri  47919  usgrexmpl1lem  47985  usgrexmpl2lem  47990  usgrexmpl2nb2  47997  usgrexmpl2nb3  47998  usgrexmpl2nb4  47999  usgrexmpl2nb5  48000  usgrexmpl2trifr  48001  gpgprismgrusgra  48022  gpg5nbgrvtx13starlem2  48036  gpg3nbgrvtx0  48040  gpg3kgrtriexlem1  48047  cznnring  48223  ply1mulgsumlem2  48349  zlmodzxznm  48459  zlmodzxzldeplem  48460  nn0eo  48490  flnn0div2ge  48495  rege1logbzge0  48521  fldivexpfllog2  48527  logbpw2m1  48529  fllog2  48530  blenpw2m1  48541  nnpw2blen  48542  nnolog2flm1  48552  blennngt2o2  48554  dig2nn1st  48567  dig2nn0  48573  dig2bits  48576  dignn0flhalflem1  48577  dignn0flhalflem2  48578  dignn0flhalf  48580  nn0sumshdiglemA  48581  ackval42  48658  rrx2xpref1o  48680  itscnhlc0yqe  48721  itsclquadb  48738  2itscp  48743  itscnhlinecirc02p  48747  sepfsepc  48889