Theorem 2re 10681

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 10670	. 2 |- 2 = ( 1 + 1 )
2		1re 9644	. . 3 |- 1 e. RR
3	2, 2	readdcli 9658	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2507	1 |- 2 e. RR

Syntax hints:   e. wcel 1869  (class class class)co 6303   RRcr 9540   1c1 9542   + caddc 9544   2c2 10661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-i2m1 9609  ax-1ne0 9610  ax-rrecex 9613  ax-cnre 9614

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-iota 5563  df-fv 5607  df-ov 6306  df-2 10670

This theorem is referenced by:  2cn  10682  3re  10685  2ne0  10704  3pos  10705  2lt3  10779  1lt3  10780  2lt4  10782  1lt4  10783  2lt5  10786  2lt6  10791  1lt6  10792  2lt7  10797  1lt7  10798  2lt8  10804  1lt8  10805  2lt9  10812  1lt9  10813  2lt10  10821  1lt10  10822  1le2  10825  2rene0  10827  halfre  10830  halfgt0  10832  halflt1  10833  rehalfcl  10841  halfpos2  10844  halfnneg2  10846  addltmul  10850  nominpos  10851  avglt1  10852  avglt2  10853  nn0lele2xi  10924  nn0n0n1ge2b  10935  nn0ge2m1nn  10936  halfnz  11016  uzuzle23  11201  uz3m2nn  11203  2rp  11309  zgt1rpn0n1  11342  fztpval  11859  fzo0to42pr  12001  flhalf  12063  2txmodxeq0  12151  expubnd  12334  expmulnbnd  12405  nn0opthlem2  12456  faclbnd2  12477  faclbnd4lem1  12479  faclbnd5  12484  4bc2eq6  12515  hashfun  12608  hashge2el2dif  12635  hashge2el2difr  12636  wrdlenge2n0  12701  f1oun2prg  12996  2swrd2eqwrdeq  13022  sqrlem7  13306  sqrt4  13330  sqrt2gt1lt2  13332  abstri  13387  sqreulem  13416  amgm2  13426  caucvgrlem  13729  caucvgrlemOLD  13730  iseralt  13744  climcndslem1  13900  climcndslem2  13901  climcnds  13902  geoihalfsum  13931  efcllem  14125  ege2le3  14137  ef01bndlem  14231  cos01bnd  14233  cos2bnd  14235  cos01gt0  14238  sin02gt0  14239  sincos2sgn  14241  sin4lt0  14242  eirrlem  14249  egt2lt3  14251  epos  14252  ene1  14255  sqrt2re  14295  n2dvds1  14347  oexpneg  14361  bitsp1o  14399  bitsfzolem  14400  bitsfzolemOLD  14401  bitsfzo  14402  bitsfi  14404  6gcd4e2  14495  prmn2uzge3  14637  3lcm2e6  14674  oddprm  14758  iserodd  14778  prmreclem2  14854  prmreclem6  14858  4sqlem11  14892  4sqlem12  14893  prmgaplem7  15020  2expltfac  15056  oppgtset  16996  efgredleme  17386  mgpsca  17723  mgptset  17724  mgpds  17726  matplusg  19431  chfacfscmul0  19874  chfacfpmmul0  19878  psmetge0  21320  xmetge0  21351  bl2in  21407  metnrmlem3  21870  metnrmlem3OLD  21885  iihalf1  21951  iihalf2  21953  pcoass  22047  tchcphlem1  22201  csbren  22345  trirn  22346  minveclem2  22360  minveclem4  22366  minveclem2OLD  22372  minveclem4OLD  22378  pjthlem1  22383  ovolunlem1a  22441  dyadss  22544  opnmbllem  22551  vitalilem2  22559  vitalilem4  22561  mbfi1fseqlem5  22669  lhop1lem  22957  aaliou3lem2  23291  aaliou3lem8  23293  pilem2  23399  pilem2OLD  23400  pilem3  23401  pilem3OLD  23402  pipos  23407  sinhalfpilem  23410  sincosq1lem  23444  sincosq4sgn  23448  tangtx  23452  sinq12gt0  23454  sincos4thpi  23460  tan4thpi  23461  sincos6thpi  23462  sineq0  23468  cosordlem  23472  tanord1  23478  efif1olem1  23483  efif1olem2  23484  efif1olem4  23486  efif1o  23487  efifo  23488  cxpcn3lem  23679  root1id  23686  root1eq1  23687  root1cj  23688  cxpeq  23689  logblog  23721  ang180lem1  23730  ang180lem2  23731  chordthmlem2  23751  1cubrlem  23759  atancj  23828  atantan  23841  atanbndlem  23843  atans2  23849  leibpilem1  23858  leibpi  23860  log2tlbnd  23863  log2ublem2  23865  log2ub  23867  divsqrtsumlem  23897  harmonicbnd3  23925  zetacvg  23932  lgamgulmlem2  23947  lgamgulmlem3  23948  lgamgulmlem4  23949  lgamgulmlem6  23951  lgamucov  23955  basellem1  23999  basellem2  24000  basellem3  24001  basellem5  24003  chtdif  24077  ppidif  24082  ppinncl  24093  chtrpcl  24094  ppieq0  24095  ppiltx  24096  ppiublem1  24122  ppiub  24124  chpeq0  24128  chteq0  24129  chtublem  24131  chtub  24132  chpval2  24138  chpub  24140  mersenne  24147  perfectlem1  24149  perfectlem2  24150  dchrptlem1  24184  dchrptlem2  24185  bcmono  24197  bclbnd  24200  bpos1lem  24202  bposlem1  24204  bposlem2  24205  bposlem3  24206  bposlem4  24207  bposlem5  24208  bposlem6  24209  bposlem7  24210  bposlem8  24211  bposlem9  24212  lgslem1  24216  lgsdirprm  24249  lgseisenlem1  24269  lgseisenlem2  24270  lgseisenlem3  24271  lgseisen  24273  lgsquadlem1  24274  lgsquadlem2  24275  m1lgs  24282  2sqlem11  24295  chebbnd1lem1  24299  chebbnd1lem2  24300  chebbnd1lem3  24301  chebbnd1  24302  chtppilimlem1  24303  chtppilimlem2  24304  chtppilim  24305  chto1ub  24306  chebbnd2  24307  chto1lb  24308  chpchtlim  24309  chpo1ub  24310  chpo1ubb  24311  rplogsumlem1  24314  rplogsumlem2  24315  dchrisumlem2  24320  dchrisumlem3  24321  dchrvmasumiflem1  24331  dchrisum0fno1  24341  dchrisum0re  24343  dchrisum0lem1b  24345  dchrisum0lem1  24346  dchrisum0lem2  24348  rplogsum  24357  mulog2sumlem1  24364  mulog2sumlem2  24365  log2sumbnd  24374  selberglem2  24376  selbergb  24379  selberg2b  24382  chpdifbndlem1  24383  logdivbnd  24386  selberg3lem1  24387  selberg3  24389  selberg4lem1  24390  selberg4  24391  pntrmax  24394  pntrsumbnd2  24397  selberg3r  24399  selberg4r  24400  selberg34r  24401  pntrlog2bndlem2  24408  pntrlog2bndlem3  24409  pntrlog2bndlem4  24410  pntrlog2bndlem5  24411  pntrlog2bndlem6  24413  pntrlog2bnd  24414  pntpbnd1a  24415  pntpbnd1  24416  pntpbnd2  24417  pntpbnd  24418  pntibndlem2  24421  pntibndlem3  24422  pntibnd  24423  pntlemb  24427  pntlemg  24428  pntlemh  24429  pntlemr  24432  pntlemk  24436  pntlemo  24437  pnt2  24443  pnt  24444  ostth2lem1  24448  ostth3  24468  istrkg3ld  24501  tgldimor  24538  trgcgrg  24552  tgcgr4  24568  axlowdimlem6  24969  axlowdimlem16  24979  axlowdimlem17  24980  axlowdim  24983  umgrafi  25041  usisuslgra  25084  usgraexmplvtxlem  25114  usgraex2elv  25117  usgraexmpldifpr  25119  constr3lem4  25367  constr3trllem3  25372  constr3pthlem1  25375  constr3pthlem3  25377  wwlkextwrd  25448  wwlkextfun  25449  wwlkextinj  25450  wwlkm1edg  25455  wwlkextproplem3  25463  clwwlkgt0  25491  clwwlkn0  25494  clwlkisclwwlklem2a1  25499  clwlkisclwwlklem2a2  25500  clwlkisclwwlklem2fv1  25502  clwlkisclwwlklem2fv2  25503  clwlkisclwwlklem2a4  25504  clwlkisclwwlklem2a  25505  clwlkisclwwlklem1  25507  clwlkisclwwlk2  25510  clwwlkext2edg  25522  usg2cwwkdifex  25541  clwlkfclwwlk  25564  konigsberg  25707  vdgfrgragt2  25747  extwwlkfablem2  25798  numclwwlkovf2ex  25806  frgrareggt1  25836  frgrareg  25837  frgraregord013  25838  ex-pss  25870  ex-res  25883  ex-fv  25885  ex-fl  25889  nvge0  26295  ipidsq  26341  minvecolem2  26509  minvecolem4  26514  minvecolem2OLD  26519  minvecolem4OLD  26524  normlem7  26761  norm-ii-i  26782  norm3lemt  26797  normpar2i  26801  bcsiALT  26824  pjhthlem1  27036  opsqrlem6  27790  cdj3lem1  28079  addltmulALT  28091  oppgle  28415  resvplusg  28598  sqsscirc1  28716  nexple  28833  dya2iocucvr  29108  omssubadd  29130  omssubaddOLD  29134  oddpwdc  29189  eulerpartlemgc  29197  fibp1  29236  coinfliplem  29313  coinflipspace  29315  ballotlem2  29323  signstfveq0  29468  subfacp1lem1  29904  subfacp1lem5  29909  subfacval3  29914  problem2  30300  problem5  30303  circum  30320  nn0prpwlem  30977  taupi  31682  relowlpssretop  31714  sin2h  31855  cos2h  31856  tan2h  31857  poimirlem7  31867  poimirlem9  31869  opnmbllem0  31896  mblfinlem1  31897  mblfinlem2  31898  itg2addnclem  31913  isbnd2  32035  isbnd3  32036  heiborlem7  32069  rabren3dioph  35583  pellexlem2  35600  pellexlem5  35603  pell14qrgapw  35648  pellfundex  35660  rmspecsqrtnq  35680  jm2.24nn  35735  jm2.17a  35736  jm2.17b  35737  jm2.17c  35738  acongrep  35756  acongeq  35759  jm2.22  35776  jm2.23  35777  jm2.20nn  35778  jm3.1lem2  35799  expdiophlem1  35802  imo72b2lem0  36472  isprm7  36524  lhe4.4ex1a  36542  isosctrlem1ALT  37198  sineq0ALT  37201  lt3addmuld  37367  suplesup  37410  sumnnodd  37536  0ellimcdiv  37556  sinaover2ne0  37569  stoweidlem13  37699  stoweidlem14  37700  stoweidlem26  37712  stoweidlem49  37736  stoweidlem52  37739  wallispilem4  37756  wallispilem5  37757  wallispi  37758  wallispi2lem1  37759  wallispi2lem2  37760  wallispi2  37761  stirlinglem1  37762  stirlinglem3  37764  stirlinglem5  37766  stirlinglem6  37767  stirlinglem7  37768  stirlinglem10  37771  stirlinglem11  37772  stirlinglem15  37776  stirlingr  37778  dirker2re  37780  dirkerval2  37782  dirkerre  37783  dirkerper  37784  dirkertrigeqlem1  37786  dirkertrigeqlem3  37788  dirkercncflem1  37791  dirkercncflem2  37792  dirkercncflem4  37794  fourierdlem24  37819  fourierdlem43  37840  fourierdlem44  37841  fourierdlem57  37853  fourierdlem58  37854  fourierdlem62  37858  fourierdlem66  37862  fourierdlem68  37864  fourierdlem72  37868  fourierdlem76  37872  fourierdlem78  37874  fourierdlem79  37875  fourierdlem94  37890  fourierdlem103  37899  fourierdlem104  37900  fourierdlem111  37907  fourierdlem113  37909  sqwvfoura  37918  sqwvfourb  37919  fourierswlem  37920  fouriersw  37921  etransclem23  37948  sge0ad2en  38067  ovnsubaddlem1  38173  mod2eq1n2dvds  38443  dfodd4  38506  oexpnegALTV  38524  nn0o1gt2ALTV  38541  nnoALTV  38542  nn0oALTV  38543  nn0e  38544  perfectALTVlem1  38561  perfectALTVlem2  38562  gbogt5  38581  sgoldbalt  38600  nnsum3primes4  38601  nnsum3primesgbe  38605  nnsum3primesle9  38607  nnsum4primesodd  38609  nnsum4primesoddALTV  38610  evengpoap3  38612  wtgoldbnnsum4prm  38615  bgoldbnnsum3prm  38617  pfx2  38671  2leaddle2  38739  p1lep2  38741  umgrfi  38850  ausgrumgri  38888  usgruspgr  38898  usgra2pthlem1  38971  plusgndxnmulrndx  39257  cznnring  39262  nn0le2is012  39454  ply1mulgsumlem2  39485  zlmodzxznm  39596  zlmodzxzldeplem  39597  3halfnz  39623  difmodm1lt  39631  nn0o1gt2  39633  nno  39634  nn0o  39635  nn0eo  39641  flnn0div2ge  39646  rege1logbzge0  39676  fldivexpfllog2  39682  logbpw2m1  39684  fllog2  39685  blenpw2m1  39696  nnpw2blen  39697  nnolog2flm1  39707  blennngt2o2  39709  dig2nn1st  39722  dig2nn0  39728  dig2bits  39731  dignn0flhalflem1  39732  dignn0flhalflem2  39733  dignn0flhalf  39735  nn0sumshdiglemA  39736