MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2re Unicode version

Theorem 2re 9748
Description: The number 2 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
2re  |-  2  e.  RR

Proof of Theorem 2re
StepHypRef Expression
1 df-2 9737 . 2  |-  2  =  ( 1  +  1 )
2 1re 8770 . . 3  |-  1  e.  RR
32, 2readdcli 8783 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2326 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1621  (class class class)co 5757   RRcr 8669   1c1 8671    + caddc 8673   2c2 9728
This theorem is referenced by:  2cn  9749  3re  9750  2ne0  9762  3pos  9763  2lt3  9819  1lt3  9820  2lt4  9822  1lt4  9823  2lt5  9826  2lt6  9831  1lt6  9832  2lt7  9837  1lt7  9838  2lt8  9844  1lt8  9845  2lt9  9852  1lt9  9853  2lt10  9861  1lt10  9862  halfgt0  9864  halflt1  9865  halfpm6th  9868  rehalfcl  9870  halfpos2  9873  halfnneg2  9875  addltmul  9879  nominpos  9880  avglt1  9881  avglt2  9882  nn0lele2xi  9948  halfnz  10022  2rp  10291  fzprval  10775  fztpval  10776  flhalf  10885  expubnd  11093  expmulnbnd  11164  nn0opthlem2  11215  faclbnd2  11235  faclbnd4lem1  11237  faclbnd5  11242  hashfun  11319  sqrlem7  11664  sqr4  11688  sqr2gt1lt2  11690  abstri  11744  rddif  11754  absrdbnd  11755  sqreulem  11773  amgm2  11783  abs3lemi  11823  caucvgrlem  12075  iseralt  12087  climcndslem1  12235  climcndslem2  12236  climcnds  12237  geoihalfsum  12265  efcllem  12286  ege2le3  12298  ef01bndlem  12391  cos01bnd  12393  cos2bnd  12395  cos01gt0  12398  sin02gt0  12399  sincos2sgn  12401  sin4lt0  12402  eirrlem  12409  egt2lt3  12411  epos  12412  sqr2re  12455  oexpneg  12517  bitsp1o  12551  bitsfzolem  12552  bitsfzo  12553  bitsmod  12554  bitsfi  12555  bitsinv1lem  12559  isprm3  12694  oddprm  12795  iserodd  12815  prmreclem2  12891  prmreclem6  12895  4sqlem11  12929  4sqlem12  12930  2expltfac  13032  oppgtset  14752  efgredleme  14979  mgpsca  15259  mgptset  15260  mgpds  15262  abvtrivd  15532  xmetge0  17836  bl2in  17884  metnrmlem3  18292  iihalf1  18356  iihalf2  18358  pcoass  18449  tchcphlem1  18592  minveclem2  18717  minveclem4  18723  pjthlem1  18728  ovolunlem1a  18782  dyadss  18876  opnmbllem  18883  vitalilem2  18891  vitalilem4  18893  mbfi1fseqlem5  19001  lhop1lem  19287  aaliou3lem1  19649  aaliou3lem2  19650  aaliou3lem3  19651  aaliou3lem8  19652  pilem2  19755  pilem3  19756  pipos  19760  sinhalfpilem  19761  sincosq1lem  19792  sincosq1sgn  19793  sincosq2sgn  19794  sincosq3sgn  19795  sincosq4sgn  19796  tangtx  19800  sinq12gt0  19802  sincos4thpi  19808  tan4thpi  19809  sincos6thpi  19810  sineq0  19816  cosordlem  19820  tanord1  19826  efif1olem1  19831  efif1olem2  19832  efif1olem4  19834  efif1o  19835  efifo  19836  logsqr  19978  cxpcn3lem  20014  root1id  20021  root1eq1  20022  root1cj  20023  cxpeq  20024  ang180lem1  20034  ang180lem2  20035  isosctrlem1  20045  chordthmlem2  20057  1cubrlem  20064  atancj  20133  atantan  20146  atanbndlem  20148  atans2  20154  leibpilem1  20163  leibpi  20165  log2tlbnd  20168  log2ublem2  20170  log2ub  20172  divsqrsumlem  20201  harmonicbnd3  20228  basellem1  20245  basellem2  20246  basellem3  20247  basellem5  20249  ppisval  20268  chtdif  20323  ppidif  20328  ppinncl  20339  chtrpcl  20340  ppieq0  20341  ppiltx  20342  ppiublem1  20368  ppiub  20370  chpeq0  20374  chteq0  20375  chtublem  20377  chtub  20378  chpval2  20384  chpub  20386  mersenne  20393  perfectlem1  20395  perfectlem2  20396  dchrptlem1  20430  dchrptlem2  20431  bcmono  20443  bclbnd  20446  bpos1lem  20448  bposlem1  20450  bposlem2  20451  bposlem3  20452  bposlem4  20453  bposlem5  20454  bposlem6  20455  bposlem7  20456  bposlem8  20457  bposlem9  20458  lgslem1  20462  lgsdirprm  20495  lgseisenlem1  20515  lgseisenlem2  20516  lgseisenlem3  20517  lgseisen  20519  lgsquadlem1  20520  lgsquadlem2  20521  m1lgs  20528  2sqlem11  20541  chebbnd1lem1  20545  chebbnd1lem2  20546  chebbnd1lem3  20547  chebbnd1  20548  chtppilimlem1  20549  chtppilimlem2  20550  chtppilim  20551  chto1ub  20552  chebbnd2  20553  chto1lb  20554  chpchtlim  20555  chpo1ub  20556  chpo1ubb  20557  rplogsumlem1  20560  rplogsumlem2  20561  dchrisumlem2  20566  dchrisumlem3  20567  dchrvmasumiflem1  20577  dchrisum0fno1  20587  dchrisum0re  20589  dchrisum0lem1b  20591  dchrisum0lem1  20592  dchrisum0lem2  20594  rplogsum  20603  mulog2sumlem1  20610  mulog2sumlem2  20611  log2sumbnd  20620  selberglem2  20622  selbergb  20625  selberg2b  20628  chpdifbndlem1  20629  logdivbnd  20632  selberg3lem1  20633  selberg3  20635  selberg4lem1  20636  selberg4  20637  pntrmax  20640  pntrsumbnd2  20643  selberg3r  20645  selberg4r  20646  selberg34r  20647  pntrlog2bndlem2  20654  pntrlog2bndlem3  20655  pntrlog2bndlem4  20656  pntrlog2bndlem5  20657  pntrlog2bndlem6  20659  pntrlog2bnd  20660  pntpbnd1a  20661  pntpbnd1  20662  pntpbnd2  20663  pntpbnd  20664  pntibndlem2  20667  pntibndlem3  20668  pntibnd  20669  pntlemb  20673  pntlemg  20674  pntlemh  20675  pntlemr  20678  pntlemk  20682  pntlemo  20683  pnt2  20689  pnt  20690  ostth2lem1  20694  ostth3  20714  ex-pss  20723  ex-res  20736  ex-fv  20738  ex-fl  20742  nvge0  21165  ipidsq  21211  minvecolem2  21379  minvecolem4  21384  normlem7  21620  norm-ii-i  21641  norm3lem  21653  norm3lemt  21656  normpar2i  21660  bcsiALT  21683  pjhthlem1  21895  opsqrlem6  22650  cdj3lem1  22939  addltmulALT  22951  zetacvg  23026  subfacp1lem1  23047  subfacp1lem5  23052  subfacval3  23057  umgrafi  23211  konigsberg  23248  circum  23344  4bc2eq6  23435  axlowdimlem3  23912  axlowdimlem4  23913  axlowdimlem6  23915  axlowdimlem16  23925  axlowdimlem17  23926  axlowdim  23929  cntrset  24934  mslb1  24939  msra3  24941  fnckle  25377  pgapspf  25384  nn0prpwlem  25570  csbrn  25794  trirn  25795  isbnd2  25839  isbnd3  25840  heiborlem7  25873  rabren3dioph  26230  pellexlem2  26247  pellexlem5  26250  pell14qrgapw  26293  pellfundex  26303  rmspecsqrnq  26323  jm2.24nn  26378  jm2.17a  26379  jm2.17b  26380  jm2.17c  26381  acongrep  26399  acongeq  26402  jm2.22  26420  jm2.23  26421  jm2.20nn  26422  jm3.1lem2  26443  expdiophlem1  26446  matplusg  26801  lhe4.4ex1a  26878  stoweidlem5  27054  stoweidlem13  27062  stoweidlem14  27063  stoweidlem24  27073  stoweidlem26  27075  stoweidlem28  27077  stoweidlem49  27098  stoweidlem52  27101  stoweidlem62  27111
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-1cn 8728  ax-icn 8729  ax-addcl 8730  ax-addrcl 8731  ax-mulcl 8732  ax-mulrcl 8733  ax-i2m1 8738  ax-1ne0 8739  ax-rrecex 8742  ax-cnre 8743
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-xp 4640  df-cnv 4642  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fv 4654  df-ov 5760  df-2 9737
  Copyright terms: Public domain W3C validator