Theorem 2re 12367

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 12356	. 2 ⊢ 2 = (1 + 1)
2		1re 11290	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 11305	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2840	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183  1c1 11185   + caddc 11187  2c2 12348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-2 12356

This theorem is referenced by:  2cnALT  12369  3re  12373  2ne0  12397  3pos  12398  2lt3  12465  1lt3  12466  2lt4  12468  1lt4  12469  2lt5  12472  2lt6  12477  1lt6  12478  2lt7  12483  1lt7  12484  2lt8  12490  1lt8  12491  2lt9  12498  1lt9  12499  1le2  12502  2rene0  12504  halfre  12507  halfgt0  12509  halflt1  12511  rehalfcl  12519  halfpos2  12522  halfnneg2  12524  addltmul  12529  nominpos  12530  avglt1  12531  avglt2  12532  div4p1lem1div2  12548  nn0lele2xi  12608  nn0n0n1ge2b  12621  nn0ge2m1nn  12622  nn0le2is012  12707  halfnz  12721  3halfnz  12722  2lt10  12896  1lt10  12897  eluz4eluz2  12950  uzuzle23  12954  uz3m2nn  12956  2rp  13062  xnn0n0n1ge2b  13194  fztpval  13646  fz0to4untppr  13687  fz0to5un2tp  13688  fzo0to42pr  13803  flhalf  13881  fldiv4p1lem1div2  13886  2txmodxeq0  13982  expubnd  14227  expmulnbnd  14284  nn0opthlem2  14318  faclbnd2  14340  faclbnd4lem1  14342  faclbnd5  14347  4bc2eq6  14378  hashgt23el  14473  hashfun  14486  hashge2el2dif  14529  hashge2el2difr  14530  hash3tpde  14542  wrdlenge2n0  14600  f1oun2prg  14966  01sqrexlem7  15297  sqrt4  15321  sqrt2gt1lt2  15323  abstri  15379  sqreulem  15408  amgm2  15418  caucvgrlem  15721  climcndslem1  15897  climcndslem2  15898  climcnds  15899  efcllem  16125  ege2le3  16138  ef01bndlem  16232  cos01bnd  16234  cos2bnd  16236  cos01gt0  16239  sin02gt0  16240  sincos2sgn  16242  sin4lt0  16243  eirrlem  16252  egt2lt3  16254  epos  16255  ene1  16258  sqrt2re  16298  mod2eq1n2dvds  16395  oddge22np1  16397  evennn2n  16399  nn0o1gt2  16429  nno  16430  nn0o  16431  nnoddm1d2  16434  bitsp1o  16479  bitsfzolem  16480  bitsfzo  16481  bitsfi  16483  6gcd4e2  16585  2mulprm  16740  ge2nprmge4  16748  isprm7  16755  3lcm2e6  16779  prmreclem2  16964  prmreclem6  16968  4sqlem11  17002  4sqlem12  17003  prmgaplem7  17104  2expltfac  17140  plusgndxnmulrndx  17356  starvndxnplusgndx  17364  scandxnplusgndx  17376  vscandxnplusgndx  17381  ipndxnplusgndx  17392  tsetndxnplusgndx  17416  plendxnplusgndx  17430  dsndxnplusgndx  17449  slotsdifunifndx  17460  oppgtsetOLD  19395  efgredleme  19785  mgpscaOLD  20170  mgptsetOLD  20172  mgpdsOLD  20175  rmodislmodOLD  20951  cnfldfunALTOLDOLD  21416  zringndrg  21502  chfacfscmul0  22885  chfacfpmmul0  22889  psmetge0  24343  xmetge0  24375  bl2in  24431  metnrmlem3  24902  iihalf1  24977  iihalf2  24980  pcoass  25076  tcphcphlem1  25288  csbren  25452  trirn  25453  minveclem2  25479  minveclem4  25485  pjthlem1  25490  ovolunlem1a  25550  dyadss  25648  opnmbllem  25655  vitalilem2  25663  vitalilem4  25665  mbfi1fseqlem5  25774  lhop1lem  26072  aaliou3lem2  26403  aaliou3lem8  26405  pilem2  26514  pilem3  26515  pipos  26520  sinhalfpilem  26523  sincosq1lem  26557  sincosq4sgn  26561  tangtx  26565  sinq12gt0  26567  sincos4thpi  26573  tan4thpi  26574  tan4thpiOLD  26575  sincos6thpi  26576  sineq0  26584  cos02pilt1  26586  cosq34lt1  26587  cosordlem  26590  cos0pilt1  26592  tanord1  26597  efif1olem1  26602  efif1olem2  26603  efif1olem4  26605  efif1o  26606  efifo  26607  2irrexpq  26791  cxpcn3lem  26808  root1id  26815  root1eq1  26816  root1cj  26817  cxpeq  26818  2logb9irr  26856  2logb3irr  26858  ang180lem1  26870  ang180lem2  26871  chordthmlem2  26894  1cubrlem  26902  atancj  26971  atantan  26984  atanbndlem  26986  atans2  26992  leibpi  27003  log2tlbnd  27006  log2ublem2  27008  log2ub  27010  divsqrtsumlem  27041  harmonicbnd3  27069  zetacvg  27076  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem4  27093  lgamgulmlem6  27095  lgamucov  27099  basellem1  27142  basellem2  27143  basellem3  27144  basellem5  27146  chtdif  27219  ppidif  27224  ppinncl  27235  chtrpcl  27236  ppieq0  27237  ppiltx  27238  ppiublem1  27264  ppiub  27266  chpeq0  27270  chteq0  27271  chtublem  27273  chtub  27274  chpval2  27280  chpub  27282  mersenne  27289  perfectlem1  27291  perfectlem2  27292  dchrptlem1  27326  dchrptlem2  27327  bcmono  27339  bclbnd  27342  bpos1lem  27344  bposlem1  27346  bposlem2  27347  bposlem3  27348  bposlem4  27349  bposlem5  27350  bposlem6  27351  bposlem7  27352  bposlem8  27353  bposlem9  27354  lgslem1  27359  lgsdirprm  27393  gausslemma2dlem0c  27420  gausslemma2dlem1a  27427  gausslemma2dlem2  27429  gausslemma2dlem3  27430  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisen  27441  lgsquadlem1  27442  lgsquadlem2  27443  m1lgs  27450  2lgslem1a1  27451  2lgslem1a2  27452  2lgslem1c  27455  2lgslem4  27468  2sqlem11  27491  2sq2  27495  2sqreultlem  27509  2sqreunnltlem  27512  chebbnd1lem1  27531  chebbnd1lem2  27532  chebbnd1lem3  27533  chebbnd1  27534  chtppilimlem1  27535  chtppilimlem2  27536  chtppilim  27537  chto1ub  27538  chebbnd2  27539  chto1lb  27540  chpchtlim  27541  chpo1ub  27542  chpo1ubb  27543  rplogsumlem1  27546  rplogsumlem2  27547  dchrisumlem2  27552  dchrisumlem3  27553  dchrvmasumiflem1  27563  dchrisum0fno1  27573  dchrisum0re  27575  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2  27580  rplogsum  27589  mulog2sumlem1  27596  mulog2sumlem2  27597  log2sumbnd  27606  selberglem2  27608  selbergb  27611  selberg2b  27614  chpdifbndlem1  27615  logdivbnd  27618  selberg3lem1  27619  selberg3  27621  selberg4lem1  27622  selberg4  27623  pntrmax  27626  pntrsumbnd2  27629  selberg3r  27631  selberg4r  27632  selberg34r  27633  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntrlog2bnd  27646  pntpbnd1a  27647  pntpbnd1  27648  pntpbnd2  27649  pntpbnd  27650  pntibndlem2  27653  pntibndlem3  27654  pntibnd  27655  pntlemb  27659  pntlemg  27660  pntlemh  27661  pntlemr  27664  pntlemk  27668  pntlemo  27669  pnt2  27675  pnt  27676  ostth2lem1  27680  ostth3  27700  slotsinbpsd  28467  slotslnbpsd  28468  istrkg3ld  28487  tgldimor  28528  trgcgrg  28541  tgcgr4  28557  axlowdimlem6  28980  axlowdimlem16  28990  axlowdimlem17  28991  axlowdim  28994  upgrfi  29126  umgrupgr  29138  umgrislfupgrlem  29157  umgrislfupgr  29158  lfgrnloop  29160  usgruspgr  29215  usgrislfuspgr  29222  lfuhgr1v0e  29289  usgrexmpldifpr  29293  usgrexmplef  29294  nbusgrvtxm1  29414  vdegp1bi  29573  upgrewlkle2  29642  lfgrwlkprop  29723  upgr2pthnlp  29768  usgr2pthlem  29799  pthdlem1  29802  wwlksm1edg  29914  wwlksnextwrd  29930  wwlksnextfun  29931  wwlksnextinj  29932  wwlksnextproplem3  29944  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a2  30025  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlk2  30035  clwlkclwwlkf  30040  clwwlkext2edg  30088  konigsbergiedgw  30280  konigsbergssiedgw  30282  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  konigsberg  30289  frgrreggt1  30425  ex-pss  30460  ex-res  30473  ex-fv  30475  ex-fl  30479  ex-mod  30481  ex-abs  30487  nrt2irr  30505  ipidsq  30742  minvecolem2  30907  minvecolem4  30912  normlem7  31148  norm-ii-i  31169  norm3lemt  31184  normpar2i  31188  bcsiALT  31211  pjhthlem1  31423  opsqrlem6  32177  cdj3lem1  32466  addltmulALT  32478  threehalves  32879  pfx1s2  32905  wrdt2ind  32920  oppgleOLD  32934  cyc3conja  33150  resvplusgOLD  33327  drngidlhash  33427  evl1deg3  33568  rtelextdg2lem  33717  fldext2chn  33719  2sqr3minply  33738  sqsscirc1  33854  nexple  33973  dya2iocucvr  34249  omssubadd  34265  oddpwdc  34319  eulerpartlemgc  34327  fibp1  34366  coinfliplem  34443  coinflipspace  34445  ballotlem2  34453  signstfveq0  34554  prodfzo03  34580  hgt750lemd  34625  logdivsqrle  34627  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  lfuhgr2  35086  usgrcyclgt2v  35099  acycgr2v  35118  subfacp1lem1  35147  subfacp1lem5  35152  subfacval3  35157  problem2  35634  problem5  35637  circum  35642  nn0prpwlem  36288  dnibndlem10  36453  knoppcnlem2  36460  knoppcnlem4  36462  knoppcnlem10  36468  unbdqndv2lem1  36475  knoppndvlem1  36478  knoppndvlem10  36487  knoppndvlem11  36488  knoppndvlem12  36489  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem17  36494  knoppndvlem18  36495  knoppndvlem19  36496  knoppndvlem20  36497  knoppndvlem21  36498  cnndvlem1  36503  taupi  37289  iccioo01  37293  relowlpssretop  37330  sin2h  37570  cos2h  37571  tan2h  37572  poimirlem7  37587  poimirlem9  37589  opnmbllem0  37616  mblfinlem1  37617  mblfinlem2  37618  itg2addnclem  37631  isbnd2  37743  isbnd3  37744  heiborlem7  37777  12gcd5e1  41960  lcm2un  41971  lcmineqlem19  42004  lcmineqlem20  42005  lcmineqlem22  42007  3lexlogpow5ineq2  42012  3lexlogpow5ineq4  42013  3lexlogpow5ineq3  42014  3lexlogpow2ineq1  42015  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  aks4d1lem1  42019  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p2  42034  aks4d1p3  42035  aks4d1p5  42037  aks4d1p6  42038  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8  42044  aks4d1p9  42045  posbezout  42057  aks6d1c3  42080  2np3bcnp1  42101  2ap1caineq  42102  aks6d1c6lem4  42130  aks6d1c7lem1  42137  aks6d1c7lem2  42138  2xp3dxp2ge1d  42198  oexpreposd  42309  asin1half  42339  remul02  42381  sn-0ne2  42382  remul01  42383  flt4lem7  42614  rabren3dioph  42771  pellexlem2  42786  pellexlem5  42789  pell14qrgapw  42832  pellfundex  42842  rmspecsqrtnq  42862  jm2.24nn  42916  jm2.17a  42917  jm2.17b  42918  jm2.17c  42919  acongrep  42937  acongeq  42940  jm2.22  42952  jm2.23  42953  jm2.20nn  42954  jm3.1lem2  42975  expdiophlem1  42978  sqrtcval  43603  imo72b2lem0  44127  mnringaddgdOLD  44187  lhe4.4ex1a  44298  isosctrlem1ALT  44905  sineq0ALT  44908  lt3addmuld  45216  suplesup  45254  infleinflem2  45286  infleinf  45287  sumnnodd  45551  0ellimcdiv  45570  sinaover2ne0  45789  stoweidlem13  45934  stoweidlem14  45935  stoweidlem26  45947  stoweidlem49  45970  stoweidlem52  45973  wallispilem4  45989  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  wallispi2  45994  stirlinglem1  45995  stirlinglem3  45997  stirlinglem5  45999  stirlinglem6  46000  stirlinglem7  46001  stirlinglem10  46004  stirlinglem11  46005  stirlinglem15  46009  stirlingr  46011  dirker2re  46013  dirkerval2  46015  dirkerre  46016  dirkerper  46017  dirkertrigeqlem1  46019  dirkertrigeqlem3  46021  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem24  46052  fourierdlem43  46071  fourierdlem44  46072  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  fourierdlem66  46093  fourierdlem68  46095  fourierdlem72  46099  fourierdlem76  46103  fourierdlem78  46105  fourierdlem79  46106  fourierdlem94  46121  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem113  46140  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  etransclem23  46178  salexct2  46260  salexct3  46263  salgencntex  46264  salgensscntex  46265  sge0ad2en  46352  ovnsubaddlem1  46491  smfmullem4  46715  smf2id  46722  2leaddle2  47213  p1lep2  47215  fmtnoge3  47404  fmtnof1  47409  fmtnoprmfac2lem1  47440  fmtno4prmfac  47446  fmtno4prm  47449  2pwp1prm  47463  31prm  47471  sfprmdvdsmersenne  47477  lighneallem2  47480  lighneallem4a  47482  lighneallem4b  47483  requad01  47495  requad1  47496  requad2  47497  dfodd4  47533  nn0o1gt2ALTV  47568  nnoALTV  47569  nn0oALTV  47570  nn0e  47571  nneven  47572  perfectALTVlem1  47595  perfectALTVlem2  47596  341fppr2  47608  9fppr8  47611  fpprel2  47615  nfermltl2rev  47617  gbowgt5  47636  sbgoldbalt  47655  sgoldbeven3prm  47657  mogoldbb  47659  nnsum3primes4  47662  nnsum3primesgbe  47666  nnsum3primesle9  47668  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  cznnring  47985  ply1mulgsumlem2  48116  zlmodzxznm  48226  zlmodzxzldeplem  48227  difmodm1lt  48256  nn0eo  48262  flnn0div2ge  48267  rege1logbzge0  48293  fldivexpfllog2  48299  logbpw2m1  48301  fllog2  48302  blenpw2m1  48313  nnpw2blen  48314  nnolog2flm1  48324  blennngt2o2  48326  dig2nn1st  48339  dig2nn0  48345  dig2bits  48348  dignn0flhalflem1  48349  dignn0flhalflem2  48350  dignn0flhalf  48352  nn0sumshdiglemA  48353  ackval42  48430  rrx2xpref1o  48452  itscnhlc0yqe  48493  itsclquadb  48510  2itscp  48515  itscnhlinecirc02p  48519  sepfsepc  48607