Theorem 2re 10601

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 10590	. 2 |- 2 = ( 1 + 1 )
2		1re 9591	. . 3 |- 1 e. RR
3	2, 2	readdcli 9605	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2551	1 |- 2 e. RR

Syntax hints:   e. wcel 1767  (class class class)co 6282   RRcr 9487   1c1 9489   + caddc 9491   2c2 10581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-i2m1 9556  ax-1ne0 9557  ax-rrecex 9560  ax-cnre 9561

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285  df-2 10590

This theorem is referenced by:  2cn  10602  3re  10605  2ne0  10624  3pos  10625  2lt3  10699  1lt3  10700  2lt4  10702  1lt4  10703  2lt5  10706  2lt6  10711  1lt6  10712  2lt7  10717  1lt7  10718  2lt8  10724  1lt8  10725  2lt9  10732  1lt9  10733  2lt10  10741  1lt10  10742  1le2  10745  2rene0  10747  halfre  10750  halfgt0  10752  halflt1  10753  rehalfcl  10761  halfpos2  10764  halfnneg2  10766  addltmul  10770  nominpos  10771  avglt1  10772  avglt2  10773  nn0lele2xi  10844  nn0n0n1ge2b  10856  nn0ge2m1nn  10857  halfnz  10935  uzuzle23  11118  uz3m2nn  11120  2eluzge0  11122  2eluzge1  11123  2rp  11221  fztpval  11737  4fvwrd4  11786  fzo0to42pr  11865  flhalf  11925  2txmodxeq0  12010  expubnd  12188  expmulnbnd  12260  nn0opthlem2  12311  faclbnd2  12331  faclbnd4lem1  12333  faclbnd5  12338  hashfun  12455  hashge2el2dif  12481  wrdlenge2n0  12536  ccatw2s1p1  12597  f1oun2prg  12822  2swrd2eqwrdeq  12848  sqrlem7  13039  sqrt4  13063  sqrt2gt1lt2  13065  abstri  13119  sqreulem  13148  amgm2  13158  caucvgrlem  13451  iseralt  13463  climcndslem1  13617  climcndslem2  13618  climcnds  13619  geoihalfsum  13647  efcllem  13668  ege2le3  13680  ef01bndlem  13773  cos01bnd  13775  cos2bnd  13777  cos01gt0  13780  sin02gt0  13781  sincos2sgn  13783  sin4lt0  13784  eirrlem  13791  egt2lt3  13793  epos  13794  sqrt2re  13837  n2dvds1  13887  oexpneg  13901  bitsp1o  13935  bitsfzolem  13936  bitsfzo  13937  bitsfi  13939  prmn2uzge3  14089  oddprm  14191  iserodd  14211  prmreclem2  14287  prmreclem6  14291  4sqlem11  14325  4sqlem12  14326  2expltfac  14428  oppgtset  16179  efgredleme  16554  mgpsca  16935  mgptset  16936  mgpds  16938  matplusg  18680  chfacfscmul0  19123  chfacfpmmul0  19127  psmetge0  20548  xmetge0  20579  bl2in  20635  metnrmlem3  21097  iihalf1  21163  iihalf2  21165  pcoass  21256  tchcphlem1  21410  csbren  21558  trirn  21559  minveclem2  21573  minveclem4  21579  pjthlem1  21584  ovolunlem1a  21639  dyadss  21735  opnmbllem  21742  vitalilem2  21750  vitalilem4  21752  mbfi1fseqlem5  21858  lhop1lem  22146  aaliou3lem2  22470  aaliou3lem8  22472  pilem2  22578  pilem3  22579  pipos  22584  sinhalfpilem  22586  sincosq1lem  22620  sincosq4sgn  22624  tangtx  22628  sinq12gt0  22630  sincos4thpi  22636  tan4thpi  22637  sincos6thpi  22638  sineq0  22644  cosordlem  22648  tanord1  22654  efif1olem1  22659  efif1olem2  22660  efif1olem4  22662  efif1o  22663  efifo  22664  cxpcn3lem  22846  root1id  22853  root1eq1  22854  root1cj  22855  cxpeq  22856  ang180lem1  22866  ang180lem2  22867  chordthmlem2  22889  1cubrlem  22897  atancj  22966  atantan  22979  atanbndlem  22981  atans2  22987  leibpilem1  22996  leibpi  22998  log2tlbnd  23001  log2ublem2  23003  log2ub  23005  divsqrtsumlem  23034  harmonicbnd3  23062  basellem1  23079  basellem2  23080  basellem3  23081  basellem5  23083  chtdif  23157  ppidif  23162  ppinncl  23173  chtrpcl  23174  ppieq0  23175  ppiltx  23176  ppiublem1  23202  ppiub  23204  chpeq0  23208  chteq0  23209  chtublem  23211  chtub  23212  chpval2  23218  chpub  23220  mersenne  23227  perfectlem1  23229  perfectlem2  23230  dchrptlem1  23264  dchrptlem2  23265  bcmono  23277  bclbnd  23280  bpos1lem  23282  bposlem1  23284  bposlem2  23285  bposlem3  23286  bposlem4  23287  bposlem5  23288  bposlem6  23289  bposlem7  23290  bposlem8  23291  bposlem9  23292  lgslem1  23296  lgsdirprm  23329  lgseisenlem1  23349  lgseisenlem2  23350  lgseisenlem3  23351  lgseisen  23353  lgsquadlem1  23354  lgsquadlem2  23355  m1lgs  23362  2sqlem11  23375  chebbnd1lem1  23379  chebbnd1lem2  23380  chebbnd1lem3  23381  chebbnd1  23382  chtppilimlem1  23383  chtppilimlem2  23384  chtppilim  23385  chto1ub  23386  chebbnd2  23387  chto1lb  23388  chpchtlim  23389  chpo1ub  23390  chpo1ubb  23391  rplogsumlem1  23394  rplogsumlem2  23395  dchrisumlem2  23400  dchrisumlem3  23401  dchrvmasumiflem1  23411  dchrisum0fno1  23421  dchrisum0re  23423  dchrisum0lem1b  23425  dchrisum0lem1  23426  dchrisum0lem2  23428  rplogsum  23437  mulog2sumlem1  23444  mulog2sumlem2  23445  log2sumbnd  23454  selberglem2  23456  selbergb  23459  selberg2b  23462  chpdifbndlem1  23463  logdivbnd  23466  selberg3lem1  23467  selberg3  23469  selberg4lem1  23470  selberg4  23471  pntrmax  23474  pntrsumbnd2  23477  selberg3r  23479  selberg4r  23480  selberg34r  23481  pntrlog2bndlem2  23488  pntrlog2bndlem3  23489  pntrlog2bndlem4  23490  pntrlog2bndlem5  23491  pntrlog2bndlem6  23493  pntrlog2bnd  23494  pntpbnd1a  23495  pntpbnd1  23496  pntpbnd2  23497  pntpbnd  23498  pntibndlem2  23501  pntibndlem3  23502  pntibnd  23503  pntlemb  23507  pntlemg  23508  pntlemh  23509  pntlemr  23512  pntlemk  23516  pntlemo  23517  pnt2  23523  pnt  23524  ostth2lem1  23528  ostth3  23548  tgldimor  23618  trgcgrg  23631  axlowdimlem6  23923  axlowdimlem16  23933  axlowdimlem17  23934  axlowdim  23937  umgrafi  23995  usisuslgra  24038  usgraexvlem  24068  usgraex2elv  24071  usgraexmpldifpr  24073  constr3lem4  24320  constr3trllem3  24325  constr3pthlem1  24328  constr3pthlem3  24330  wwlkextwrd  24401  wwlkextfun  24402  wwlkextinj  24403  wwlkm1edg  24408  wwlkextproplem3  24416  clwwlkgt0  24444  clwwlkn0  24447  clwlkisclwwlklem2a1  24452  clwlkisclwwlklem2a2  24453  clwlkisclwwlklem2fv1  24455  clwlkisclwwlklem2fv2  24456  clwlkisclwwlklem2a4  24457  clwlkisclwwlklem2a  24458  clwlkisclwwlklem1  24460  clwlkisclwwlk2  24463  clwwlkext2edg  24475  usg2cwwkdifex  24494  clwlkfclwwlk  24517  konigsberg  24660  vdgfrgragt2  24701  extwwlkfablem1  24748  extwwlkfablem2  24752  numclwwlkovf2ex  24760  frgrareggt1  24790  frgrareg  24791  frgraregord013  24792  ex-pss  24823  ex-res  24836  ex-fv  24838  ex-fl  24842  nvge0  25250  ipidsq  25296  minvecolem2  25464  minvecolem4  25469  normlem7  25706  norm-ii-i  25727  norm3lemt  25742  normpar2i  25746  bcsiALT  25769  pjhthlem1  25982  opsqrlem6  26737  cdj3lem1  27026  addltmulALT  27038  oppgle  27300  resvplusg  27483  sqsscirc1  27523  nexple  27642  rnlogblem  27652  dya2iocucvr  27892  oddpwdc  27930  eulerpartlemgc  27938  fibp1  27977  coinfliplem  28054  coinflipspace  28056  ballotlem2  28064  signstfveq0  28171  zetacvg  28194  lgamgulmlem2  28209  lgamgulmlem3  28210  lgamgulmlem4  28211  lgamgulmlem6  28213  lgamucov  28217  subfacp1lem1  28260  subfacp1lem5  28265  subfacval3  28270  problem2  28492  problem5  28495  circum  28512  4bc2eq6  28584  sin2h  29620  cos2h  29621  tan2h  29622  opnmbllem0  29625  mblfinlem1  29626  mblfinlem2  29627  itg2addnclem  29641  nn0prpwlem  29715  isbnd2  29880  isbnd3  29881  heiborlem7  29914  rabren3dioph  30351  pellexlem2  30368  pellexlem5  30371  pell14qrgapw  30414  pellfundex  30424  rmspecsqrtnq  30444  jm2.24nn  30499  jm2.17a  30500  jm2.17b  30501  jm2.17c  30502  acongrep  30520  acongeq  30523  jm2.22  30541  jm2.23  30542  jm2.20nn  30543  jm3.1lem2  30564  expdiophlem1  30567  isprm7  30795  3lcm2e6  30819  lhe4.4ex1a  30834  lt3addmuld  31078  ioomidp  31118  sumnnodd  31172  lptre2pt  31182  0ellimcdiv  31191  sinaover2ne0  31204  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweidlem13  31313  stoweidlem14  31314  stoweidlem26  31326  stoweidlem49  31349  stoweidlem52  31352  wallispilem4  31368  wallispilem5  31369  wallispi  31370  wallispi2lem1  31371  wallispi2lem2  31372  wallispi2  31373  stirlinglem1  31374  stirlinglem3  31376  stirlinglem5  31378  stirlinglem6  31379  stirlinglem7  31380  stirlinglem10  31383  stirlinglem11  31384  stirlinglem15  31388  stirlingr  31390  dirker2re  31392  dirkerval2  31394  dirkerre  31395  dirkerper  31396  dirkertrigeqlem1  31398  dirkertrigeqlem3  31400  dirkercncflem1  31403  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem24  31431  fourierdlem42  31449  fourierdlem43  31450  fourierdlem44  31451  fourierdlem57  31464  fourierdlem58  31465  fourierdlem62  31469  fourierdlem66  31473  fourierdlem68  31475  fourierdlem72  31479  fourierdlem76  31483  fourierdlem78  31485  fourierdlem79  31486  fourierdlem83  31490  fourierdlem87  31494  fourierdlem94  31501  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  sqwvfoura  31529  sqwvfourb  31530  fourierswlem  31531  fouriersw  31532  2leaddle2  31789  p1lep2  31791  usgra2pthlem1  31822  nn0le2is012  32021  ply1mulgsumlem2  32060  zlmodzxznm  32179  zlmodzxzldeplem  32180  ene1  32249  isosctrlem1ALT  32814  sineq0ALT  32817  bj-pirp  33680  pirp  36765  taupi  36769