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

Theorem 0red 9600
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 9599 . 2  |-  0  e.  RR
21a1i 11 1  |-  ( ph  ->  0  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   RRcr 9494   0cc0 9495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284
This theorem is referenced by:  gt0ne0  10023  add20  10070  subge0  10071  lesub0  10075  mulge0  10076  msqgt0  10079  msqge0  10080  addgt0d  10133  prodgt0  10393  prodge0  10395  lt2msq1  10434  supmul1  10514  supmul  10517  0mnnnnn0  10834  rpgecl  11254  ge0p1rp  11257  max0sub  11404  iccf1o  11673  xov1plusxeqvd  11675  elfz1b  11757  elfz0fzfz0  11787  fz0fzelfz0  11788  fzo1fzo0n0  11843  elfzo0z  11844  fzofzim  11848  elfzodifsumelfzo  11861  ssfzoulel  11885  elfznelfzo  11894  modltm1p1mod  12018  expgt1  12183  ltexp2a  12196  expcan  12197  ltexp2  12198  leexp2  12199  leexp2a  12200  expnlbnd2  12276  discr  12282  brfi1uzind  12511  ccatsymb  12579  swrdnd  12636  swrdvalodm2  12643  swrdswrdlem  12663  swrdswrd  12664  swrdccatin2  12691  swrdccatin12lem3  12694  repswswrd  12735  swrd2lsw  12869  2swrd2eqwrdeq  12870  leabs  13111  max0add  13122  absgt0  13136  rlimrege0  13381  iseraltlem2  13484  fsumrecl  13535  o1fsum  13606  cvgcmp  13609  cvgcmpce  13611  geomulcvg  13664  mertenslem2  13673  rpnnen2lem4  13828  moddvds  13870  bitsfzolem  13961  bitsinv1lem  13968  sadcaddlem  13984  qnumgt0  14160  modprm0  14207  qexpz  14297  prmreclem4  14314  4sqlem6  14338  gzrngunit  18357  regsumsupp  18531  fvmptnn04ifd  19227  chfacffsupp  19230  chfacfscmul0  19232  chfacfscmulgsum  19234  chfacfpmmul0  19236  chfacfpmmulgsum  19238  prdsmet  20746  metustexhalf  20940  nlmvscnlem2  21067  nlmvscnlem1  21068  nmo0  21115  evth  21332  lebnumlem1  21334  lebnumii  21339  htpycc  21353  pcohtpylem  21392  pcoass  21397  pcorevlem  21399  nmoleub2lem3  21471  ipcnlem2  21557  ipcnlem1  21558  rrxcph  21697  rrxmetlem  21707  rrxmet  21708  rrxdstprj1  21709  ehlbase  21711  minveclem3b  21716  minveclem6  21722  pjthlem1  21725  ovolicopnf  21808  ioorcl2  21854  volivth  21889  mbfposr  21932  i1fmulc  21983  itg1mulc  21984  itg1ge0a  21991  mbfi1flim  22003  itg2split  22029  itg2monolem1  22030  itg2monolem3  22032  itg2mono  22033  itg2cnlem2  22042  itgge0  22090  dvlip  22267  dvlipcn  22268  dveq0  22274  dv11cn  22275  dvlt0  22279  dvfsumge  22296  dgradd2  22537  plydivlem3  22563  mtest  22671  radcnvlem1  22680  radcnv0  22683  radcnvlt1  22685  radcnvle  22687  pserulm  22689  pserdvlem1  22694  pserdv  22696  abelthlem2  22699  abelthlem7  22705  pilem2  22719  coseq00topi  22767  tanabsge  22771  tanord1  22796  tanord  22797  logne0  22859  rplogcl  22861  logdivle  22879  logcnlem3  22897  logcnlem4  22898  dvloglem  22901  logtayl  22913  abscxp2  22946  cxplt  22947  cxple  22948  cxple2a  22952  cxpcn3lem  22993  abscxpbnd  22999  chordthmlem5  23039  asinlem3  23074  atanre  23088  atanlogaddlem  23116  atanlogadd  23117  atanlogsublem  23118  atantan  23126  atans2  23134  efrlim  23171  cxp2limlem  23177  cxp2lim  23178  cxploglim2  23180  divsqrtsumlem  23181  jensenlem2  23189  harmonicubnd  23211  fsumharmonic  23213  ftalem1  23218  ftalem2  23219  ftalem5  23222  vmacl  23264  chtwordi  23302  ppiwordi  23308  chtrpcl  23321  fsumfldivdiaglem  23337  fsumvma2  23361  chpval2  23365  chpchtsum  23366  chpub  23367  logfacbnd3  23370  logexprlim  23372  mersenne  23374  lgslem4  23446  lgsdilem  23469  lgsne0  23480  lgseisen  23500  lgsquadlem1  23501  lgsquadlem2  23502  chebbnd1lem2  23527  chebbnd1lem3  23528  chebbnd1  23529  chtppilimlem1  23530  chtppilimlem2  23531  chtppilim  23532  chebbnd2  23534  chto1lb  23535  chpchtlim  23536  chpo1ub  23537  dchrisumlema  23545  dchrisumlem2  23547  dchrisumlem3  23548  dchrmusumlema  23550  dchrvmasumlem2  23555  dchrvmasumiflem1  23558  dchrisum0flblem1  23565  dchrisum0flblem2  23566  dchrisum0re  23570  dchrisum0lema  23571  dchrisum0  23577  dirith2  23585  mulog2sumlem1  23591  vmalogdivsum2  23595  log2sumbnd  23601  selberg2lem  23607  chpdifbndlem1  23610  chpdifbndlem2  23611  chpdifbnd  23612  selberg3lem1  23614  pntrmax  23621  pntrsumo1  23622  pntrlog2bndlem4  23637  pntrlog2bndlem5  23638  pntpbnd1a  23642  pntpbnd1  23643  pntpbnd2  23644  pntlemg  23655  pntlemj  23660  pntlemk  23663  pntlem3  23666  pntleml  23668  pnt2  23670  pnt  23671  ostth2lem1  23675  padicabv  23687  padicabvcxp  23689  ostth2lem3  23692  ostth2lem4  23693  ostth3  23695  trgcgrg  23778  axsegconlem7  24098  axsegconlem10  24101  axcontlem2  24140  axcontlem4  24142  axcontlem7  24145  axcontlem10  24148  nvnencycllem  24515  clwwlkn0  24646  clwlkisclwwlklem2a2  24652  clwlkisclwwlklem2a  24657  wwlksubclwwlk  24676  frgraogt3nreg  24992  friendshipgt3  24993  minvecolem5  25669  minvecolem6  25670  htthlem  25706  pjhthlem1  26181  mul2lt0rlt0  27437  mul2lt0rgt0  27438  mul2lt0bi  27441  nndiffz1  27468  bcm1n  27472  2sqmod  27509  regsumfsum  27645  pnfneige0  27806  nexple  27878  indf1o  27910  measinb  28065  eulerpartlems  28172  eulerpartlemgc  28174  ballotlemfc0  28304  ballotlemfcc  28305  ballotlemodife  28309  sgnneg  28352  sgnmul  28354  sgnsub  28356  signsply0  28381  signslema  28392  signsvtp  28413  signshf  28418  dmlogdmgm  28439  lgamgulmlem1  28444  lgamgulmlem2  28445  cvmliftlem2  28604  bddiblnc  30060  ftc1anclem7  30071  ftc1anclem8  30072  ftc1anc  30073  areacirclem1  30082  areacirclem4  30085  areacirc  30087  geomcau  30227  isbnd3b  30256  prdsbnd  30264  bfp  30295  rrnequiv  30306  irrapxlem1  30733  irrapxlem2  30734  irrapxlem3  30735  irrapxlem4  30736  pellexlem6  30745  pell14qrgt0  30770  pell1qrgaplem  30784  pellfundex  30797  pellfundrp  30799  monotoddzzfi  30853  jm2.24  30876  jm2.23  30913  jm2.26lem3  30918  jm3.1lem3  30936  isprm7  31168  dvgrat  31169  lcmgcdlem  31188  hashnzfz2  31202  neglt  31416  divlt0gt0d  31418  sublt0d  31444  upbdrech2  31457  sumnnodd  31544  lptre2pt  31554  dvmptconst  31614  dvdivbd  31624  dvcosax  31627  dvbdfbdioolem1  31629  dvbdfbdioolem2  31630  ioodvbdlimc1lem1  31632  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  volioc  31661  stoweidlem1  31672  stoweidlem7  31678  stoweidlem11  31682  stoweidlem25  31696  stoweidlem26  31697  stoweidlem34  31705  stoweidlem36  31707  stoweidlem41  31712  stoweidlem42  31713  stoweidlem44  31715  stoweidlem45  31716  wallispilem3  31738  wallispilem4  31739  wallispi  31741  stirlinglem3  31747  stirlinglem5  31749  stirlinglem6  31750  stirlinglem7  31751  stirlinglem10  31754  stirlinglem11  31755  stirlinglem12  31756  dirkeritg  31773  dirkercncflem2  31775  fourierdlem9  31787  fourierdlem11  31789  fourierdlem12  31790  fourierdlem14  31792  fourierdlem15  31793  fourierdlem19  31797  fourierdlem24  31802  fourierdlem28  31806  fourierdlem30  31808  fourierdlem40  31818  fourierdlem41  31819  fourierdlem43  31821  fourierdlem44  31822  fourierdlem47  31825  fourierdlem50  31828  fourierdlem51  31829  fourierdlem57  31835  fourierdlem60  31838  fourierdlem61  31839  fourierdlem66  31844  fourierdlem68  31846  fourierdlem73  31851  fourierdlem74  31852  fourierdlem75  31853  fourierdlem78  31856  fourierdlem79  31857  fourierdlem83  31861  fourierdlem88  31866  fourierdlem92  31870  fourierdlem93  31871  fourierdlem97  31875  fourierdlem103  31881  fourierdlem104  31882  fourierdlem109  31887  fourierdlem111  31889  sqwvfoura  31900  sqwvfourb  31901  fourierswlem  31902  fouriersw  31903  sharhght  31920  zm1nn  32163  eluzge0nn0  32167  elfz2z  32169  2ffzoeq  32179  bj-pinftynminfty  34364  imo72b2lem1  37651
  Copyright terms: Public domain W3C validator