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

Theorem 0red 9595
Description:  0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
0red  |-  ( ph  ->  0  e.  RR )

Proof of Theorem 0red
StepHypRef Expression
1 0re 9594 . 2  |-  0  e.  RR
21a1i 11 1  |-  ( ph  ->  0  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   RRcr 9489   0cc0 9490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-i2m1 9558  ax-1ne0 9559  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-iota 5508  df-fv 5552  df-ov 6252
This theorem is referenced by:  gt0ne0  10030  add20  10077  subge0  10078  lesub0  10082  mulge0  10083  msqgt0  10085  msqge0  10086  addgt0d  10139  sublt0d  10189  prodgt0  10401  prodge0  10403  lt2msq1  10441  supmul1  10527  supmul  10530  0mnnnnn0  10853  rpgecl  11279  ge0p1rp  11282  mul2lt0rlt0  11349  mul2lt0rgt0  11350  mul2lt0bi  11353  max0sub  11440  reltxrnmnf  11583  infmrp1  11585  iccf1o  11727  xov1plusxeqvd  11729  elfz1b  11815  elfz0fzfz0  11846  fz0fzelfz0  11847  fzo1fzo0n0  11908  elfzo0z  11909  fzofzim  11913  elfzodifsumelfzo  11930  ssfzoulel  11955  elfznelfzo  11964  muladdmodid  12087  modltm1p1mod  12092  expgt1  12260  ltexp2a  12274  expcan  12275  ltexp2  12276  leexp2  12277  leexp2a  12278  expnlbnd2  12353  discr  12359  fi1uzind  12598  ccatsymb  12675  ccat2s1fvw  12717  swrdnd  12734  swrdswrdlem  12761  swrdswrd  12762  swrdccatin2  12789  swrdccatin12lem3  12792  repswswrd  12833  swrd2lsw  12971  2swrd2eqwrdeq  12972  leabs  13306  max0add  13317  absgt0  13331  rlimrege0  13586  iseraltlem2  13692  fsumrecl  13743  o1fsum  13816  cvgcmp  13819  cvgcmpce  13821  geomulcvg  13875  mertenslem2  13884  fprodle  13993  rpnnen2lem4  14213  moddvds  14255  bitsfzolem  14350  bitsfzolemOLD  14351  bitsinv1lem  14358  sadcaddlem  14374  lcmgcdlem  14514  qnumgt0  14642  modprm0  14699  qexpz  14789  prmreclem4  14806  4sqlem6  14830  prmgaplem7  14970  gzrngunit  18976  regsumsupp  19132  fvmptnn04ifd  19819  chfacffsupp  19822  chfacfscmul0  19824  chfacfscmulgsum  19826  chfacfpmmul0  19828  chfacfpmmulgsum  19830  prdsmet  21327  metustexhalf  21513  nlmvscnlem2  21630  nlmvscnlem1  21631  nmo0  21698  evth  21929  lebnumlem1  21931  lebnumlem1OLD  21934  lebnumii  21939  htpycc  21953  pcohtpylem  21992  pcoass  21997  pcorevlem  21999  nmoleub2lem3  22071  ipcnlem2  22157  ipcnlem1  22158  rrxcph  22293  rrxmetlem  22303  rrxmet  22304  rrxdstprj1  22305  ehlbase  22307  minveclem3b  22312  minveclem6  22318  minveclem3bOLD  22324  minveclem6OLD  22330  pjthlem1  22333  ovolicopnf  22420  ioorcl2  22466  volivth  22507  mbfposr  22550  i1fmulc  22603  itg1mulc  22604  itg1ge0a  22611  mbfi1flim  22623  itg2split  22649  itg2monolem1  22650  itg2monolem3  22652  itg2mono  22653  itg2cnlem2  22662  itgge0  22710  dvlip  22887  dvlipcn  22888  dveq0  22894  dv11cn  22895  dvlt0  22899  dvfsumge  22916  dgradd2  23164  plydivlem3  23190  mtest  23301  radcnvlem1  23310  radcnv0  23313  radcnvlt1  23315  radcnvle  23317  pserulm  23319  pserdvlem1  23324  pserdv  23326  abelthlem2  23329  abelthlem7  23335  pilem2  23349  pilem2OLD  23350  coseq00topi  23399  tanabsge  23403  tanord1  23428  tanord  23429  rplogcl  23495  logdivle  23513  logcnlem3  23531  logcnlem4  23532  dvloglem  23535  logtayl  23547  abscxp2  23580  cxplt  23581  cxple  23582  cxple2a  23586  cxpcn3lem  23629  abscxpbnd  23635  chordthmlem5  23704  asinlem3  23739  atanre  23753  atanlogaddlem  23781  atanlogadd  23782  atanlogsublem  23783  atantan  23791  atans2  23799  efrlim  23837  cxp2limlem  23843  cxp2lim  23844  cxploglim2  23846  divsqrtsumlem  23847  jensenlem2  23855  harmonicubnd  23877  fsumharmonic  23879  dmlogdmgm  23891  lgamgulmlem1  23896  lgamgulmlem2  23897  ftalem1  23939  ftalem2  23940  ftalem5  23943  ftalem5OLD  23945  vmacl  23987  chtwordi  24025  ppiwordi  24031  chtrpcl  24044  fsumfldivdiaglem  24060  fsumvma2  24084  chpval2  24088  chpchtsum  24089  chpub  24090  logfacbnd3  24093  logexprlim  24095  mersenne  24097  lgslem4  24169  lgsdilem  24192  lgsne0  24203  lgseisen  24223  lgsquadlem1  24224  lgsquadlem2  24225  chebbnd1lem2  24250  chebbnd1lem3  24251  chebbnd1  24252  chtppilimlem1  24253  chtppilimlem2  24254  chtppilim  24255  chebbnd2  24257  chto1lb  24258  chpchtlim  24259  chpo1ub  24260  dchrisumlema  24268  dchrisumlem2  24270  dchrisumlem3  24271  dchrmusumlema  24273  dchrvmasumlem2  24278  dchrvmasumiflem1  24281  dchrisum0flblem1  24288  dchrisum0flblem2  24289  dchrisum0re  24293  dchrisum0lema  24294  dchrisum0  24300  dirith2  24308  mulog2sumlem1  24314  vmalogdivsum2  24318  log2sumbnd  24324  selberg2lem  24330  chpdifbndlem1  24333  chpdifbndlem2  24334  chpdifbnd  24335  selberg3lem1  24337  pntrmax  24344  pntrsumo1  24345  pntrlog2bndlem4  24360  pntrlog2bndlem5  24361  pntpbnd1a  24365  pntpbnd1  24366  pntpbnd2  24367  pntlemg  24378  pntlemj  24383  pntlemk  24386  pntlem3  24389  pntleml  24391  pnt2  24393  pnt  24394  ostth2lem1  24398  padicabv  24410  padicabvcxp  24412  ostth2lem3  24415  ostth2lem4  24416  ostth3  24418  trgcgrg  24502  tgcgr4  24518  axsegconlem7  24895  axsegconlem10  24898  axcontlem2  24937  axcontlem4  24939  axcontlem7  24942  axcontlem10  24945  nvnencycllem  25313  clwwlkn0  25444  clwlkisclwwlklem2a2  25450  clwlkisclwwlklem2a  25455  wwlksubclwwlk  25474  frgraogt3nreg  25790  friendshipgt3  25791  minvecolem5  26465  minvecolem6  26466  minvecolem5OLD  26475  minvecolem6OLD  26476  htthlem  26512  pjhthlem1  26986  nndiffz1  28316  bcm1n  28321  2sqmod  28360  regsumfsum  28496  pnfneige0  28709  nexple  28783  indf1o  28797  measinb  28995  eulerpartlems  29145  eulerpartlemgc  29147  ballotlemfc0  29277  ballotlemfcc  29278  ballotlemodife  29282  sgnneg  29363  sgnmul  29365  sgnsub  29367  signsply0  29392  signslema  29403  signsvtp  29424  signshf  29429  cvmliftlem2  29961  bj-pinftynminfty  31576  poimirlem10  31857  poimirlem11  31858  poimirlem24  31871  poimirlem29  31876  poimirlem31  31878  poimirlem32  31879  poimir  31880  bddiblnc  31919  ftc1anclem7  31930  ftc1anclem8  31931  ftc1anc  31932  areacirclem1  31939  areacirclem4  31942  areacirc  31944  geomcau  31995  isbnd3b  32024  prdsbnd  32032  bfp  32063  rrnequiv  32074  irrapxlem1  35579  irrapxlem2  35580  irrapxlem3  35581  irrapxlem4  35582  pellexlem6  35591  pell14qrgt0  35618  pell1qrgaplem  35632  pellfundex  35647  pellfundrp  35649  monotoddzzfi  35703  jm2.24  35726  jm2.23  35764  jm2.26lem3  35769  jm3.1lem3  35787  imo72b2lem1  36527  isprm7  36573  dvgrat  36574  hashnzfz2  36583  binomcxplemnn0  36611  binomcxplemnotnn0  36618  neglt  37391  divlt0gt0d  37393  upbdrech2  37423  xralrple2  37474  fsumnncl  37534  sumnnodd  37593  lptre2pt  37603  dvmptconst  37668  dvdivbd  37678  dvcosax  37681  dvbdfbdioolem1  37683  dvbdfbdioolem2  37684  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem1OLD  37688  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  dvxpaek  37698  dvnxpaek  37700  volioc  37732  stoweidlem1  37744  stoweidlem7  37750  stoweidlem11  37754  stoweidlem25  37768  stoweidlem26  37769  stoweidlem34  37778  stoweidlem36  37780  stoweidlem41  37785  stoweidlem42  37786  stoweidlem44  37788  stoweidlem45  37789  wallispilem3  37812  wallispilem4  37813  wallispi  37815  stirlinglem3  37821  stirlinglem5  37823  stirlinglem6  37824  stirlinglem7  37825  stirlinglem10  37828  stirlinglem11  37829  stirlinglem12  37830  dirkeritg  37847  dirkercncflem2  37849  fourierdlem9  37861  fourierdlem11  37863  fourierdlem12  37864  fourierdlem14  37866  fourierdlem15  37867  fourierdlem19  37871  fourierdlem24  37876  fourierdlem28  37880  fourierdlem30  37882  fourierdlem40  37893  fourierdlem41  37894  fourierdlem43  37897  fourierdlem44  37898  fourierdlem47  37900  fourierdlem50  37903  fourierdlem51  37904  fourierdlem57  37910  fourierdlem60  37913  fourierdlem61  37914  fourierdlem66  37919  fourierdlem68  37921  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem78  37931  fourierdlem79  37932  fourierdlem83  37936  fourierdlem88  37941  fourierdlem92  37945  fourierdlem93  37946  fourierdlem97  37950  fourierdlem103  37956  fourierdlem104  37957  fourierdlem109  37962  fourierdlem111  37964  sqwvfoura  37975  sqwvfourb  37976  fourierswlem  37977  fouriersw  37978  elaa2lem  37980  elaa2lemOLD  37981  etransclem4  37986  etransclem18  38000  etransclem19  38001  etransclem23  38005  etransclem27  38009  etransclem31  38013  etransclem32  38014  etransclem35  38017  etransclem41  38023  etransclem46  38028  etransclem48OLD  38030  etransclem48  38031  sge0tsms  38073  sge0isum  38120  volico  38210  volicorecl  38215  hoiprodcl  38216  ovnlerp  38231  ovnsubaddlem1  38239  hoiprodcl3  38249  volicore  38250  hoidmvcl  38251  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem3  38266  ovnhoi  38272  sharhght  38288  iccpartigtl  38550  iccpartgt  38554  zm1nn  38847  eluzge0nn0  38851  elfz2z  38853  2ffzoeq  38862  expnegico01  39918  m1modmmod  39927  difmodm1lt  39928  regt1loggt0  39950  refdivmptf  39956  elbigolo1  39971  rege1logbrege0  39972  fllog2  39982  dignn0flhalflem1  40029
  Copyright terms: Public domain W3C validator