Theorem 2re 10379

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 10368	. 2 |- 2 = ( 1 + 1 )
2		1re 9373	. . 3 |- 1 e. RR
3	2, 2	readdcli 9387	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2503	1 |- 2 e. RR

Syntax hints:   e. wcel 1755  (class class class)co 6080   RRcr 9269   1c1 9271   + caddc 9273   2c2 10359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-i2m1 9338  ax-1ne0 9339  ax-rrecex 9342  ax-cnre 9343

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-2 10368

This theorem is referenced by:  2cn  10380  3re  10383  2ne0  10402  3pos  10403  2lt3  10477  1lt3  10478  2lt4  10480  1lt4  10481  2lt5  10484  2lt6  10489  1lt6  10490  2lt7  10495  1lt7  10496  2lt8  10502  1lt8  10503  2lt9  10510  1lt9  10511  2lt10  10519  1lt10  10520  1le2  10523  2rene0  10525  halfre  10528  halfgt0  10530  halflt1  10531  rehalfcl  10539  halfpos2  10542  halfnneg2  10544  addltmul  10548  nominpos  10549  avglt1  10550  avglt2  10551  nn0lele2xi  10620  nn0n0n1ge2b  10632  halfnz  10708  2eluzge0  10888  2eluzge1  10889  2rp  10984  fztpval  11502  4fvwrd4  11517  fzo0to42pr  11600  flhalf  11658  2txmodxeq0  11743  expubnd  11908  expmulnbnd  11980  nn0opthlem2  12031  faclbnd2  12051  faclbnd4lem1  12053  faclbnd5  12058  hashge2el2dif  12168  hashfun  12183  wrdlenge2n0  12245  f1oun2prg  12511  2swrd2eqwrdeq  12537  sqrlem7  12722  sqr4  12746  sqr2gt1lt2  12748  abstri  12802  sqreulem  12831  amgm2  12841  caucvgrlem  13134  iseralt  13146  climcndslem1  13295  climcndslem2  13296  climcnds  13297  geoihalfsum  13325  efcllem  13346  ege2le3  13358  ef01bndlem  13451  cos01bnd  13453  cos2bnd  13455  cos01gt0  13458  sin02gt0  13459  sincos2sgn  13461  sin4lt0  13462  eirrlem  13469  egt2lt3  13471  epos  13472  sqr2re  13515  n2dvds1  13565  oexpneg  13578  bitsp1o  13612  bitsfzolem  13613  bitsfzo  13614  bitsfi  13616  oddprm  13865  iserodd  13885  prmreclem2  13961  prmreclem6  13965  4sqlem11  13999  4sqlem12  14000  2expltfac  14102  oppgtset  15847  efgredleme  16220  mgpsca  16572  mgptset  16573  mgpds  16575  matplusg  18157  psmetge0  19730  xmetge0  19761  bl2in  19817  metnrmlem3  20279  iihalf1  20345  iihalf2  20347  pcoass  20438  tchcphlem1  20592  csbren  20740  trirn  20741  minveclem2  20755  minveclem4  20761  pjthlem1  20766  ovolunlem1a  20821  dyadss  20916  opnmbllem  20923  vitalilem2  20931  vitalilem4  20933  mbfi1fseqlem5  21039  lhop1lem  21327  aaliou3lem2  21694  aaliou3lem8  21696  pilem2  21802  pilem3  21803  pipos  21808  sinhalfpilem  21810  sincosq1lem  21844  sincosq4sgn  21848  tangtx  21852  sinq12gt0  21854  sincos4thpi  21860  tan4thpi  21861  sincos6thpi  21862  sineq0  21868  cosordlem  21872  tanord1  21878  efif1olem1  21883  efif1olem2  21884  efif1olem4  21886  efif1o  21887  efifo  21888  cxpcn3lem  22070  root1id  22077  root1eq1  22078  root1cj  22079  cxpeq  22080  ang180lem1  22090  ang180lem2  22091  chordthmlem2  22113  1cubrlem  22121  atancj  22190  atantan  22203  atanbndlem  22205  atans2  22211  leibpilem1  22220  leibpi  22222  log2tlbnd  22225  log2ublem2  22227  log2ub  22229  divsqrsumlem  22258  harmonicbnd3  22286  basellem1  22303  basellem2  22304  basellem3  22305  basellem5  22307  chtdif  22381  ppidif  22386  ppinncl  22397  chtrpcl  22398  ppieq0  22399  ppiltx  22400  ppiublem1  22426  ppiub  22428  chpeq0  22432  chteq0  22433  chtublem  22435  chtub  22436  chpval2  22442  chpub  22444  mersenne  22451  perfectlem1  22453  perfectlem2  22454  dchrptlem1  22488  dchrptlem2  22489  bcmono  22501  bclbnd  22504  bpos1lem  22506  bposlem1  22508  bposlem2  22509  bposlem3  22510  bposlem4  22511  bposlem5  22512  bposlem6  22513  bposlem7  22514  bposlem8  22515  bposlem9  22516  lgslem1  22520  lgsdirprm  22553  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem3  22575  lgseisen  22577  lgsquadlem1  22578  lgsquadlem2  22579  m1lgs  22586  2sqlem11  22599  chebbnd1lem1  22603  chebbnd1lem2  22604  chebbnd1lem3  22605  chebbnd1  22606  chtppilimlem1  22607  chtppilimlem2  22608  chtppilim  22609  chto1ub  22610  chebbnd2  22611  chto1lb  22612  chpchtlim  22613  chpo1ub  22614  chpo1ubb  22615  rplogsumlem1  22618  rplogsumlem2  22619  dchrisumlem2  22624  dchrisumlem3  22625  dchrvmasumiflem1  22635  dchrisum0fno1  22645  dchrisum0re  22647  dchrisum0lem1b  22649  dchrisum0lem1  22650  dchrisum0lem2  22652  rplogsum  22661  mulog2sumlem1  22668  mulog2sumlem2  22669  log2sumbnd  22678  selberglem2  22680  selbergb  22683  selberg2b  22686  chpdifbndlem1  22687  logdivbnd  22690  selberg3lem1  22691  selberg3  22693  selberg4lem1  22694  selberg4  22695  pntrmax  22698  pntrsumbnd2  22701  selberg3r  22703  selberg4r  22704  selberg34r  22705  pntrlog2bndlem2  22712  pntrlog2bndlem3  22713  pntrlog2bndlem4  22714  pntrlog2bndlem5  22715  pntrlog2bndlem6  22717  pntrlog2bnd  22718  pntpbnd1a  22719  pntpbnd1  22720  pntpbnd2  22721  pntpbnd  22722  pntibndlem2  22725  pntibndlem3  22726  pntibnd  22727  pntlemb  22731  pntlemg  22732  pntlemh  22733  pntlemr  22736  pntlemk  22740  pntlemo  22741  pnt2  22747  pnt  22748  ostth2lem1  22752  ostth3  22772  tgldimor  22837  trgcgrg  22848  axlowdimlem6  23016  axlowdimlem16  23026  axlowdimlem17  23027  axlowdim  23030  umgrafi  23079  usisuslgra  23109  usgraexvlem  23136  usgraex2elv  23139  usgraexmpldifpr  23141  constr3lem4  23356  constr3trllem3  23361  constr3pthlem1  23364  constr3pthlem3  23366  konigsberg  23431  ex-pss  23458  ex-res  23471  ex-fv  23473  ex-fl  23477  nvge0  23885  ipidsq  23931  minvecolem2  24099  minvecolem4  24104  normlem7  24341  norm-ii-i  24362  norm3lemt  24377  normpar2i  24381  bcsiALT  24404  pjhthlem1  24617  opsqrlem6  25372  cdj3lem1  25661  addltmulALT  25673  oppgle  25937  resvplusg  26155  sqsscirc1  26192  nexple  26302  rnlogblem  26312  dya2iocucvr  26553  oddpwdc  26585  eulerpartlemgc  26593  fibp1  26632  coinfliplem  26709  coinflipspace  26711  ballotlem2  26719  signstfveq0  26826  zetacvg  26849  lgamgulmlem2  26864  lgamgulmlem3  26865  lgamgulmlem4  26866  lgamgulmlem6  26868  lgamucov  26872  subfacp1lem1  26915  subfacp1lem5  26920  subfacval3  26925  problem2  27147  problem5  27150  circum  27166  4bc2eq6  27238  sin2h  28266  cos2h  28267  tan2h  28268  opnmbllem0  28271  mblfinlem1  28272  mblfinlem2  28273  itg2addnclem  28287  nn0prpwlem  28361  isbnd2  28526  isbnd3  28527  heiborlem7  28560  rabren3dioph  28999  pellexlem2  29016  pellexlem5  29019  pell14qrgapw  29062  pellfundex  29072  rmspecsqrnq  29092  jm2.24nn  29147  jm2.17a  29148  jm2.17b  29149  jm2.17c  29150  acongrep  29168  acongeq  29171  jm2.22  29189  jm2.23  29190  jm2.20nn  29191  jm3.1lem2  29212  expdiophlem1  29215  lhe4.4ex1a  29448  stoweidlem13  29654  stoweidlem14  29655  stoweidlem26  29667  stoweidlem49  29690  stoweidlem52  29693  wallispilem4  29709  wallispilem5  29710  wallispi  29711  wallispi2lem1  29712  wallispi2lem2  29713  wallispi2  29714  stirlinglem1  29715  stirlinglem3  29717  stirlinglem5  29719  stirlinglem6  29720  stirlinglem7  29721  stirlinglem10  29724  stirlinglem11  29725  stirlinglem15  29729  stirlingr  29731  2leaddle2  30021  p1lep2  30023  uzuzle23  30039  uz3m2nn  30041  elfzom1elfzo  30063  prmn2uzge3  30095  ccatw2s1p1  30115  usgra2pthlem1  30146  wwlkextwrd  30206  wwlkextfun  30207  wwlkextinj  30208  wwlkm1edg  30213  clwwlkgt0  30280  clwwlkn0  30283  clwlkisclwwlklem2a1  30287  clwlkisclwwlklem2a2  30288  clwlkisclwwlklem2fv1  30290  clwlkisclwwlklem2fv2  30291  clwlkisclwwlklem2a4  30292  clwlkisclwwlklem2a  30293  clwlkisclwwlklem1  30295  clwlkisclwwlk2  30298  clwwlkext2edg  30310  usg2cwwkdifex  30341  clwlkfclwwlk  30363  wwlkextproplem3  30408  vdgfrgragt2  30466  extwwlkfablem1  30513  extwwlkfablem2  30517  numclwwlkovf2ex  30525  frgrareggt1  30555  frgrareg  30556  frgraregord013  30557  nn0le2is012  30597  zlmodzxznm  30748  zlmodzxzldeplem  30749  ene1  30818  isosctrlem1ALT  31372  sineq0ALT  31375  bj-pirp  32108  pirp  35186  taupi  35190