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

Theorem 2re 10383
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 10372 . 2  |-  2  =  ( 1  +  1 )
2 1re 9377 . . 3  |-  1  e.  RR
32, 2readdcli 9391 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2508 1  |-  2  e.  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756  (class class class)co 6086   RRcr 9273   1c1 9275    + caddc 9277   2c2 10363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rrecex 9346  ax-cnre 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-2 10372
This theorem is referenced by:  2cn  10384  3re  10387  2ne0  10406  3pos  10407  2lt3  10481  1lt3  10482  2lt4  10484  1lt4  10485  2lt5  10488  2lt6  10493  1lt6  10494  2lt7  10499  1lt7  10500  2lt8  10506  1lt8  10507  2lt9  10514  1lt9  10515  2lt10  10523  1lt10  10524  1le2  10527  2rene0  10529  halfre  10532  halfgt0  10534  halflt1  10535  rehalfcl  10543  halfpos2  10546  halfnneg2  10548  addltmul  10552  nominpos  10553  avglt1  10554  avglt2  10555  nn0lele2xi  10624  nn0n0n1ge2b  10636  halfnz  10712  2eluzge0  10892  2eluzge1  10893  2rp  10988  fztpval  11510  4fvwrd4  11525  fzo0to42pr  11608  flhalf  11666  2txmodxeq0  11751  expubnd  11916  expmulnbnd  11988  nn0opthlem2  12039  faclbnd2  12059  faclbnd4lem1  12061  faclbnd5  12066  hashge2el2dif  12176  hashfun  12191  wrdlenge2n0  12253  f1oun2prg  12519  2swrd2eqwrdeq  12545  sqrlem7  12730  sqr4  12754  sqr2gt1lt2  12756  abstri  12810  sqreulem  12839  amgm2  12849  caucvgrlem  13142  iseralt  13154  climcndslem1  13304  climcndslem2  13305  climcnds  13306  geoihalfsum  13334  efcllem  13355  ege2le3  13367  ef01bndlem  13460  cos01bnd  13462  cos2bnd  13464  cos01gt0  13467  sin02gt0  13468  sincos2sgn  13470  sin4lt0  13471  eirrlem  13478  egt2lt3  13480  epos  13481  sqr2re  13524  n2dvds1  13574  oexpneg  13587  bitsp1o  13621  bitsfzolem  13622  bitsfzo  13623  bitsfi  13625  oddprm  13874  iserodd  13894  prmreclem2  13970  prmreclem6  13974  4sqlem11  14008  4sqlem12  14009  2expltfac  14111  oppgtset  15858  efgredleme  16231  mgpsca  16586  mgptset  16587  mgpds  16589  matplusg  18290  psmetge0  19863  xmetge0  19894  bl2in  19950  metnrmlem3  20412  iihalf1  20478  iihalf2  20480  pcoass  20571  tchcphlem1  20725  csbren  20873  trirn  20874  minveclem2  20888  minveclem4  20894  pjthlem1  20899  ovolunlem1a  20954  dyadss  21049  opnmbllem  21056  vitalilem2  21064  vitalilem4  21066  mbfi1fseqlem5  21172  lhop1lem  21460  aaliou3lem2  21784  aaliou3lem8  21786  pilem2  21892  pilem3  21893  pipos  21898  sinhalfpilem  21900  sincosq1lem  21934  sincosq4sgn  21938  tangtx  21942  sinq12gt0  21944  sincos4thpi  21950  tan4thpi  21951  sincos6thpi  21952  sineq0  21958  cosordlem  21962  tanord1  21968  efif1olem1  21973  efif1olem2  21974  efif1olem4  21976  efif1o  21977  efifo  21978  cxpcn3lem  22160  root1id  22167  root1eq1  22168  root1cj  22169  cxpeq  22170  ang180lem1  22180  ang180lem2  22181  chordthmlem2  22203  1cubrlem  22211  atancj  22280  atantan  22293  atanbndlem  22295  atans2  22301  leibpilem1  22310  leibpi  22312  log2tlbnd  22315  log2ublem2  22317  log2ub  22319  divsqrsumlem  22348  harmonicbnd3  22376  basellem1  22393  basellem2  22394  basellem3  22395  basellem5  22397  chtdif  22471  ppidif  22476  ppinncl  22487  chtrpcl  22488  ppieq0  22489  ppiltx  22490  ppiublem1  22516  ppiub  22518  chpeq0  22522  chteq0  22523  chtublem  22525  chtub  22526  chpval2  22532  chpub  22534  mersenne  22541  perfectlem1  22543  perfectlem2  22544  dchrptlem1  22578  dchrptlem2  22579  bcmono  22591  bclbnd  22594  bpos1lem  22596  bposlem1  22598  bposlem2  22599  bposlem3  22600  bposlem4  22601  bposlem5  22602  bposlem6  22603  bposlem7  22604  bposlem8  22605  bposlem9  22606  lgslem1  22610  lgsdirprm  22643  lgseisenlem1  22663  lgseisenlem2  22664  lgseisenlem3  22665  lgseisen  22667  lgsquadlem1  22668  lgsquadlem2  22669  m1lgs  22676  2sqlem11  22689  chebbnd1lem1  22693  chebbnd1lem2  22694  chebbnd1lem3  22695  chebbnd1  22696  chtppilimlem1  22697  chtppilimlem2  22698  chtppilim  22699  chto1ub  22700  chebbnd2  22701  chto1lb  22702  chpchtlim  22703  chpo1ub  22704  chpo1ubb  22705  rplogsumlem1  22708  rplogsumlem2  22709  dchrisumlem2  22714  dchrisumlem3  22715  dchrvmasumiflem1  22725  dchrisum0fno1  22735  dchrisum0re  22737  dchrisum0lem1b  22739  dchrisum0lem1  22740  dchrisum0lem2  22742  rplogsum  22751  mulog2sumlem1  22758  mulog2sumlem2  22759  log2sumbnd  22768  selberglem2  22770  selbergb  22773  selberg2b  22776  chpdifbndlem1  22777  logdivbnd  22780  selberg3lem1  22781  selberg3  22783  selberg4lem1  22784  selberg4  22785  pntrmax  22788  pntrsumbnd2  22791  selberg3r  22793  selberg4r  22794  selberg34r  22795  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  pntrlog2bndlem6  22807  pntrlog2bnd  22808  pntpbnd1a  22809  pntpbnd1  22810  pntpbnd2  22811  pntpbnd  22812  pntibndlem2  22815  pntibndlem3  22816  pntibnd  22817  pntlemb  22821  pntlemg  22822  pntlemh  22823  pntlemr  22826  pntlemk  22830  pntlemo  22831  pnt2  22837  pnt  22838  ostth2lem1  22842  ostth3  22862  tgldimor  22930  trgcgrg  22942  axlowdimlem6  23144  axlowdimlem16  23154  axlowdimlem17  23155  axlowdim  23158  umgrafi  23207  usisuslgra  23237  usgraexvlem  23264  usgraex2elv  23267  usgraexmpldifpr  23269  constr3lem4  23484  constr3trllem3  23489  constr3pthlem1  23492  constr3pthlem3  23494  konigsberg  23559  ex-pss  23586  ex-res  23599  ex-fv  23601  ex-fl  23605  nvge0  24013  ipidsq  24059  minvecolem2  24227  minvecolem4  24232  normlem7  24469  norm-ii-i  24490  norm3lemt  24505  normpar2i  24509  bcsiALT  24532  pjhthlem1  24745  opsqrlem6  25500  cdj3lem1  25789  addltmulALT  25801  oppgle  26065  resvplusg  26253  sqsscirc1  26290  nexple  26400  rnlogblem  26410  dya2iocucvr  26651  oddpwdc  26689  eulerpartlemgc  26697  fibp1  26736  coinfliplem  26813  coinflipspace  26815  ballotlem2  26823  signstfveq0  26930  zetacvg  26953  lgamgulmlem2  26968  lgamgulmlem3  26969  lgamgulmlem4  26970  lgamgulmlem6  26972  lgamucov  26976  subfacp1lem1  27019  subfacp1lem5  27024  subfacval3  27029  problem2  27251  problem5  27254  circum  27270  4bc2eq6  27342  sin2h  28375  cos2h  28376  tan2h  28377  opnmbllem0  28380  mblfinlem1  28381  mblfinlem2  28382  itg2addnclem  28396  nn0prpwlem  28470  isbnd2  28635  isbnd3  28636  heiborlem7  28669  rabren3dioph  29107  pellexlem2  29124  pellexlem5  29127  pell14qrgapw  29170  pellfundex  29180  rmspecsqrnq  29200  jm2.24nn  29255  jm2.17a  29256  jm2.17b  29257  jm2.17c  29258  acongrep  29276  acongeq  29279  jm2.22  29297  jm2.23  29298  jm2.20nn  29299  jm3.1lem2  29320  expdiophlem1  29323  lhe4.4ex1a  29556  stoweidlem13  29761  stoweidlem14  29762  stoweidlem26  29774  stoweidlem49  29797  stoweidlem52  29800  wallispilem4  29816  wallispilem5  29817  wallispi  29818  wallispi2lem1  29819  wallispi2lem2  29820  wallispi2  29821  stirlinglem1  29822  stirlinglem3  29824  stirlinglem5  29826  stirlinglem6  29827  stirlinglem7  29828  stirlinglem10  29831  stirlinglem11  29832  stirlinglem15  29836  stirlingr  29838  2leaddle2  30128  p1lep2  30130  uzuzle23  30146  uz3m2nn  30148  elfzom1elfzo  30170  prmn2uzge3  30202  ccatw2s1p1  30222  usgra2pthlem1  30253  wwlkextwrd  30313  wwlkextfun  30314  wwlkextinj  30315  wwlkm1edg  30320  clwwlkgt0  30387  clwwlkn0  30390  clwlkisclwwlklem2a1  30394  clwlkisclwwlklem2a2  30395  clwlkisclwwlklem2fv1  30397  clwlkisclwwlklem2fv2  30398  clwlkisclwwlklem2a4  30399  clwlkisclwwlklem2a  30400  clwlkisclwwlklem1  30402  clwlkisclwwlk2  30405  clwwlkext2edg  30417  usg2cwwkdifex  30448  clwlkfclwwlk  30470  wwlkextproplem3  30515  vdgfrgragt2  30573  extwwlkfablem1  30620  extwwlkfablem2  30624  numclwwlkovf2ex  30632  frgrareggt1  30662  frgrareg  30663  frgraregord013  30664  nn0le2is012  30717  zlmodzxznm  30928  zlmodzxzldeplem  30929  ene1  30998  isosctrlem1ALT  31557  sineq0ALT  31560  bj-pirp  32375  pirp  35453  taupi  35457
  Copyright terms: Public domain W3C validator