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

Theorem 0red 9670
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 9669 . 2  |-  0  e.  RR
21a1i 11 1  |-  ( ph  ->  0  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   RRcr 9564   0cc0 9565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-i2m1 9633  ax-1ne0 9634  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-iota 5565  df-fv 5609  df-ov 6318
This theorem is referenced by:  gt0ne0  10107  add20  10154  subge0  10155  lesub0  10159  mulge0  10160  msqgt0  10162  msqge0  10163  addgt0d  10216  sublt0d  10266  prodgt0  10478  prodge0  10480  lt2msq1  10518  supmul1  10604  supmul  10607  0mnnnnn0  10931  rpgecl  11357  ge0p1rp  11360  mul2lt0rlt0  11427  mul2lt0rgt0  11428  mul2lt0bi  11431  max0sub  11518  reltxrnmnf  11661  infmrp1  11663  iccf1o  11805  xov1plusxeqvd  11807  elfz1b  11893  elfz0fzfz0  11925  fz0fzelfz0  11926  fzo1fzo0n0  11988  elfzo0z  11989  fzofzim  11993  elfzodifsumelfzo  12011  ssfzoulel  12036  elfznelfzo  12045  muladdmodid  12169  modltm1p1mod  12174  expgt1  12342  ltexp2a  12356  expcan  12357  ltexp2  12358  leexp2  12359  leexp2a  12360  expnlbnd2  12435  discr  12441  fi1uzind  12683  ccatsymb  12763  ccat2s1fvw  12808  swrdnd  12825  swrdswrdlem  12852  swrdswrd  12853  swrdccatin2  12880  swrdccatin12lem3  12883  repswswrd  12924  swrd2lsw  13076  2swrd2eqwrdeq  13077  leabs  13411  max0add  13422  absgt0  13436  rlimrege0  13692  iseraltlem2  13798  fsumrecl  13849  o1fsum  13922  cvgcmp  13925  cvgcmpce  13927  geomulcvg  13981  mertenslem2  13990  fprodle  14099  rpnnen2lem4  14319  moddvds  14361  bitsfzolem  14456  bitsfzolemOLD  14457  bitsinv1lem  14464  sadcaddlem  14480  lcmgcdlem  14620  qnumgt0  14748  modprm0  14805  qexpz  14895  prmreclem4  14912  4sqlem6  14936  prmgaplem7  15076  gzrngunit  19082  regsumfsum  19084  regsumsupp  19239  fvmptnn04ifd  19926  chfacffsupp  19929  chfacfscmul0  19931  chfacfscmulgsum  19933  chfacfpmmul0  19935  chfacfpmmulgsum  19937  prdsmet  21434  metustexhalf  21620  nlmvscnlem2  21737  nlmvscnlem1  21738  nmo0  21805  evth  22036  lebnumlem1  22038  lebnumlem1OLD  22041  lebnumii  22046  htpycc  22060  pcohtpylem  22099  pcoass  22104  pcorevlem  22106  nmoleub2lem3  22178  ipcnlem2  22264  ipcnlem1  22265  rrxcph  22400  rrxmetlem  22410  rrxmet  22411  rrxdstprj1  22412  ehlbase  22414  minveclem3b  22419  minveclem6  22425  minveclem3bOLD  22431  minveclem6OLD  22437  pjthlem1  22440  ovolicopnf  22527  ioorcl2  22573  volivth  22614  mbfposr  22657  i1fmulc  22710  itg1mulc  22711  itg1ge0a  22718  mbfi1flim  22730  itg2split  22756  itg2monolem1  22757  itg2monolem3  22759  itg2mono  22760  itg2cnlem2  22769  itgge0  22817  dvlip  22994  dvlipcn  22995  dveq0  23001  dv11cn  23002  dvlt0  23006  dvfsumge  23023  dgradd2  23271  plydivlem3  23297  mtest  23408  radcnvlem1  23417  radcnv0  23420  radcnvlt1  23422  radcnvle  23424  pserulm  23426  pserdvlem1  23431  pserdv  23433  abelthlem2  23436  abelthlem7  23442  pilem2  23456  pilem2OLD  23457  coseq00topi  23506  tanabsge  23510  tanord1  23535  tanord  23536  rplogcl  23602  logdivle  23620  logcnlem3  23638  logcnlem4  23639  dvloglem  23642  logtayl  23654  abscxp2  23687  cxplt  23688  cxple  23689  cxple2a  23693  cxpcn3lem  23736  abscxpbnd  23742  chordthmlem5  23811  asinlem3  23846  atanre  23860  atanlogaddlem  23888  atanlogadd  23889  atanlogsublem  23890  atantan  23898  atans2  23906  efrlim  23944  cxp2limlem  23950  cxp2lim  23951  cxploglim2  23953  divsqrtsumlem  23954  jensenlem2  23962  harmonicubnd  23984  fsumharmonic  23986  dmlogdmgm  23998  lgamgulmlem1  24003  lgamgulmlem2  24004  ftalem1  24046  ftalem2  24047  ftalem5  24050  ftalem5OLD  24052  vmacl  24094  chtwordi  24132  ppiwordi  24138  chtrpcl  24151  fsumfldivdiaglem  24167  fsumvma2  24191  chpval2  24195  chpchtsum  24196  chpub  24197  logfacbnd3  24200  logexprlim  24202  mersenne  24204  lgslem4  24276  lgsdilem  24299  lgsne0  24310  lgseisen  24330  lgsquadlem1  24331  lgsquadlem2  24332  chebbnd1lem2  24357  chebbnd1lem3  24358  chebbnd1  24359  chtppilimlem1  24360  chtppilimlem2  24361  chtppilim  24362  chebbnd2  24364  chto1lb  24365  chpchtlim  24366  chpo1ub  24367  dchrisumlema  24375  dchrisumlem2  24377  dchrisumlem3  24378  dchrmusumlema  24380  dchrvmasumlem2  24385  dchrvmasumiflem1  24388  dchrisum0flblem1  24395  dchrisum0flblem2  24396  dchrisum0re  24400  dchrisum0lema  24401  dchrisum0  24407  dirith2  24415  mulog2sumlem1  24421  vmalogdivsum2  24425  log2sumbnd  24431  selberg2lem  24437  chpdifbndlem1  24440  chpdifbndlem2  24441  chpdifbnd  24442  selberg3lem1  24444  pntrmax  24451  pntrsumo1  24452  pntrlog2bndlem4  24467  pntrlog2bndlem5  24468  pntpbnd1a  24472  pntpbnd1  24473  pntpbnd2  24474  pntlemg  24485  pntlemj  24490  pntlemk  24493  pntlem3  24496  pntleml  24498  pnt2  24500  pnt  24501  ostth2lem1  24505  padicabv  24517  padicabvcxp  24519  ostth2lem3  24522  ostth2lem4  24523  ostth3  24525  trgcgrg  24609  tgcgr4  24625  axsegconlem7  25002  axsegconlem10  25005  axcontlem2  25044  axcontlem4  25046  axcontlem7  25049  axcontlem10  25052  nvnencycllem  25420  clwwlkn0  25551  clwlkisclwwlklem2a2  25557  clwlkisclwwlklem2a  25562  wwlksubclwwlk  25581  frgraogt3nreg  25897  friendshipgt3  25898  minvecolem5  26572  minvecolem6  26573  minvecolem5OLD  26582  minvecolem6OLD  26583  htthlem  26619  pjhthlem1  27093  nndiffz1  28415  bcm1n  28420  2sqmod  28458  pnfneige0  28806  nexple  28880  indf1o  28894  measinb  29092  eulerpartlems  29242  eulerpartlemgc  29244  ballotlemfc0  29374  ballotlemfcc  29375  ballotlemodife  29379  sgnneg  29460  sgnmul  29462  sgnsub  29464  signsply0  29489  signslema  29500  signsvtp  29521  signshf  29526  cvmliftlem2  30058  bj-pinftynminfty  31714  poimirlem10  31995  poimirlem11  31996  poimirlem24  32009  poimirlem29  32014  poimirlem31  32016  poimirlem32  32017  poimir  32018  bddiblnc  32057  ftc1anclem7  32068  ftc1anclem8  32069  ftc1anc  32070  areacirclem1  32077  areacirclem4  32080  areacirc  32082  geomcau  32133  isbnd3b  32162  prdsbnd  32170  bfp  32201  rrnequiv  32212  irrapxlem1  35711  irrapxlem2  35712  irrapxlem3  35713  irrapxlem4  35714  pellexlem6  35723  pell14qrgt0  35750  pell1qrgaplem  35764  pellfundex  35779  pellfundrp  35781  monotoddzzfi  35835  jm2.24  35858  jm2.23  35896  jm2.26lem3  35901  jm3.1lem3  35919  imo72b2lem1  36659  isprm7  36704  dvgrat  36705  hashnzfz2  36714  binomcxplemnn0  36742  binomcxplemnotnn0  36749  neglt  37532  divlt0gt0d  37534  upbdrech2  37564  xralrple2  37615  fsumnncl  37688  fsumsupp0  37695  sumnnodd  37748  lptre2pt  37758  dvmptconst  37823  dvdivbd  37833  dvcosax  37836  dvbdfbdioolem1  37838  dvbdfbdioolem2  37839  ioodvbdlimc1lem1  37841  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem1OLD  37843  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  dvxpaek  37853  dvnxpaek  37855  volioc  37887  stoweidlem1  37899  stoweidlem7  37905  stoweidlem11  37909  stoweidlem25  37923  stoweidlem26  37924  stoweidlem34  37933  stoweidlem36  37935  stoweidlem41  37940  stoweidlem42  37941  stoweidlem44  37943  stoweidlem45  37944  wallispilem3  37967  wallispilem4  37968  wallispi  37970  stirlinglem3  37976  stirlinglem5  37978  stirlinglem6  37979  stirlinglem7  37980  stirlinglem10  37983  stirlinglem11  37984  stirlinglem12  37985  dirkeritg  38002  dirkercncflem2  38004  fourierdlem9  38016  fourierdlem11  38018  fourierdlem12  38019  fourierdlem14  38021  fourierdlem15  38022  fourierdlem19  38026  fourierdlem24  38031  fourierdlem28  38035  fourierdlem30  38037  fourierdlem40  38048  fourierdlem41  38049  fourierdlem43  38052  fourierdlem44  38053  fourierdlem47  38055  fourierdlem50  38058  fourierdlem51  38059  fourierdlem57  38065  fourierdlem60  38068  fourierdlem61  38069  fourierdlem66  38074  fourierdlem68  38076  fourierdlem73  38081  fourierdlem74  38082  fourierdlem75  38083  fourierdlem78  38086  fourierdlem79  38087  fourierdlem83  38091  fourierdlem88  38096  fourierdlem92  38100  fourierdlem93  38101  fourierdlem97  38105  fourierdlem103  38111  fourierdlem104  38112  fourierdlem109  38117  fourierdlem111  38119  sqwvfoura  38130  sqwvfourb  38131  fourierswlem  38132  fouriersw  38133  elaa2lem  38135  elaa2lemOLD  38136  etransclem4  38141  etransclem18  38155  etransclem19  38156  etransclem23  38160  etransclem27  38164  etransclem31  38168  etransclem32  38169  etransclem35  38172  etransclem41  38178  etransclem46  38183  etransclem48OLD  38185  etransclem48  38186  rrxtopnfi  38193  qndenserrnbllem  38201  salgencntex  38240  sge0tsms  38260  sge0isum  38307  volico  38401  volicorecl  38406  hoiprodcl  38407  ovnlerp  38422  ovnsubaddlem1  38430  hoiprodcl3  38440  volicore  38441  hoidmvcl  38442  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem3  38457  ovnhoi  38463  hoiqssbllem2  38483  sharhght  38512  iccpartigtl  38775  iccpartgt  38779  zm1nn  39091  eluzge0nn0  39095  elfz2z  39097  2ffzoeq  39106  expnegico01  40588  m1modmmod  40597  difmodm1lt  40598  regt1loggt0  40620  refdivmptf  40626  elbigolo1  40641  rege1logbrege0  40642  fllog2  40652  dignn0flhalflem1  40699
  Copyright terms: Public domain W3C validator