Theorem 2re 10492

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 10481	. 2 |- 2 = ( 1 + 1 )
2		1re 9486	. . 3 |- 1 e. RR
3	2, 2	readdcli 9500	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2535	1 |- 2 e. RR

Syntax hints:   e. wcel 1758  (class class class)co 6190   RRcr 9382   1c1 9384   + caddc 9386   2c2 10472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-i2m1 9451  ax-1ne0 9452  ax-rrecex 9455  ax-cnre 9456

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193  df-2 10481

This theorem is referenced by:  2cn  10493  3re  10496  2ne0  10515  3pos  10516  2lt3  10590  1lt3  10591  2lt4  10593  1lt4  10594  2lt5  10597  2lt6  10602  1lt6  10603  2lt7  10608  1lt7  10609  2lt8  10615  1lt8  10616  2lt9  10623  1lt9  10624  2lt10  10632  1lt10  10633  1le2  10636  2rene0  10638  halfre  10641  halfgt0  10643  halflt1  10644  rehalfcl  10652  halfpos2  10655  halfnneg2  10657  addltmul  10661  nominpos  10662  avglt1  10663  avglt2  10664  nn0lele2xi  10733  nn0n0n1ge2b  10745  halfnz  10821  2eluzge0  11001  2eluzge1  11002  2rp  11097  fztpval  11619  4fvwrd4  11634  fzo0to42pr  11717  flhalf  11775  2txmodxeq0  11860  expubnd  12025  expmulnbnd  12097  nn0opthlem2  12148  faclbnd2  12168  faclbnd4lem1  12170  faclbnd5  12175  hashge2el2dif  12286  hashfun  12301  wrdlenge2n0  12363  f1oun2prg  12629  2swrd2eqwrdeq  12655  sqrlem7  12840  sqr4  12864  sqr2gt1lt2  12866  abstri  12920  sqreulem  12949  amgm2  12959  caucvgrlem  13252  iseralt  13264  climcndslem1  13414  climcndslem2  13415  climcnds  13416  geoihalfsum  13444  efcllem  13465  ege2le3  13477  ef01bndlem  13570  cos01bnd  13572  cos2bnd  13574  cos01gt0  13577  sin02gt0  13578  sincos2sgn  13580  sin4lt0  13581  eirrlem  13588  egt2lt3  13590  epos  13591  sqr2re  13634  n2dvds1  13684  oexpneg  13697  bitsp1o  13731  bitsfzolem  13732  bitsfzo  13733  bitsfi  13735  oddprm  13984  iserodd  14004  prmreclem2  14080  prmreclem6  14084  4sqlem11  14118  4sqlem12  14119  2expltfac  14221  oppgtset  15969  efgredleme  16344  mgpsca  16703  mgptset  16704  mgpds  16706  matplusg  18424  psmetge0  20004  xmetge0  20035  bl2in  20091  metnrmlem3  20553  iihalf1  20619  iihalf2  20621  pcoass  20712  tchcphlem1  20866  csbren  21014  trirn  21015  minveclem2  21029  minveclem4  21035  pjthlem1  21040  ovolunlem1a  21095  dyadss  21190  opnmbllem  21197  vitalilem2  21205  vitalilem4  21207  mbfi1fseqlem5  21313  lhop1lem  21601  aaliou3lem2  21925  aaliou3lem8  21927  pilem2  22033  pilem3  22034  pipos  22039  sinhalfpilem  22041  sincosq1lem  22075  sincosq4sgn  22079  tangtx  22083  sinq12gt0  22085  sincos4thpi  22091  tan4thpi  22092  sincos6thpi  22093  sineq0  22099  cosordlem  22103  tanord1  22109  efif1olem1  22114  efif1olem2  22115  efif1olem4  22117  efif1o  22118  efifo  22119  cxpcn3lem  22301  root1id  22308  root1eq1  22309  root1cj  22310  cxpeq  22311  ang180lem1  22321  ang180lem2  22322  chordthmlem2  22344  1cubrlem  22352  atancj  22421  atantan  22434  atanbndlem  22436  atans2  22442  leibpilem1  22451  leibpi  22453  log2tlbnd  22456  log2ublem2  22458  log2ub  22460  divsqrsumlem  22489  harmonicbnd3  22517  basellem1  22534  basellem2  22535  basellem3  22536  basellem5  22538  chtdif  22612  ppidif  22617  ppinncl  22628  chtrpcl  22629  ppieq0  22630  ppiltx  22631  ppiublem1  22657  ppiub  22659  chpeq0  22663  chteq0  22664  chtublem  22666  chtub  22667  chpval2  22673  chpub  22675  mersenne  22682  perfectlem1  22684  perfectlem2  22685  dchrptlem1  22719  dchrptlem2  22720  bcmono  22732  bclbnd  22735  bpos1lem  22737  bposlem1  22739  bposlem2  22740  bposlem3  22741  bposlem4  22742  bposlem5  22743  bposlem6  22744  bposlem7  22745  bposlem8  22746  bposlem9  22747  lgslem1  22751  lgsdirprm  22784  lgseisenlem1  22804  lgseisenlem2  22805  lgseisenlem3  22806  lgseisen  22808  lgsquadlem1  22809  lgsquadlem2  22810  m1lgs  22817  2sqlem11  22830  chebbnd1lem1  22834  chebbnd1lem2  22835  chebbnd1lem3  22836  chebbnd1  22837  chtppilimlem1  22838  chtppilimlem2  22839  chtppilim  22840  chto1ub  22841  chebbnd2  22842  chto1lb  22843  chpchtlim  22844  chpo1ub  22845  chpo1ubb  22846  rplogsumlem1  22849  rplogsumlem2  22850  dchrisumlem2  22855  dchrisumlem3  22856  dchrvmasumiflem1  22866  dchrisum0fno1  22876  dchrisum0re  22878  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2  22883  rplogsum  22892  mulog2sumlem1  22899  mulog2sumlem2  22900  log2sumbnd  22909  selberglem2  22911  selbergb  22914  selberg2b  22917  chpdifbndlem1  22918  logdivbnd  22921  selberg3lem1  22922  selberg3  22924  selberg4lem1  22925  selberg4  22926  pntrmax  22929  pntrsumbnd2  22932  selberg3r  22934  selberg4r  22935  selberg34r  22936  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntpbnd1a  22950  pntpbnd1  22951  pntpbnd2  22952  pntpbnd  22953  pntibndlem2  22956  pntibndlem3  22957  pntibnd  22958  pntlemb  22962  pntlemg  22963  pntlemh  22964  pntlemr  22967  pntlemk  22971  pntlemo  22972  pnt2  22978  pnt  22979  ostth2lem1  22983  ostth3  23003  tgldimor  23073  trgcgrg  23086  axlowdimlem6  23328  axlowdimlem16  23338  axlowdimlem17  23339  axlowdim  23342  umgrafi  23391  usisuslgra  23421  usgraexvlem  23448  usgraex2elv  23451  usgraexmpldifpr  23453  constr3lem4  23668  constr3trllem3  23673  constr3pthlem1  23676  constr3pthlem3  23678  konigsberg  23743  ex-pss  23770  ex-res  23783  ex-fv  23785  ex-fl  23789  nvge0  24197  ipidsq  24243  minvecolem2  24411  minvecolem4  24416  normlem7  24653  norm-ii-i  24674  norm3lemt  24689  normpar2i  24693  bcsiALT  24716  pjhthlem1  24929  opsqrlem6  25684  cdj3lem1  25973  addltmulALT  25985  oppgle  26248  resvplusg  26435  sqsscirc1  26472  nexple  26582  rnlogblem  26592  dya2iocucvr  26833  oddpwdc  26871  eulerpartlemgc  26879  fibp1  26918  coinfliplem  26995  coinflipspace  26997  ballotlem2  27005  signstfveq0  27112  zetacvg  27135  lgamgulmlem2  27150  lgamgulmlem3  27151  lgamgulmlem4  27152  lgamgulmlem6  27154  lgamucov  27158  subfacp1lem1  27201  subfacp1lem5  27206  subfacval3  27211  problem2  27433  problem5  27436  circum  27453  4bc2eq6  27525  sin2h  28560  cos2h  28561  tan2h  28562  opnmbllem0  28565  mblfinlem1  28566  mblfinlem2  28567  itg2addnclem  28581  nn0prpwlem  28655  isbnd2  28820  isbnd3  28821  heiborlem7  28854  rabren3dioph  29292  pellexlem2  29309  pellexlem5  29312  pell14qrgapw  29355  pellfundex  29365  rmspecsqrnq  29385  jm2.24nn  29440  jm2.17a  29441  jm2.17b  29442  jm2.17c  29443  acongrep  29461  acongeq  29464  jm2.22  29482  jm2.23  29483  jm2.20nn  29484  jm3.1lem2  29505  expdiophlem1  29508  lhe4.4ex1a  29741  stoweidlem13  29946  stoweidlem14  29947  stoweidlem26  29959  stoweidlem49  29982  stoweidlem52  29985  wallispilem4  30001  wallispilem5  30002  wallispi  30003  wallispi2lem1  30004  wallispi2lem2  30005  wallispi2  30006  stirlinglem1  30007  stirlinglem3  30009  stirlinglem5  30011  stirlinglem6  30012  stirlinglem7  30013  stirlinglem10  30016  stirlinglem11  30017  stirlinglem15  30021  stirlingr  30023  2leaddle2  30313  p1lep2  30315  uzuzle23  30331  uz3m2nn  30333  elfzom1elfzo  30355  prmn2uzge3  30387  ccatw2s1p1  30407  usgra2pthlem1  30438  wwlkextwrd  30498  wwlkextfun  30499  wwlkextinj  30500  wwlkm1edg  30505  clwwlkgt0  30572  clwwlkn0  30575  clwlkisclwwlklem2a1  30579  clwlkisclwwlklem2a2  30580  clwlkisclwwlklem2fv1  30582  clwlkisclwwlklem2fv2  30583  clwlkisclwwlklem2a4  30584  clwlkisclwwlklem2a  30585  clwlkisclwwlklem1  30587  clwlkisclwwlk2  30590  clwwlkext2edg  30602  usg2cwwkdifex  30633  clwlkfclwwlk  30655  wwlkextproplem3  30700  vdgfrgragt2  30758  extwwlkfablem1  30805  extwwlkfablem2  30809  numclwwlkovf2ex  30817  frgrareggt1  30847  frgrareg  30848  frgraregord013  30849  nn0le2is012  30906  ply1mulgsumlem2  30987  zlmodzxznm  31146  zlmodzxzldeplem  31147  chfacfscmul0  31312  chfacfpmmul0  31316  ene1  31405  isosctrlem1ALT  31970  sineq0ALT  31973  bj-pirp  32834  pirp  35919  taupi  35923