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

Theorem 2re 9695
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 9684 . 2  |-  2  =  ( 1  +  1 )
2 1re 8717 . . 3  |-  1  e.  RR
32, 2readdcli 8730 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2323 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1621  (class class class)co 5710   RRcr 8616   1c1 8618    + caddc 8620   2c2 9675
This theorem is referenced by:  2cn  9696  3re  9697  2ne0  9709  3pos  9710  2lt3  9766  1lt3  9767  2lt4  9769  1lt4  9770  2lt5  9773  2lt6  9778  1lt6  9779  2lt7  9784  1lt7  9785  2lt8  9791  1lt8  9792  2lt9  9799  1lt9  9800  2lt10  9808  1lt10  9809  halfgt0  9811  halflt1  9812  halfpm6th  9815  rehalfcl  9817  halfpos2  9820  halfnneg2  9822  addltmul  9826  nominpos  9827  avglt1  9828  avglt2  9829  nn0lele2xi  9895  halfnz  9969  2rp  10238  fzprval  10722  fztpval  10723  flhalf  10832  expubnd  11040  expmulnbnd  11111  nn0opthlem2  11162  faclbnd2  11182  faclbnd4lem1  11184  faclbnd5  11189  hashfun  11266  sqrlem7  11611  sqr4  11635  sqr2gt1lt2  11637  abstri  11691  rddif  11701  absrdbnd  11702  sqreulem  11720  amgm2  11730  abs3lemi  11770  caucvgrlem  12022  iseralt  12034  climcndslem1  12182  climcndslem2  12183  climcnds  12184  geoihalfsum  12212  efcllem  12233  ege2le3  12245  ef01bndlem  12338  cos01bnd  12340  cos2bnd  12342  cos01gt0  12345  sin02gt0  12346  sincos2sgn  12348  sin4lt0  12349  eirrlem  12356  egt2lt3  12358  epos  12359  sqr2re  12402  oexpneg  12464  bitsp1o  12498  bitsfzolem  12499  bitsfzo  12500  bitsmod  12501  bitsfi  12502  bitsinv1lem  12506  isprm3  12641  oddprm  12742  iserodd  12762  prmreclem2  12838  prmreclem6  12842  4sqlem11  12876  4sqlem12  12877  2expltfac  12979  oppgtset  14660  efgredleme  14887  mgpsca  15167  mgptset  15168  mgpds  15170  abvtrivd  15440  xmetge0  17741  bl2in  17789  metnrmlem3  18197  iihalf1  18261  iihalf2  18263  pcoass  18354  tchcphlem1  18497  minveclem2  18622  minveclem4  18628  pjthlem1  18633  ovolunlem1a  18687  dyadss  18781  opnmbllem  18788  vitalilem2  18796  vitalilem4  18798  mbfi1fseqlem5  18906  lhop1lem  19192  aaliou3lem1  19554  aaliou3lem2  19555  aaliou3lem3  19556  aaliou3lem8  19557  pilem2  19660  pilem3  19661  pipos  19665  sinhalfpilem  19666  sincosq1lem  19697  sincosq1sgn  19698  sincosq2sgn  19699  sincosq3sgn  19700  sincosq4sgn  19701  tangtx  19705  sinq12gt0  19707  sincos4thpi  19713  tan4thpi  19714  sincos6thpi  19715  sineq0  19721  cosordlem  19725  tanord1  19731  efif1olem1  19736  efif1olem2  19737  efif1olem4  19739  efif1o  19740  efifo  19741  ang180lem1  19851  ang180lem2  19852  isosctrlem1  19862  chordthmlem2  19874  logsqr  19919  cxpcn3lem  19955  root1id  19962  root1eq1  19963  root1cj  19964  cxpeq  19965  1cubrlem  19969  atancj  20038  atantan  20051  atanbndlem  20053  atans2  20059  leibpilem1  20068  leibpi  20070  log2tlbnd  20073  log2ublem2  20075  log2ub  20077  divsqrsumlem  20106  harmonicbnd3  20133  basellem1  20150  basellem2  20151  basellem3  20152  basellem5  20154  ppisval  20173  chtdif  20228  ppidif  20233  ppinncl  20244  chtrpcl  20245  ppieq0  20246  ppiltx  20247  ppiublem1  20273  ppiub  20275  chpeq0  20279  chteq0  20280  chtublem  20282  chtub  20283  chpval2  20289  chpub  20291  mersenne  20298  perfectlem1  20300  perfectlem2  20301  dchrptlem1  20335  dchrptlem2  20336  bcmono  20348  bclbnd  20351  bpos1lem  20353  bposlem1  20355  bposlem2  20356  bposlem3  20357  bposlem4  20358  bposlem5  20359  bposlem6  20360  bposlem7  20361  bposlem8  20362  bposlem9  20363  lgslem1  20367  lgsdirprm  20400  lgseisenlem1  20420  lgseisenlem2  20421  lgseisenlem3  20422  lgseisen  20424  lgsquadlem1  20425  lgsquadlem2  20426  m1lgs  20433  2sqlem11  20446  chebbnd1lem1  20450  chebbnd1lem2  20451  chebbnd1lem3  20452  chebbnd1  20453  chtppilimlem1  20454  chtppilimlem2  20455  chtppilim  20456  chto1ub  20457  chebbnd2  20458  chto1lb  20459  chpchtlim  20460  chpo1ub  20461  chpo1ubb  20462  rplogsumlem1  20465  rplogsumlem2  20466  dchrisumlem2  20471  dchrisumlem3  20472  dchrvmasumiflem1  20482  dchrisum0fno1  20492  dchrisum0re  20494  dchrisum0lem1b  20496  dchrisum0lem1  20497  dchrisum0lem2  20499  rplogsum  20508  mulog2sumlem1  20515  mulog2sumlem2  20516  log2sumbnd  20525  selberglem2  20527  selbergb  20530  selberg2b  20533  chpdifbndlem1  20534  logdivbnd  20537  selberg3lem1  20538  selberg3  20540  selberg4lem1  20541  selberg4  20542  pntrmax  20545  pntrsumbnd2  20548  selberg3r  20550  selberg4r  20551  selberg34r  20552  pntrlog2bndlem2  20559  pntrlog2bndlem3  20560  pntrlog2bndlem4  20561  pntrlog2bndlem5  20562  pntrlog2bndlem6  20564  pntrlog2bnd  20565  pntpbnd1a  20566  pntpbnd1  20567  pntpbnd2  20568  pntpbnd  20569  pntibndlem2  20572  pntibndlem3  20573  pntibnd  20574  pntlemb  20578  pntlemg  20579  pntlemh  20580  pntlemr  20583  pntlemk  20587  pntlemo  20588  pnt2  20594  pnt  20595  ostth2lem1  20599  ostth3  20619  ex-pss  20628  ex-res  20641  ex-fv  20643  ex-fl  20647  nvge0  21070  ipidsq  21116  minvecolem2  21284  minvecolem4  21289  normlem7  21525  norm-ii-i  21546  norm3lem  21558  norm3lemt  21561  normpar2i  21565  bcsiALT  21588  pjhthlem1  21800  opsqrlem6  22555  cdj3lem1  22844  addltmulALT  22856  zetacvg  22860  subfacp1lem1  22881  subfacp1lem5  22886  subfacval3  22891  umgrafi  23045  konigsberg  23082  circum  23178  4bc2eq6  23269  axlowdimlem3  23746  axlowdimlem4  23747  axlowdimlem6  23749  axlowdimlem16  23759  axlowdimlem17  23760  axlowdim  23763  cntrset  24768  mslb1  24773  msra3  24775  fnckle  25211  pgapspf  25218  nn0prpwlem  25404  csbrn  25628  trirn  25629  isbnd2  25673  isbnd3  25674  heiborlem7  25707  rabren3dioph  26064  pellexlem2  26081  pellexlem5  26084  pell14qrgapw  26127  pellfundex  26137  rmspecsqrnq  26157  jm2.24nn  26212  jm2.17a  26213  jm2.17b  26214  jm2.17c  26215  acongrep  26233  acongeq  26236  jm2.22  26254  jm2.23  26255  jm2.20nn  26256  jm3.1lem2  26277  expdiophlem1  26280  matplusg  26635  lhe4.4ex1a  26712
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 1926  ax-ext 2234  ax-1cn 8675  ax-icn 8676  ax-addcl 8677  ax-addrcl 8678  ax-mulcl 8679  ax-mulrcl 8680  ax-i2m1 8685  ax-1ne0 8686  ax-rrecex 8689  ax-cnre 8690
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-xp 4594  df-cnv 4596  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fv 4608  df-ov 5713  df-2 9684
  Copyright terms: Public domain W3C validator