Theorem 2re 10626

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 10615	. 2 |- 2 = ( 1 + 1 )
2		1re 9612	. . 3 |- 1 e. RR
3	2, 2	readdcli 9626	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2541	1 |- 2 e. RR

Syntax hints:   e. wcel 1819  (class class class)co 6296   RRcr 9508   1c1 9510   + caddc 9512   2c2 10606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-i2m1 9577  ax-1ne0 9578  ax-rrecex 9581  ax-cnre 9582

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-iota 5557  df-fv 5602  df-ov 6299  df-2 10615

This theorem is referenced by:  2cn  10627  3re  10630  2ne0  10649  3pos  10650  2lt3  10724  1lt3  10725  2lt4  10727  1lt4  10728  2lt5  10731  2lt6  10736  1lt6  10737  2lt7  10742  1lt7  10743  2lt8  10749  1lt8  10750  2lt9  10757  1lt9  10758  2lt10  10766  1lt10  10767  1le2  10770  2rene0  10772  halfre  10775  halfgt0  10777  halflt1  10778  rehalfcl  10786  halfpos2  10789  halfnneg2  10791  addltmul  10795  nominpos  10796  avglt1  10797  avglt2  10798  nn0lele2xi  10869  nn0n0n1ge2b  10881  nn0ge2m1nn  10882  halfnz  10962  uzuzle23  11146  uz3m2nn  11148  2rp  11250  fztpval  11766  fzo0to42pr  11903  flhalf  11964  2txmodxeq0  12049  expubnd  12228  expmulnbnd  12300  nn0opthlem2  12351  faclbnd2  12371  faclbnd4lem1  12373  faclbnd5  12378  hashfun  12498  hashge2el2dif  12524  wrdlenge2n0  12584  f1oun2prg  12876  2swrd2eqwrdeq  12902  sqrlem7  13093  sqrt4  13117  sqrt2gt1lt2  13119  abstri  13174  sqreulem  13203  amgm2  13213  caucvgrlem  13506  iseralt  13518  climcndslem1  13672  climcndslem2  13673  climcnds  13674  geoihalfsum  13702  efcllem  13824  ege2le3  13836  ef01bndlem  13930  cos01bnd  13932  cos2bnd  13934  cos01gt0  13937  sin02gt0  13938  sincos2sgn  13940  sin4lt0  13941  eirrlem  13948  egt2lt3  13950  epos  13951  sqrt2re  13994  n2dvds1  14046  oexpneg  14060  bitsp1o  14094  bitsfzolem  14095  bitsfzo  14096  bitsfi  14098  prmn2uzge3  14248  oddprm  14350  iserodd  14370  prmreclem2  14446  prmreclem6  14450  4sqlem11  14484  4sqlem12  14485  2expltfac  14588  oppgtset  16513  efgredleme  16887  mgpsca  17274  mgptset  17275  mgpds  17277  matplusg  19042  chfacfscmul0  19485  chfacfpmmul0  19489  psmetge0  20941  xmetge0  20972  bl2in  21028  metnrmlem3  21490  iihalf1  21556  iihalf2  21558  pcoass  21649  tchcphlem1  21803  csbren  21951  trirn  21952  minveclem2  21966  minveclem4  21972  pjthlem1  21977  ovolunlem1a  22032  dyadss  22128  opnmbllem  22135  vitalilem2  22143  vitalilem4  22145  mbfi1fseqlem5  22251  lhop1lem  22539  aaliou3lem2  22864  aaliou3lem8  22866  pilem2  22972  pilem3  22973  pipos  22978  sinhalfpilem  22981  sincosq1lem  23015  sincosq4sgn  23019  tangtx  23023  sinq12gt0  23025  sincos4thpi  23031  tan4thpi  23032  sincos6thpi  23033  sineq0  23039  cosordlem  23043  tanord1  23049  efif1olem1  23054  efif1olem2  23055  efif1olem4  23057  efif1o  23058  efifo  23059  cxpcn3lem  23246  root1id  23253  root1eq1  23254  root1cj  23255  cxpeq  23256  ang180lem1  23266  ang180lem2  23267  chordthmlem2  23289  1cubrlem  23297  atancj  23366  atantan  23379  atanbndlem  23381  atans2  23387  leibpilem1  23396  leibpi  23398  log2tlbnd  23401  log2ublem2  23403  log2ub  23405  divsqrtsumlem  23434  harmonicbnd3  23462  basellem1  23479  basellem2  23480  basellem3  23481  basellem5  23483  chtdif  23557  ppidif  23562  ppinncl  23573  chtrpcl  23574  ppieq0  23575  ppiltx  23576  ppiublem1  23602  ppiub  23604  chpeq0  23608  chteq0  23609  chtublem  23611  chtub  23612  chpval2  23618  chpub  23620  mersenne  23627  perfectlem1  23629  perfectlem2  23630  dchrptlem1  23664  dchrptlem2  23665  bcmono  23677  bclbnd  23680  bpos1lem  23682  bposlem1  23684  bposlem2  23685  bposlem3  23686  bposlem4  23687  bposlem5  23688  bposlem6  23689  bposlem7  23690  bposlem8  23691  bposlem9  23692  lgslem1  23696  lgsdirprm  23729  lgseisenlem1  23749  lgseisenlem2  23750  lgseisenlem3  23751  lgseisen  23753  lgsquadlem1  23754  lgsquadlem2  23755  m1lgs  23762  2sqlem11  23775  chebbnd1lem1  23779  chebbnd1lem2  23780  chebbnd1lem3  23781  chebbnd1  23782  chtppilimlem1  23783  chtppilimlem2  23784  chtppilim  23785  chto1ub  23786  chebbnd2  23787  chto1lb  23788  chpchtlim  23789  chpo1ub  23790  chpo1ubb  23791  rplogsumlem1  23794  rplogsumlem2  23795  dchrisumlem2  23800  dchrisumlem3  23801  dchrvmasumiflem1  23811  dchrisum0fno1  23821  dchrisum0re  23823  dchrisum0lem1b  23825  dchrisum0lem1  23826  dchrisum0lem2  23828  rplogsum  23837  mulog2sumlem1  23844  mulog2sumlem2  23845  log2sumbnd  23854  selberglem2  23856  selbergb  23859  selberg2b  23862  chpdifbndlem1  23863  logdivbnd  23866  selberg3lem1  23867  selberg3  23869  selberg4lem1  23870  selberg4  23871  pntrmax  23874  pntrsumbnd2  23877  selberg3r  23879  selberg4r  23880  selberg34r  23881  pntrlog2bndlem2  23888  pntrlog2bndlem3  23889  pntrlog2bndlem4  23890  pntrlog2bndlem5  23891  pntrlog2bndlem6  23893  pntrlog2bnd  23894  pntpbnd1a  23895  pntpbnd1  23896  pntpbnd2  23897  pntpbnd  23898  pntibndlem2  23901  pntibndlem3  23902  pntibnd  23903  pntlemb  23907  pntlemg  23908  pntlemh  23909  pntlemr  23912  pntlemk  23916  pntlemo  23917  pnt2  23923  pnt  23924  ostth2lem1  23928  ostth3  23948  tgldimor  24018  trgcgrg  24031  axlowdimlem6  24376  axlowdimlem16  24386  axlowdimlem17  24387  axlowdim  24390  umgrafi  24448  usisuslgra  24491  usgraexvlem  24521  usgraex2elv  24524  usgraexmpldifpr  24526  constr3lem4  24773  constr3trllem3  24778  constr3pthlem1  24781  constr3pthlem3  24783  wwlkextwrd  24854  wwlkextfun  24855  wwlkextinj  24856  wwlkm1edg  24861  wwlkextproplem3  24869  clwwlkgt0  24897  clwwlkn0  24900  clwlkisclwwlklem2a1  24905  clwlkisclwwlklem2a2  24906  clwlkisclwwlklem2fv1  24908  clwlkisclwwlklem2fv2  24909  clwlkisclwwlklem2a4  24910  clwlkisclwwlklem2a  24911  clwlkisclwwlklem1  24913  clwlkisclwwlk2  24916  clwwlkext2edg  24928  usg2cwwkdifex  24947  clwlkfclwwlk  24970  konigsberg  25113  vdgfrgragt2  25153  extwwlkfablem2  25204  numclwwlkovf2ex  25212  frgrareggt1  25242  frgrareg  25243  frgraregord013  25244  ex-pss  25275  ex-res  25288  ex-fv  25290  ex-fl  25294  nvge0  25703  ipidsq  25749  minvecolem2  25917  minvecolem4  25922  normlem7  26159  norm-ii-i  26180  norm3lemt  26195  normpar2i  26199  bcsiALT  26222  pjhthlem1  26435  opsqrlem6  27190  cdj3lem1  27479  addltmulALT  27491  oppgle  27793  resvplusg  27976  sqsscirc1  28043  nexple  28158  rnlogblem  28168  dya2iocucvr  28416  omssubadd  28432  oddpwdc  28468  eulerpartlemgc  28476  fibp1  28515  coinfliplem  28592  coinflipspace  28594  ballotlem2  28602  signstfveq0  28709  zetacvg  28732  lgamgulmlem2  28747  lgamgulmlem3  28748  lgamgulmlem4  28749  lgamgulmlem6  28751  lgamucov  28755  subfacp1lem1  28798  subfacp1lem5  28803  subfacval3  28808  problem2  29195  problem5  29198  circum  29215  4bc2eq6  29287  sin2h  30207  cos2h  30208  tan2h  30209  opnmbllem0  30212  mblfinlem1  30213  mblfinlem2  30214  itg2addnclem  30228  nn0prpwlem  30302  isbnd2  30441  isbnd3  30442  heiborlem7  30475  rabren3dioph  30911  pellexlem2  30928  pellexlem5  30931  pell14qrgapw  30974  pellfundex  30984  rmspecsqrtnq  31004  jm2.24nn  31059  jm2.17a  31060  jm2.17b  31061  jm2.17c  31062  acongrep  31080  acongeq  31083  jm2.22  31099  jm2.23  31100  jm2.20nn  31101  jm3.1lem2  31122  expdiophlem1  31125  isprm7  31354  3lcm2e6  31381  lhe4.4ex1a  31396  lt3addmuld  31662  sumnnodd  31797  0ellimcdiv  31816  sinaover2ne0  31829  stoweidlem13  31956  stoweidlem14  31957  stoweidlem26  31969  stoweidlem49  31992  stoweidlem52  31995  wallispilem4  32011  wallispilem5  32012  wallispi  32013  wallispi2lem1  32014  wallispi2lem2  32015  wallispi2  32016  stirlinglem1  32017  stirlinglem3  32019  stirlinglem5  32021  stirlinglem6  32022  stirlinglem7  32023  stirlinglem10  32026  stirlinglem11  32027  stirlinglem15  32031  stirlingr  32033  dirker2re  32035  dirkerval2  32037  dirkerre  32038  dirkerper  32039  dirkertrigeqlem1  32041  dirkertrigeqlem3  32043  dirkercncflem1  32046  dirkercncflem2  32047  dirkercncflem4  32049  fourierdlem24  32074  fourierdlem43  32093  fourierdlem44  32094  fourierdlem57  32107  fourierdlem58  32108  fourierdlem62  32112  fourierdlem66  32116  fourierdlem68  32118  fourierdlem72  32122  fourierdlem76  32126  fourierdlem78  32128  fourierdlem79  32129  fourierdlem94  32144  fourierdlem103  32153  fourierdlem104  32154  fourierdlem111  32161  fourierdlem113  32163  sqwvfoura  32172  sqwvfourb  32173  fourierswlem  32174  fouriersw  32175  etransclem23  32201  pfx2  32488  2leaddle2  32542  p1lep2  32544  usgra2pthlem1  32573  plusgndxnmulrndx  32861  cznnring  32866  nn0le2is012  33058  ply1mulgsumlem2  33089  zlmodzxznm  33200  zlmodzxzldeplem  33201  ene1  33270  isosctrlem1ALT  33835  sineq0ALT  33838  taupi  37799  imo72b2lem0  38083