Theorem 2re 10679

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 10668	. 2 |- 2 = ( 1 + 1 )
2		1re 9642	. . 3 |- 1 e. RR
3	2, 2	readdcli 9656	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2525	1 |- 2 e. RR

Syntax hints:   e. wcel 1887  (class class class)co 6290   RRcr 9538   1c1 9540   + caddc 9542   2c2 10659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-i2m1 9607  ax-1ne0 9608  ax-rrecex 9611  ax-cnre 9612

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-iota 5546  df-fv 5590  df-ov 6293  df-2 10668

This theorem is referenced by:  2cn  10680  3re  10683  2ne0  10702  3pos  10703  2lt3  10777  1lt3  10778  2lt4  10780  1lt4  10781  2lt5  10784  2lt6  10789  1lt6  10790  2lt7  10795  1lt7  10796  2lt8  10802  1lt8  10803  2lt9  10810  1lt9  10811  2lt10  10819  1lt10  10820  1le2  10823  2rene0  10825  halfre  10828  halfgt0  10830  halflt1  10831  rehalfcl  10839  halfpos2  10842  halfnneg2  10844  addltmul  10848  nominpos  10849  avglt1  10850  avglt2  10851  nn0lele2xi  10922  nn0n0n1ge2b  10933  nn0ge2m1nn  10934  halfnz  11014  uzuzle23  11199  uz3m2nn  11201  2rp  11307  zgt1rpn0n1  11340  fztpval  11857  fzo0to42pr  12000  flhalf  12062  2txmodxeq0  12150  expubnd  12333  expmulnbnd  12404  nn0opthlem2  12455  faclbnd2  12476  faclbnd4lem1  12478  faclbnd5  12483  4bc2eq6  12514  hashfun  12609  hashge2el2dif  12637  hashge2el2difr  12638  wrdlenge2n0  12703  f1oun2prg  13002  2swrd2eqwrdeq  13028  sqrlem7  13312  sqrt4  13336  sqrt2gt1lt2  13338  abstri  13393  sqreulem  13422  amgm2  13432  caucvgrlem  13736  caucvgrlemOLD  13737  iseralt  13751  climcndslem1  13907  climcndslem2  13908  climcnds  13909  geoihalfsum  13938  efcllem  14132  ege2le3  14144  ef01bndlem  14238  cos01bnd  14240  cos2bnd  14242  cos01gt0  14245  sin02gt0  14246  sincos2sgn  14248  sin4lt0  14249  eirrlem  14256  egt2lt3  14258  epos  14259  ene1  14262  sqrt2re  14302  n2dvds1  14354  oexpneg  14368  bitsp1o  14406  bitsfzolem  14407  bitsfzolemOLD  14408  bitsfzo  14409  bitsfi  14411  6gcd4e2  14502  prmn2uzge3  14644  3lcm2e6  14681  oddprm  14765  iserodd  14785  prmreclem2  14861  prmreclem6  14865  4sqlem11  14899  4sqlem12  14900  prmgaplem7  15027  2expltfac  15063  oppgtset  17003  efgredleme  17393  mgpsca  17730  mgptset  17731  mgpds  17733  matplusg  19439  chfacfscmul0  19882  chfacfpmmul0  19886  psmetge0  21328  xmetge0  21359  bl2in  21415  metnrmlem3  21878  metnrmlem3OLD  21893  iihalf1  21959  iihalf2  21961  pcoass  22055  tchcphlem1  22209  csbren  22353  trirn  22354  minveclem2  22368  minveclem4  22374  minveclem2OLD  22380  minveclem4OLD  22386  pjthlem1  22391  ovolunlem1a  22449  dyadss  22552  opnmbllem  22559  vitalilem2  22567  vitalilem4  22569  mbfi1fseqlem5  22677  lhop1lem  22965  aaliou3lem2  23299  aaliou3lem8  23301  pilem2  23407  pilem2OLD  23408  pilem3  23409  pilem3OLD  23410  pipos  23415  sinhalfpilem  23418  sincosq1lem  23452  sincosq4sgn  23456  tangtx  23460  sinq12gt0  23462  sincos4thpi  23468  tan4thpi  23469  sincos6thpi  23470  sineq0  23476  cosordlem  23480  tanord1  23486  efif1olem1  23491  efif1olem2  23492  efif1olem4  23494  efif1o  23495  efifo  23496  cxpcn3lem  23687  root1id  23694  root1eq1  23695  root1cj  23696  cxpeq  23697  logblog  23729  ang180lem1  23738  ang180lem2  23739  chordthmlem2  23759  1cubrlem  23767  atancj  23836  atantan  23849  atanbndlem  23851  atans2  23857  leibpilem1  23866  leibpi  23868  log2tlbnd  23871  log2ublem2  23873  log2ub  23875  divsqrtsumlem  23905  harmonicbnd3  23933  zetacvg  23940  lgamgulmlem2  23955  lgamgulmlem3  23956  lgamgulmlem4  23957  lgamgulmlem6  23959  lgamucov  23963  basellem1  24007  basellem2  24008  basellem3  24009  basellem5  24011  chtdif  24085  ppidif  24090  ppinncl  24101  chtrpcl  24102  ppieq0  24103  ppiltx  24104  ppiublem1  24130  ppiub  24132  chpeq0  24136  chteq0  24137  chtublem  24139  chtub  24140  chpval2  24146  chpub  24148  mersenne  24155  perfectlem1  24157  perfectlem2  24158  dchrptlem1  24192  dchrptlem2  24193  bcmono  24205  bclbnd  24208  bpos1lem  24210  bposlem1  24212  bposlem2  24213  bposlem3  24214  bposlem4  24215  bposlem5  24216  bposlem6  24217  bposlem7  24218  bposlem8  24219  bposlem9  24220  lgslem1  24224  lgsdirprm  24257  lgseisenlem1  24277  lgseisenlem2  24278  lgseisenlem3  24279  lgseisen  24281  lgsquadlem1  24282  lgsquadlem2  24283  m1lgs  24290  2sqlem11  24303  chebbnd1lem1  24307  chebbnd1lem2  24308  chebbnd1lem3  24309  chebbnd1  24310  chtppilimlem1  24311  chtppilimlem2  24312  chtppilim  24313  chto1ub  24314  chebbnd2  24315  chto1lb  24316  chpchtlim  24317  chpo1ub  24318  chpo1ubb  24319  rplogsumlem1  24322  rplogsumlem2  24323  dchrisumlem2  24328  dchrisumlem3  24329  dchrvmasumiflem1  24339  dchrisum0fno1  24349  dchrisum0re  24351  dchrisum0lem1b  24353  dchrisum0lem1  24354  dchrisum0lem2  24356  rplogsum  24365  mulog2sumlem1  24372  mulog2sumlem2  24373  log2sumbnd  24382  selberglem2  24384  selbergb  24387  selberg2b  24390  chpdifbndlem1  24391  logdivbnd  24394  selberg3lem1  24395  selberg3  24397  selberg4lem1  24398  selberg4  24399  pntrmax  24402  pntrsumbnd2  24405  selberg3r  24407  selberg4r  24408  selberg34r  24409  pntrlog2bndlem2  24416  pntrlog2bndlem3  24417  pntrlog2bndlem4  24418  pntrlog2bndlem5  24419  pntrlog2bndlem6  24421  pntrlog2bnd  24422  pntpbnd1a  24423  pntpbnd1  24424  pntpbnd2  24425  pntpbnd  24426  pntibndlem2  24429  pntibndlem3  24430  pntibnd  24431  pntlemb  24435  pntlemg  24436  pntlemh  24437  pntlemr  24440  pntlemk  24444  pntlemo  24445  pnt2  24451  pnt  24452  ostth2lem1  24456  ostth3  24476  istrkg3ld  24509  tgldimor  24546  trgcgrg  24560  tgcgr4  24576  axlowdimlem6  24977  axlowdimlem16  24987  axlowdimlem17  24988  axlowdim  24991  umgrafi  25049  usisuslgra  25092  usgraexmplvtxlem  25122  usgraex2elv  25125  usgraexmpldifpr  25127  constr3lem4  25375  constr3trllem3  25380  constr3pthlem1  25383  constr3pthlem3  25385  wwlkextwrd  25456  wwlkextfun  25457  wwlkextinj  25458  wwlkm1edg  25463  wwlkextproplem3  25471  clwwlkgt0  25499  clwwlkn0  25502  clwlkisclwwlklem2a1  25507  clwlkisclwwlklem2a2  25508  clwlkisclwwlklem2fv1  25510  clwlkisclwwlklem2fv2  25511  clwlkisclwwlklem2a4  25512  clwlkisclwwlklem2a  25513  clwlkisclwwlklem1  25515  clwlkisclwwlk2  25518  clwwlkext2edg  25530  usg2cwwkdifex  25549  clwlkfclwwlk  25572  konigsberg  25715  vdgfrgragt2  25755  extwwlkfablem2  25806  numclwwlkovf2ex  25814  frgrareggt1  25844  frgrareg  25845  frgraregord013  25846  ex-pss  25878  ex-res  25891  ex-fv  25893  ex-fl  25897  nvge0  26303  ipidsq  26349  minvecolem2  26517  minvecolem4  26522  minvecolem2OLD  26527  minvecolem4OLD  26532  normlem7  26769  norm-ii-i  26790  norm3lemt  26805  normpar2i  26809  bcsiALT  26832  pjhthlem1  27044  opsqrlem6  27798  cdj3lem1  28087  addltmulALT  28099  oppgle  28414  resvplusg  28596  sqsscirc1  28714  nexple  28831  dya2iocucvr  29106  omssubadd  29128  omssubaddOLD  29132  oddpwdc  29187  eulerpartlemgc  29195  fibp1  29234  coinfliplem  29311  coinflipspace  29313  ballotlem2  29321  signstfveq0  29466  subfacp1lem1  29902  subfacp1lem5  29907  subfacval3  29912  problem2  30298  problem5  30301  circum  30318  nn0prpwlem  30978  taupi  31724  relowlpssretop  31767  sin2h  31935  cos2h  31936  tan2h  31937  poimirlem7  31947  poimirlem9  31949  opnmbllem0  31976  mblfinlem1  31977  mblfinlem2  31978  itg2addnclem  31993  isbnd2  32115  isbnd3  32116  heiborlem7  32149  rabren3dioph  35658  pellexlem2  35674  pellexlem5  35677  pell14qrgapw  35722  pellfundex  35734  rmspecsqrtnq  35754  jm2.24nn  35809  jm2.17a  35810  jm2.17b  35811  jm2.17c  35812  acongrep  35830  acongeq  35833  jm2.22  35850  jm2.23  35851  jm2.20nn  35852  jm3.1lem2  35873  expdiophlem1  35876  imo72b2lem0  36608  isprm7  36660  lhe4.4ex1a  36678  isosctrlem1ALT  37331  sineq0ALT  37334  lt3addmuld  37519  suplesup  37562  sumnnodd  37710  0ellimcdiv  37730  sinaover2ne0  37743  stoweidlem13  37873  stoweidlem14  37874  stoweidlem26  37886  stoweidlem49  37910  stoweidlem52  37913  wallispilem4  37930  wallispilem5  37931  wallispi  37932  wallispi2lem1  37933  wallispi2lem2  37934  wallispi2  37935  stirlinglem1  37936  stirlinglem3  37938  stirlinglem5  37940  stirlinglem6  37941  stirlinglem7  37942  stirlinglem10  37945  stirlinglem11  37946  stirlinglem15  37950  stirlingr  37952  dirker2re  37954  dirkerval2  37956  dirkerre  37957  dirkerper  37958  dirkertrigeqlem1  37960  dirkertrigeqlem3  37962  dirkercncflem1  37965  dirkercncflem2  37966  dirkercncflem4  37968  fourierdlem24  37993  fourierdlem43  38014  fourierdlem44  38015  fourierdlem57  38027  fourierdlem58  38028  fourierdlem62  38032  fourierdlem66  38036  fourierdlem68  38038  fourierdlem72  38042  fourierdlem76  38046  fourierdlem78  38048  fourierdlem79  38049  fourierdlem94  38064  fourierdlem103  38073  fourierdlem104  38074  fourierdlem111  38081  fourierdlem113  38083  sqwvfoura  38092  sqwvfourb  38093  fourierswlem  38094  fouriersw  38095  etransclem23  38122  salexct2  38198  salexct3  38201  salgencntex  38202  salgensscntex  38203  sge0ad2en  38273  ovnsubaddlem1  38392  mod2eq1n2dvds  38725  dfodd4  38788  oexpnegALTV  38806  nn0o1gt2ALTV  38823  nnoALTV  38824  nn0oALTV  38825  nn0e  38826  perfectALTVlem1  38843  perfectALTVlem2  38844  gbogt5  38863  sgoldbalt  38882  nnsum3primes4  38883  nnsum3primesgbe  38887  nnsum3primesle9  38889  nnsum4primesodd  38891  nnsum4primesoddALTV  38892  evengpoap3  38894  wtgoldbnnsum4prm  38897  bgoldbnnsum3prm  38899  pfx2  38953  2leaddle2  39044  p1lep2  39046  upgrfi  39183  umgrupgr  39192  upgredg  39228  usgruspgr  39265  nbusgrvtxm1  39453  upgrewlkle2  39625  usgra2pthlem1  39720  plusgndxnmulrndx  40006  cznnring  40011  nn0le2is012  40201  ply1mulgsumlem2  40232  zlmodzxznm  40343  zlmodzxzldeplem  40344  3halfnz  40370  difmodm1lt  40378  nn0o1gt2  40380  nno  40381  nn0o  40382  nn0eo  40388  flnn0div2ge  40393  rege1logbzge0  40423  fldivexpfllog2  40429  logbpw2m1  40431  fllog2  40432  blenpw2m1  40443  nnpw2blen  40444  nnolog2flm1  40454  blennngt2o2  40456  dig2nn1st  40469  dig2nn0  40475  dig2bits  40478  dignn0flhalflem1  40479  dignn0flhalflem2  40480  dignn0flhalf  40482  nn0sumshdiglemA  40483