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

Theorem 0red 9390
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 9389 . 2  |-  0  e.  RR
21a1i 11 1  |-  ( ph  ->  0  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   RRcr 9284   0cc0 9285
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 2423  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-addrcl 9346  ax-mulcl 9347  ax-mulrcl 9348  ax-i2m1 9353  ax-1ne0 9354  ax-rnegex 9356  ax-rrecex 9357  ax-cnre 9358
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 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-iota 5384  df-fv 5429  df-ov 6097
This theorem is referenced by:  gt0ne0  9807  add20  9854  subge0  9855  lesub0  9859  mulge0  9860  msqgt0  9863  msqge0  9864  addgt0d  9917  prodgt0  10177  prodge0  10179  lt2msq1  10218  supmul1  10298  supmul  10301  0mnnnnn0  10615  rpgecl  11019  ge0p1rp  11022  max0sub  11169  iccf1o  11432  xov1plusxeqvd  11434  elfz0fzfz0  11488  fz0fzelfz0  11489  elfz1b  11530  fzo1fzo0n0  11591  elfzo0z  11592  fzofzim  11596  elfzodifsumelfzo  11607  ssfzoulel  11624  elfznelfzo  11633  modltm1p1mod  11754  expgt1  11905  ltexp2a  11918  expcan  11919  ltexp2  11920  leexp2  11921  leexp2a  11922  expnlbnd2  11998  discr  12004  brfi1uzind  12222  ccatsymb  12284  swrdnd  12329  swrdvalodm2  12336  swrdswrdlem  12356  swrdswrd  12357  swrdccatin2  12381  swrdccatin12lem3  12384  repswswrd  12425  swrd2lsw  12555  2swrd2eqwrdeq  12556  leabs  12791  max0add  12802  absgt0  12815  rlimrege0  13060  iseraltlem2  13163  fsumrecl  13214  o1fsum  13279  cvgcmp  13282  cvgcmpce  13284  geomulcvg  13339  mertenslem2  13348  rpnnen2lem4  13503  moddvds  13545  bitsfzolem  13633  bitsinv1lem  13640  sadcaddlem  13656  qnumgt0  13831  modprm0  13876  qexpz  13966  prmreclem4  13983  4sqlem6  14007  gzrngunit  17881  regsumsupp  18055  prdsmet  19948  metustexhalf  20142  nlmvscnlem2  20269  nlmvscnlem1  20270  nmo0  20317  evth  20534  lebnumlem1  20536  lebnumii  20541  htpycc  20555  pcohtpylem  20594  pcoass  20599  pcorevlem  20601  nmoleub2lem3  20673  ipcnlem2  20759  ipcnlem1  20760  rrxcph  20899  rrxmetlem  20909  rrxmet  20910  rrxdstprj1  20911  ehlbase  20913  minveclem3b  20918  minveclem6  20924  pjthlem1  20927  ovolicopnf  21010  ioorcl2  21055  volivth  21090  mbfposr  21133  i1fmulc  21184  itg1mulc  21185  itg1ge0a  21192  mbfi1flim  21204  itg2split  21230  itg2monolem1  21231  itg2monolem3  21233  itg2mono  21234  itgge0  21291  dvlip  21468  dvlipcn  21469  dveq0  21475  dv11cn  21476  dvlt0  21480  dvfsumge  21497  dgradd2  21738  plydivlem3  21764  mtest  21872  radcnvlem1  21881  radcnv0  21884  radcnvlt1  21886  radcnvle  21888  pserulm  21890  pserdvlem1  21895  pserdv  21897  abelthlem2  21900  abelthlem7  21906  pilem2  21920  coseq00topi  21967  tanabsge  21971  tanord1  21996  tanord  21997  logne0  22054  rplogcl  22056  logdivle  22074  logcnlem3  22092  logcnlem4  22093  dvloglem  22096  logtayl  22108  abscxp2  22141  cxplt  22142  cxple  22143  cxple2a  22147  cxpcn3lem  22188  abscxpbnd  22194  chordthmlem5  22234  asinlem3  22269  atanre  22283  atanlogaddlem  22311  atanlogadd  22312  atanlogsublem  22313  atantan  22321  atans2  22329  cxp2limlem  22372  cxp2lim  22373  cxploglim2  22375  divsqrsumlem  22376  jensenlem2  22384  harmonicubnd  22406  fsumharmonic  22408  ftalem1  22413  ftalem2  22414  ftalem5  22417  vmacl  22459  chtwordi  22497  ppiwordi  22503  chtrpcl  22516  fsumfldivdiaglem  22532  fsumvma2  22556  chpval2  22560  chpchtsum  22561  chpub  22562  logfacbnd3  22565  logexprlim  22567  mersenne  22569  lgslem4  22641  lgsdilem  22664  lgsne0  22675  lgseisen  22695  lgsquadlem1  22696  lgsquadlem2  22697  chebbnd1lem2  22722  chebbnd1lem3  22723  chebbnd1  22724  chtppilimlem1  22725  chtppilimlem2  22726  chtppilim  22727  chebbnd2  22729  chto1lb  22730  chpchtlim  22731  chpo1ub  22732  dchrisumlema  22740  dchrisumlem2  22742  dchrisumlem3  22743  dchrmusumlema  22745  dchrvmasumlem2  22750  dchrvmasumiflem1  22753  dchrisum0flblem1  22760  dchrisum0flblem2  22761  dchrisum0re  22765  dchrisum0lema  22766  dchrisum0  22772  dirith2  22780  mulog2sumlem1  22786  vmalogdivsum2  22790  log2sumbnd  22796  selberg2lem  22802  chpdifbndlem1  22805  chpdifbndlem2  22806  chpdifbnd  22807  selberg3lem1  22809  pntrmax  22816  pntrsumo1  22817  pntrlog2bndlem4  22832  pntrlog2bndlem5  22833  pntpbnd1a  22837  pntpbnd1  22838  pntpbnd2  22839  pntlemg  22850  pntlemj  22855  pntlemk  22858  pntlem3  22861  pntleml  22863  pnt2  22865  pnt  22866  ostth2lem1  22870  padicabv  22882  padicabvcxp  22884  ostth2lem3  22887  ostth2lem4  22888  ostth3  22890  nvnencycllem  23532  minvecolem5  24285  minvecolem6  24286  htthlem  24322  pjhthlem1  24797  eulerpartlemgc  26748  stoweidlem1  29799  stoweidlem7  29805  stoweidlem11  29809  stoweidlem25  29823  stoweidlem26  29824  stoweidlem34  29832  stoweidlem36  29834  stoweidlem41  29839  stoweidlem42  29840  stoweidlem44  29842  stoweidlem45  29843  frgraogt3nreg  30716  friendshipgt3  30717  bj-pinftynminfty  32553
  Copyright terms: Public domain W3C validator