Theorem 2re 10566

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	|- 2 e. RR

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 10555	. 2 |- 2 = ( 1 + 1 )
2		1re 9545	. . 3 |- 1 e. RR
3	2, 2	readdcli 9559	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2486	1 |- 2 e. RR

Syntax hints:   e. wcel 1842  (class class class)co 6234   RRcr 9441   1c1 9443   + caddc 9445   2c2 10546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-1cn 9500  ax-icn 9501  ax-addcl 9502  ax-addrcl 9503  ax-mulcl 9504  ax-mulrcl 9505  ax-i2m1 9510  ax-1ne0 9511  ax-rrecex 9514  ax-cnre 9515

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-br 4395  df-iota 5489  df-fv 5533  df-ov 6237  df-2 10555

This theorem is referenced by:  2cn  10567  3re  10570  2ne0  10589  3pos  10590  2lt3  10664  1lt3  10665  2lt4  10667  1lt4  10668  2lt5  10671  2lt6  10676  1lt6  10677  2lt7  10682  1lt7  10683  2lt8  10689  1lt8  10690  2lt9  10697  1lt9  10698  2lt10  10706  1lt10  10707  1le2  10710  2rene0  10712  halfre  10715  halfgt0  10717  halflt1  10718  rehalfcl  10726  halfpos2  10729  halfnneg2  10731  addltmul  10735  nominpos  10736  avglt1  10737  avglt2  10738  nn0lele2xi  10809  nn0n0n1ge2b  10821  nn0ge2m1nn  10822  halfnz  10902  uzuzle23  11085  uz3m2nn  11087  2rp  11188  zgt1rpn0n1  11221  fztpval  11713  fzo0to42pr  11851  flhalf  11913  2txmodxeq0  12001  expubnd  12181  expmulnbnd  12252  nn0opthlem2  12303  faclbnd2  12323  faclbnd4lem1  12325  faclbnd5  12330  hashfun  12451  hashge2el2dif  12477  wrdlenge2n0  12537  f1oun2prg  12828  2swrd2eqwrdeq  12854  sqrlem7  13138  sqrt4  13162  sqrt2gt1lt2  13164  abstri  13219  sqreulem  13248  amgm2  13258  caucvgrlem  13551  iseralt  13563  climcndslem1  13719  climcndslem2  13720  climcnds  13721  geoihalfsum  13750  efcllem  13914  ege2le3  13926  ef01bndlem  14020  cos01bnd  14022  cos2bnd  14024  cos01gt0  14027  sin02gt0  14028  sincos2sgn  14030  sin4lt0  14031  eirrlem  14038  egt2lt3  14040  epos  14041  ene1  14044  sqrt2re  14084  n2dvds1  14136  oexpneg  14150  bitsp1o  14184  bitsfzolem  14185  bitsfzo  14186  bitsfi  14188  prmn2uzge3  14338  oddprm  14440  iserodd  14460  prmreclem2  14536  prmreclem6  14540  4sqlem11  14574  4sqlem12  14575  2expltfac  14678  oppgtset  16603  efgredleme  16977  mgpsca  17360  mgptset  17361  mgpds  17363  matplusg  19100  chfacfscmul0  19543  chfacfpmmul0  19547  psmetge0  21000  xmetge0  21031  bl2in  21087  metnrmlem3  21549  iihalf1  21615  iihalf2  21617  pcoass  21708  tchcphlem1  21862  csbren  22010  trirn  22011  minveclem2  22025  minveclem4  22031  pjthlem1  22036  ovolunlem1a  22091  dyadss  22187  opnmbllem  22194  vitalilem2  22202  vitalilem4  22204  mbfi1fseqlem5  22310  lhop1lem  22598  aaliou3lem2  22923  aaliou3lem8  22925  pilem2  23031  pilem3  23032  pipos  23037  sinhalfpilem  23040  sincosq1lem  23074  sincosq4sgn  23078  tangtx  23082  sinq12gt0  23084  sincos4thpi  23090  tan4thpi  23091  sincos6thpi  23092  sineq0  23098  cosordlem  23102  tanord1  23108  efif1olem1  23113  efif1olem2  23114  efif1olem4  23116  efif1o  23117  efifo  23118  cxpcn3lem  23309  root1id  23316  root1eq1  23317  root1cj  23318  cxpeq  23319  logblog  23351  ang180lem1  23360  ang180lem2  23361  chordthmlem2  23381  1cubrlem  23389  atancj  23458  atantan  23471  atanbndlem  23473  atans2  23479  leibpilem1  23488  leibpi  23490  log2tlbnd  23493  log2ublem2  23495  log2ub  23497  divsqrtsumlem  23527  harmonicbnd3  23555  zetacvg  23562  lgamgulmlem2  23577  lgamgulmlem3  23578  lgamgulmlem4  23579  lgamgulmlem6  23581  lgamucov  23585  basellem1  23627  basellem2  23628  basellem3  23629  basellem5  23631  chtdif  23705  ppidif  23710  ppinncl  23721  chtrpcl  23722  ppieq0  23723  ppiltx  23724  ppiublem1  23750  ppiub  23752  chpeq0  23756  chteq0  23757  chtublem  23759  chtub  23760  chpval2  23766  chpub  23768  mersenne  23775  perfectlem1  23777  perfectlem2  23778  dchrptlem1  23812  dchrptlem2  23813  bcmono  23825  bclbnd  23828  bpos1lem  23830  bposlem1  23832  bposlem2  23833  bposlem3  23834  bposlem4  23835  bposlem5  23836  bposlem6  23837  bposlem7  23838  bposlem8  23839  bposlem9  23840  lgslem1  23844  lgsdirprm  23877  lgseisenlem1  23897  lgseisenlem2  23898  lgseisenlem3  23899  lgseisen  23901  lgsquadlem1  23902  lgsquadlem2  23903  m1lgs  23910  2sqlem11  23923  chebbnd1lem1  23927  chebbnd1lem2  23928  chebbnd1lem3  23929  chebbnd1  23930  chtppilimlem1  23931  chtppilimlem2  23932  chtppilim  23933  chto1ub  23934  chebbnd2  23935  chto1lb  23936  chpchtlim  23937  chpo1ub  23938  chpo1ubb  23939  rplogsumlem1  23942  rplogsumlem2  23943  dchrisumlem2  23948  dchrisumlem3  23949  dchrvmasumiflem1  23959  dchrisum0fno1  23969  dchrisum0re  23971  dchrisum0lem1b  23973  dchrisum0lem1  23974  dchrisum0lem2  23976  rplogsum  23985  mulog2sumlem1  23992  mulog2sumlem2  23993  log2sumbnd  24002  selberglem2  24004  selbergb  24007  selberg2b  24010  chpdifbndlem1  24011  logdivbnd  24014  selberg3lem1  24015  selberg3  24017  selberg4lem1  24018  selberg4  24019  pntrmax  24022  pntrsumbnd2  24025  selberg3r  24027  selberg4r  24028  selberg34r  24029  pntrlog2bndlem2  24036  pntrlog2bndlem3  24037  pntrlog2bndlem4  24038  pntrlog2bndlem5  24039  pntrlog2bndlem6  24041  pntrlog2bnd  24042  pntpbnd1a  24043  pntpbnd1  24044  pntpbnd2  24045  pntpbnd  24046  pntibndlem2  24049  pntibndlem3  24050  pntibnd  24051  pntlemb  24055  pntlemg  24056  pntlemh  24057  pntlemr  24060  pntlemk  24064  pntlemo  24065  pnt2  24071  pnt  24072  ostth2lem1  24076  ostth3  24096  istrkg3ld  24129  tgldimor  24166  trgcgrg  24179  axlowdimlem6  24548  axlowdimlem16  24558  axlowdimlem17  24559  axlowdim  24562  umgrafi  24620  usisuslgra  24663  usgraexvlem  24693  usgraex2elv  24696  usgraexmpldifpr  24698  constr3lem4  24945  constr3trllem3  24950  constr3pthlem1  24953  constr3pthlem3  24955  wwlkextwrd  25026  wwlkextfun  25027  wwlkextinj  25028  wwlkm1edg  25033  wwlkextproplem3  25041  clwwlkgt0  25069  clwwlkn0  25072  clwlkisclwwlklem2a1  25077  clwlkisclwwlklem2a2  25078  clwlkisclwwlklem2fv1  25080  clwlkisclwwlklem2fv2  25081  clwlkisclwwlklem2a4  25082  clwlkisclwwlklem2a  25083  clwlkisclwwlklem1  25085  clwlkisclwwlk2  25088  clwwlkext2edg  25100  usg2cwwkdifex  25119  clwlkfclwwlk  25142  konigsberg  25285  vdgfrgragt2  25325  extwwlkfablem2  25376  numclwwlkovf2ex  25384  frgrareggt1  25414  frgrareg  25415  frgraregord013  25416  ex-pss  25447  ex-res  25460  ex-fv  25462  ex-fl  25466  nvge0  25871  ipidsq  25917  minvecolem2  26085  minvecolem4  26090  normlem7  26327  norm-ii-i  26348  norm3lemt  26363  normpar2i  26367  bcsiALT  26390  pjhthlem1  26603  opsqrlem6  27357  cdj3lem1  27646  addltmulALT  27658  oppgle  27973  resvplusg  28156  sqsscirc1  28223  nexple  28337  dya2iocucvr  28612  omssubadd  28628  oddpwdc  28679  eulerpartlemgc  28687  fibp1  28726  coinfliplem  28803  coinflipspace  28805  ballotlem2  28813  signstfveq0  28920  subfacp1lem1  29357  subfacp1lem5  29362  subfacval3  29367  problem2  29753  problem5  29756  circum  29773  4bc2eq6  29821  nn0prpwlem  30538  taupi  31237  sin2h  31398  cos2h  31399  tan2h  31400  opnmbllem0  31403  mblfinlem1  31404  mblfinlem2  31405  itg2addnclem  31420  isbnd2  31542  isbnd3  31543  heiborlem7  31576  rabren3dioph  35091  pellexlem2  35108  pellexlem5  35111  pell14qrgapw  35154  pellfundex  35164  rmspecsqrtnq  35184  jm2.24nn  35239  jm2.17a  35240  jm2.17b  35241  jm2.17c  35242  acongrep  35260  acongeq  35263  jm2.22  35280  jm2.23  35281  jm2.20nn  35282  jm3.1lem2  35303  expdiophlem1  35306  imo72b2lem0  35974  isprm7  36021  3lcm2e6  36048  lhe4.4ex1a  36063  isosctrlem1ALT  36746  sineq0ALT  36749  lt3addmuld  36851  sumnnodd  36986  0ellimcdiv  37005  sinaover2ne0  37018  stoweidlem13  37145  stoweidlem14  37146  stoweidlem26  37158  stoweidlem49  37181  stoweidlem52  37184  wallispilem4  37200  wallispilem5  37201  wallispi  37202  wallispi2lem1  37203  wallispi2lem2  37204  wallispi2  37205  stirlinglem1  37206  stirlinglem3  37208  stirlinglem5  37210  stirlinglem6  37211  stirlinglem7  37212  stirlinglem10  37215  stirlinglem11  37216  stirlinglem15  37220  stirlingr  37222  dirker2re  37224  dirkerval2  37226  dirkerre  37227  dirkerper  37228  dirkertrigeqlem1  37230  dirkertrigeqlem3  37232  dirkercncflem1  37235  dirkercncflem2  37236  dirkercncflem4  37238  fourierdlem24  37263  fourierdlem43  37282  fourierdlem44  37283  fourierdlem57  37296  fourierdlem58  37297  fourierdlem62  37301  fourierdlem66  37305  fourierdlem68  37307  fourierdlem72  37311  fourierdlem76  37315  fourierdlem78  37317  fourierdlem79  37318  fourierdlem94  37333  fourierdlem103  37342  fourierdlem104  37343  fourierdlem111  37350  fourierdlem113  37352  sqwvfoura  37361  sqwvfourb  37362  fourierswlem  37363  fouriersw  37364  etransclem23  37390  mod2eq1n2dvds  37656  dfodd4  37721  oexpnegALTV  37739  nn0o1gt2ALTV  37756  nnoALTV  37757  nn0oALTV  37758  nn0e  37759  perfectALTVlem1  37776  perfectALTVlem2  37777  gbogt5  37796  sgoldbalt  37815  nnsum3primes4  37816  nnsum3primesgbe  37820  nnsum3primesle9  37822  nnsum4primesodd  37824  nnsum4primesoddALTV  37825  evengpoap3  37827  wtgoldbnnsum4prm  37830  bgoldbnnsum3prm  37832  pfx2  37879  2leaddle2  37932  p1lep2  37934  usgra2pthlem1  37962  plusgndxnmulrndx  38250  cznnring  38255  nn0le2is012  38447  ply1mulgsumlem2  38478  zlmodzxznm  38589  zlmodzxzldeplem  38590  3halfnz  38617  difmodm1lt  38625  nn0o1gt2  38627  nno  38628  nn0o  38629  nn0eo  38635  flnn0div2ge  38640  rege1logbzge0  38670  fldivexpfllog2  38676  logbpw2m1  38678  fllog2  38679  blenpw2m1  38690  nnpw2blen  38691  nnolog2flm1  38701  blennngt2o2  38703  dig2nn1st  38716  dig2nn0  38722  dig2bits  38725  dignn0flhalflem1  38726  dignn0flhalflem2  38727  dignn0flhalf  38729  nn0sumshdiglemA  38730