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

Theorem 2re 9811
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 9800 . 2  |-  2  =  ( 1  +  1 )
2 1re 8833 . . 3  |-  1  e.  RR
32, 2readdcli 8846 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2354 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1685  (class class class)co 5820   RRcr 8732   1c1 8734    + caddc 8736   2c2 9791
This theorem is referenced by:  2cn  9812  3re  9813  2ne0  9825  3pos  9826  2lt3  9883  1lt3  9884  2lt4  9886  1lt4  9887  2lt5  9890  2lt6  9895  1lt6  9896  2lt7  9901  1lt7  9902  2lt8  9908  1lt8  9909  2lt9  9916  1lt9  9917  2lt10  9925  1lt10  9926  halfgt0  9928  halflt1  9929  halfpm6th  9932  rehalfcl  9934  halfpos2  9937  halfnneg2  9939  addltmul  9943  nominpos  9944  avglt1  9945  avglt2  9946  nn0lele2xi  10012  halfnz  10086  2rp  10355  fzprval  10840  fztpval  10841  flhalf  10950  expubnd  11158  expmulnbnd  11229  nn0opthlem2  11280  faclbnd2  11300  faclbnd4lem1  11302  faclbnd5  11307  hashfun  11385  sqrlem7  11730  sqr4  11754  sqr2gt1lt2  11756  abstri  11810  rddif  11820  absrdbnd  11821  sqreulem  11839  amgm2  11849  abs3lemi  11889  caucvgrlem  12141  iseralt  12153  climcndslem1  12304  climcndslem2  12305  climcnds  12306  geoihalfsum  12334  efcllem  12355  ege2le3  12367  ef01bndlem  12460  cos01bnd  12462  cos2bnd  12464  cos01gt0  12467  sin02gt0  12468  sincos2sgn  12470  sin4lt0  12471  eirrlem  12478  egt2lt3  12480  epos  12481  sqr2re  12524  oexpneg  12586  bitsp1o  12620  bitsfzolem  12621  bitsfzo  12622  bitsmod  12623  bitsfi  12624  bitsinv1lem  12628  isprm3  12763  oddprm  12864  iserodd  12884  prmreclem2  12960  prmreclem6  12964  4sqlem11  12998  4sqlem12  12999  2expltfac  13101  oppgtset  14821  efgredleme  15048  mgpsca  15328  mgptset  15329  mgpds  15331  abvtrivd  15601  xmetge0  17905  bl2in  17953  metnrmlem3  18361  iihalf1  18425  iihalf2  18427  pcoass  18518  tchcphlem1  18661  minveclem2  18786  minveclem4  18792  pjthlem1  18797  ovolunlem1a  18851  dyadss  18945  opnmbllem  18952  vitalilem2  18960  vitalilem4  18962  mbfi1fseqlem5  19070  lhop1lem  19356  aaliou3lem1  19718  aaliou3lem2  19719  aaliou3lem3  19720  aaliou3lem8  19721  pilem2  19824  pilem3  19825  pipos  19829  sinhalfpilem  19830  sincosq1lem  19861  sincosq1sgn  19862  sincosq2sgn  19863  sincosq3sgn  19864  sincosq4sgn  19865  tangtx  19869  sinq12gt0  19871  sincos4thpi  19877  tan4thpi  19878  sincos6thpi  19879  sineq0  19885  cosordlem  19889  tanord1  19895  efif1olem1  19900  efif1olem2  19901  efif1olem4  19903  efif1o  19904  efifo  19905  logsqr  20047  cxpcn3lem  20083  root1id  20090  root1eq1  20091  root1cj  20092  cxpeq  20093  ang180lem1  20103  ang180lem2  20104  isosctrlem1  20114  chordthmlem2  20126  1cubrlem  20133  atancj  20202  atantan  20215  atanbndlem  20217  atans2  20223  leibpilem1  20232  leibpi  20234  log2tlbnd  20237  log2ublem2  20239  log2ub  20241  divsqrsumlem  20270  harmonicbnd3  20297  basellem1  20314  basellem2  20315  basellem3  20316  basellem5  20318  ppisval  20337  chtdif  20392  ppidif  20397  ppinncl  20408  chtrpcl  20409  ppieq0  20410  ppiltx  20411  ppiublem1  20437  ppiub  20439  chpeq0  20443  chteq0  20444  chtublem  20446  chtub  20447  chpval2  20453  chpub  20455  mersenne  20462  perfectlem1  20464  perfectlem2  20465  dchrptlem1  20499  dchrptlem2  20500  bcmono  20512  bclbnd  20515  bpos1lem  20517  bposlem1  20519  bposlem2  20520  bposlem3  20521  bposlem4  20522  bposlem5  20523  bposlem6  20524  bposlem7  20525  bposlem8  20526  bposlem9  20527  lgslem1  20531  lgsdirprm  20564  lgseisenlem1  20584  lgseisenlem2  20585  lgseisenlem3  20586  lgseisen  20588  lgsquadlem1  20589  lgsquadlem2  20590  m1lgs  20597  2sqlem11  20610  chebbnd1lem1  20614  chebbnd1lem2  20615  chebbnd1lem3  20616  chebbnd1  20617  chtppilimlem1  20618  chtppilimlem2  20619  chtppilim  20620  chto1ub  20621  chebbnd2  20622  chto1lb  20623  chpchtlim  20624  chpo1ub  20625  chpo1ubb  20626  rplogsumlem1  20629  rplogsumlem2  20630  dchrisumlem2  20635  dchrisumlem3  20636  dchrvmasumiflem1  20646  dchrisum0fno1  20656  dchrisum0re  20658  dchrisum0lem1b  20660  dchrisum0lem1  20661  dchrisum0lem2  20663  rplogsum  20672  mulog2sumlem1  20679  mulog2sumlem2  20680  log2sumbnd  20689  selberglem2  20691  selbergb  20694  selberg2b  20697  chpdifbndlem1  20698  logdivbnd  20701  selberg3lem1  20702  selberg3  20704  selberg4lem1  20705  selberg4  20706  pntrmax  20709  pntrsumbnd2  20712  selberg3r  20714  selberg4r  20715  selberg34r  20716  pntrlog2bndlem2  20723  pntrlog2bndlem3  20724  pntrlog2bndlem4  20725  pntrlog2bndlem5  20726  pntrlog2bndlem6  20728  pntrlog2bnd  20729  pntpbnd1a  20730  pntpbnd1  20731  pntpbnd2  20732  pntpbnd  20733  pntibndlem2  20736  pntibndlem3  20737  pntibnd  20738  pntlemb  20742  pntlemg  20743  pntlemh  20744  pntlemr  20747  pntlemk  20751  pntlemo  20752  pnt2  20758  pnt  20759  ostth2lem1  20763  ostth3  20783  ex-pss  20792  ex-res  20805  ex-fv  20807  ex-fl  20811  nvge0  21234  ipidsq  21280  minvecolem2  21448  minvecolem4  21453  normlem7  21691  norm-ii-i  21712  norm3lem  21724  norm3lemt  21727  normpar2i  21731  bcsiALT  21754  pjhthlem1  21966  opsqrlem6  22721  cdj3lem1  23010  addltmulALT  23022  zetacvg  23096  subfacp1lem1  23117  subfacp1lem5  23122  subfacval3  23127  umgrafi  23281  konigsberg  23318  circum  23414  4bc2eq6  23505  axlowdimlem3  23982  axlowdimlem4  23983  axlowdimlem6  23985  axlowdimlem16  23995  axlowdimlem17  23996  axlowdim  23999  cntrset  25013  mslb1  25018  msra3  25020  fnckle  25456  pgapspf  25463  nn0prpwlem  25649  csbrn  25873  trirn  25874  isbnd2  25918  isbnd3  25919  heiborlem7  25952  rabren3dioph  26309  pellexlem2  26326  pellexlem5  26329  pell14qrgapw  26372  pellfundex  26382  rmspecsqrnq  26402  jm2.24nn  26457  jm2.17a  26458  jm2.17b  26459  jm2.17c  26460  acongrep  26478  acongeq  26481  jm2.22  26499  jm2.23  26500  jm2.20nn  26501  jm3.1lem2  26522  expdiophlem1  26525  matplusg  26880  lhe4.4ex1a  26957  stoweidlem5  27165  stoweidlem13  27173  stoweidlem14  27174  stoweidlem24  27184  stoweidlem26  27186  stoweidlem28  27188  stoweidlem49  27209  stoweidlem52  27212  stoweidlem62  27222  wallispilem3  27227  wallispilem4  27228  wallispilem5  27229  wallispi  27230  wallispi2lem1  27231  wallispi2lem2  27232  wallispi2  27233  stirlinglem1  27234  stirlinglem3  27236  stirlinglem5  27238  stirlinglem6  27239  stirlinglem7  27240  stirlinglem10  27243  stirlinglem11  27244  stirlinglem15  27248  stirlingr  27250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-1cn 8791  ax-icn 8792  ax-addcl 8793  ax-addrcl 8794  ax-mulcl 8795  ax-mulrcl 8796  ax-i2m1 8801  ax-1ne0 8802  ax-rrecex 8805  ax-cnre 8806
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-xp 4694  df-cnv 4696  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fv 5229  df-ov 5823  df-2 9800
  Copyright terms: Public domain W3C validator