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

Theorem 2re 9783
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 9772 . 2  |-  2  =  ( 1  +  1 )
2 1re 8805 . . 3  |-  1  e.  RR
32, 2readdcli 8818 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2328 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1621  (class class class)co 5792   RRcr 8704   1c1 8706    + caddc 8708   2c2 9763
This theorem is referenced by:  2cn  9784  3re  9785  2ne0  9797  3pos  9798  2lt3  9855  1lt3  9856  2lt4  9858  1lt4  9859  2lt5  9862  2lt6  9867  1lt6  9868  2lt7  9873  1lt7  9874  2lt8  9880  1lt8  9881  2lt9  9888  1lt9  9889  2lt10  9897  1lt10  9898  halfgt0  9900  halflt1  9901  halfpm6th  9904  rehalfcl  9906  halfpos2  9909  halfnneg2  9911  addltmul  9915  nominpos  9916  avglt1  9917  avglt2  9918  nn0lele2xi  9984  halfnz  10058  2rp  10327  fzprval  10811  fztpval  10812  flhalf  10921  expubnd  11129  expmulnbnd  11200  nn0opthlem2  11251  faclbnd2  11271  faclbnd4lem1  11273  faclbnd5  11278  hashfun  11355  sqrlem7  11700  sqr4  11724  sqr2gt1lt2  11726  abstri  11780  rddif  11790  absrdbnd  11791  sqreulem  11809  amgm2  11819  abs3lemi  11859  caucvgrlem  12111  iseralt  12123  climcndslem1  12271  climcndslem2  12272  climcnds  12273  geoihalfsum  12301  efcllem  12322  ege2le3  12334  ef01bndlem  12427  cos01bnd  12429  cos2bnd  12431  cos01gt0  12434  sin02gt0  12435  sincos2sgn  12437  sin4lt0  12438  eirrlem  12445  egt2lt3  12447  epos  12448  sqr2re  12491  oexpneg  12553  bitsp1o  12587  bitsfzolem  12588  bitsfzo  12589  bitsmod  12590  bitsfi  12591  bitsinv1lem  12595  isprm3  12730  oddprm  12831  iserodd  12851  prmreclem2  12927  prmreclem6  12931  4sqlem11  12965  4sqlem12  12966  2expltfac  13068  oppgtset  14788  efgredleme  15015  mgpsca  15295  mgptset  15296  mgpds  15298  abvtrivd  15568  xmetge0  17872  bl2in  17920  metnrmlem3  18328  iihalf1  18392  iihalf2  18394  pcoass  18485  tchcphlem1  18628  minveclem2  18753  minveclem4  18759  pjthlem1  18764  ovolunlem1a  18818  dyadss  18912  opnmbllem  18919  vitalilem2  18927  vitalilem4  18929  mbfi1fseqlem5  19037  lhop1lem  19323  aaliou3lem1  19685  aaliou3lem2  19686  aaliou3lem3  19687  aaliou3lem8  19688  pilem2  19791  pilem3  19792  pipos  19796  sinhalfpilem  19797  sincosq1lem  19828  sincosq1sgn  19829  sincosq2sgn  19830  sincosq3sgn  19831  sincosq4sgn  19832  tangtx  19836  sinq12gt0  19838  sincos4thpi  19844  tan4thpi  19845  sincos6thpi  19846  sineq0  19852  cosordlem  19856  tanord1  19862  efif1olem1  19867  efif1olem2  19868  efif1olem4  19870  efif1o  19871  efifo  19872  logsqr  20014  cxpcn3lem  20050  root1id  20057  root1eq1  20058  root1cj  20059  cxpeq  20060  ang180lem1  20070  ang180lem2  20071  isosctrlem1  20081  chordthmlem2  20093  1cubrlem  20100  atancj  20169  atantan  20182  atanbndlem  20184  atans2  20190  leibpilem1  20199  leibpi  20201  log2tlbnd  20204  log2ublem2  20206  log2ub  20208  divsqrsumlem  20237  harmonicbnd3  20264  basellem1  20281  basellem2  20282  basellem3  20283  basellem5  20285  ppisval  20304  chtdif  20359  ppidif  20364  ppinncl  20375  chtrpcl  20376  ppieq0  20377  ppiltx  20378  ppiublem1  20404  ppiub  20406  chpeq0  20410  chteq0  20411  chtublem  20413  chtub  20414  chpval2  20420  chpub  20422  mersenne  20429  perfectlem1  20431  perfectlem2  20432  dchrptlem1  20466  dchrptlem2  20467  bcmono  20479  bclbnd  20482  bpos1lem  20484  bposlem1  20486  bposlem2  20487  bposlem3  20488  bposlem4  20489  bposlem5  20490  bposlem6  20491  bposlem7  20492  bposlem8  20493  bposlem9  20494  lgslem1  20498  lgsdirprm  20531  lgseisenlem1  20551  lgseisenlem2  20552  lgseisenlem3  20553  lgseisen  20555  lgsquadlem1  20556  lgsquadlem2  20557  m1lgs  20564  2sqlem11  20577  chebbnd1lem1  20581  chebbnd1lem2  20582  chebbnd1lem3  20583  chebbnd1  20584  chtppilimlem1  20585  chtppilimlem2  20586  chtppilim  20587  chto1ub  20588  chebbnd2  20589  chto1lb  20590  chpchtlim  20591  chpo1ub  20592  chpo1ubb  20593  rplogsumlem1  20596  rplogsumlem2  20597  dchrisumlem2  20602  dchrisumlem3  20603  dchrvmasumiflem1  20613  dchrisum0fno1  20623  dchrisum0re  20625  dchrisum0lem1b  20627  dchrisum0lem1  20628  dchrisum0lem2  20630  rplogsum  20639  mulog2sumlem1  20646  mulog2sumlem2  20647  log2sumbnd  20656  selberglem2  20658  selbergb  20661  selberg2b  20664  chpdifbndlem1  20665  logdivbnd  20668  selberg3lem1  20669  selberg3  20671  selberg4lem1  20672  selberg4  20673  pntrmax  20676  pntrsumbnd2  20679  selberg3r  20681  selberg4r  20682  selberg34r  20683  pntrlog2bndlem2  20690  pntrlog2bndlem3  20691  pntrlog2bndlem4  20692  pntrlog2bndlem5  20693  pntrlog2bndlem6  20695  pntrlog2bnd  20696  pntpbnd1a  20697  pntpbnd1  20698  pntpbnd2  20699  pntpbnd  20700  pntibndlem2  20703  pntibndlem3  20704  pntibnd  20705  pntlemb  20709  pntlemg  20710  pntlemh  20711  pntlemr  20714  pntlemk  20718  pntlemo  20719  pnt2  20725  pnt  20726  ostth2lem1  20730  ostth3  20750  ex-pss  20759  ex-res  20772  ex-fv  20774  ex-fl  20778  nvge0  21201  ipidsq  21247  minvecolem2  21415  minvecolem4  21420  normlem7  21656  norm-ii-i  21677  norm3lem  21689  norm3lemt  21692  normpar2i  21696  bcsiALT  21719  pjhthlem1  21931  opsqrlem6  22686  cdj3lem1  22975  addltmulALT  22987  zetacvg  23062  subfacp1lem1  23083  subfacp1lem5  23088  subfacval3  23093  umgrafi  23247  konigsberg  23284  circum  23380  4bc2eq6  23471  axlowdimlem3  23948  axlowdimlem4  23949  axlowdimlem6  23951  axlowdimlem16  23961  axlowdimlem17  23962  axlowdim  23965  cntrset  24970  mslb1  24975  msra3  24977  fnckle  25413  pgapspf  25420  nn0prpwlem  25606  csbrn  25830  trirn  25831  isbnd2  25875  isbnd3  25876  heiborlem7  25909  rabren3dioph  26266  pellexlem2  26283  pellexlem5  26286  pell14qrgapw  26329  pellfundex  26339  rmspecsqrnq  26359  jm2.24nn  26414  jm2.17a  26415  jm2.17b  26416  jm2.17c  26417  acongrep  26435  acongeq  26438  jm2.22  26456  jm2.23  26457  jm2.20nn  26458  jm3.1lem2  26479  expdiophlem1  26482  matplusg  26837  lhe4.4ex1a  26914  stoweidlem5  27123  stoweidlem13  27131  stoweidlem14  27132  stoweidlem24  27142  stoweidlem26  27144  stoweidlem28  27146  stoweidlem49  27167  stoweidlem52  27170  stoweidlem62  27180  wallispilem3  27185  wallispilem4  27186  wallispilem5  27187  wallispi  27188  wallispi2lem1  27189  wallispi2lem2  27190  wallispi2  27191  stirlinglem1  27192  stirlinglem3  27194  stirlinglem5  27196  stirlinglem6  27197  stirlinglem7  27198  stirlinglem10  27201  stirlinglem11  27202  stirlinglem15  27206  stirlingr  27208
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 2239  ax-1cn 8763  ax-icn 8764  ax-addcl 8765  ax-addrcl 8766  ax-mulcl 8767  ax-mulrcl 8768  ax-i2m1 8773  ax-1ne0 8774  ax-rrecex 8777  ax-cnre 8778
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-xp 4675  df-cnv 4677  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fv 4689  df-ov 5795  df-2 9772
  Copyright terms: Public domain W3C validator