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

Theorem 0red 9379
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 9378 . 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 9273   0cc0 9274
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 2418  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-rnegex 9345  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 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-iota 5374  df-fv 5419  df-ov 6089
This theorem is referenced by:  gt0ne0  9796  add20  9843  subge0  9844  lesub0  9848  mulge0  9849  msqgt0  9852  msqge0  9853  addgt0d  9906  prodgt0  10166  prodge0  10168  lt2msq1  10207  supmul1  10287  supmul  10290  0mnnnnn0  10604  rpgecl  11008  ge0p1rp  11011  max0sub  11158  iccf1o  11421  xov1plusxeqvd  11423  elfz0fzfz0  11477  fz0fzelfz0  11478  elfz1b  11519  fzo1fzo0n0  11580  elfzo0z  11581  fzofzim  11585  elfzodifsumelfzo  11596  ssfzoulel  11613  elfznelfzo  11622  modltm1p1mod  11743  expgt1  11894  ltexp2a  11907  expcan  11908  ltexp2  11909  leexp2  11910  leexp2a  11911  expnlbnd2  11987  discr  11993  brfi1uzind  12211  ccatsymb  12273  swrdnd  12318  swrdvalodm2  12325  swrdswrdlem  12345  swrdswrd  12346  swrdccatin2  12370  swrdccatin12lem3  12373  repswswrd  12414  swrd2lsw  12544  2swrd2eqwrdeq  12545  leabs  12780  max0add  12791  absgt0  12804  rlimrege0  13049  iseraltlem2  13152  fsumrecl  13203  o1fsum  13268  cvgcmp  13271  cvgcmpce  13273  geomulcvg  13328  mertenslem2  13337  rpnnen2lem4  13492  moddvds  13534  bitsfzolem  13622  bitsinv1lem  13629  sadcaddlem  13645  qnumgt0  13820  modprm0  13865  qexpz  13955  prmreclem4  13972  4sqlem6  13996  gzrngunit  17847  regsumsupp  18021  prdsmet  19914  metustexhalf  20108  nlmvscnlem2  20235  nlmvscnlem1  20236  nmo0  20283  evth  20500  lebnumlem1  20502  lebnumii  20507  htpycc  20521  pcohtpylem  20560  pcoass  20565  pcorevlem  20567  nmoleub2lem3  20639  ipcnlem2  20725  ipcnlem1  20726  rrxcph  20865  rrxmetlem  20875  rrxmet  20876  rrxdstprj1  20877  ehlbase  20879  minveclem3b  20884  minveclem6  20890  pjthlem1  20893  ovolicopnf  20976  ioorcl2  21021  volivth  21056  mbfposr  21099  i1fmulc  21150  itg1mulc  21151  itg1ge0a  21158  mbfi1flim  21170  itg2split  21196  itg2monolem1  21197  itg2monolem3  21199  itg2mono  21200  itgge0  21257  dvlip  21434  dvlipcn  21435  dveq0  21441  dv11cn  21442  dvlt0  21446  dvfsumge  21463  dgradd2  21704  plydivlem3  21730  mtest  21838  radcnvlem1  21847  radcnv0  21850  radcnvlt1  21852  radcnvle  21854  pserulm  21856  pserdvlem1  21861  pserdv  21863  abelthlem2  21866  abelthlem7  21872  pilem2  21886  coseq00topi  21933  tanabsge  21937  tanord1  21962  tanord  21963  logne0  22020  rplogcl  22022  logdivle  22040  logcnlem3  22058  logcnlem4  22059  dvloglem  22062  logtayl  22074  abscxp2  22107  cxplt  22108  cxple  22109  cxple2a  22113  cxpcn3lem  22154  abscxpbnd  22160  chordthmlem5  22200  asinlem3  22235  atanre  22249  atanlogaddlem  22277  atanlogadd  22278  atanlogsublem  22279  atantan  22287  atans2  22295  cxp2limlem  22338  cxp2lim  22339  cxploglim2  22341  divsqrsumlem  22342  jensenlem2  22350  harmonicubnd  22372  fsumharmonic  22374  ftalem1  22379  ftalem2  22380  ftalem5  22383  vmacl  22425  chtwordi  22463  ppiwordi  22469  chtrpcl  22482  fsumfldivdiaglem  22498  fsumvma2  22522  chpval2  22526  chpchtsum  22527  chpub  22528  logfacbnd3  22531  logexprlim  22533  mersenne  22535  lgslem4  22607  lgsdilem  22630  lgsne0  22641  lgseisen  22661  lgsquadlem1  22662  lgsquadlem2  22663  chebbnd1lem2  22688  chebbnd1lem3  22689  chebbnd1  22690  chtppilimlem1  22691  chtppilimlem2  22692  chtppilim  22693  chebbnd2  22695  chto1lb  22696  chpchtlim  22697  chpo1ub  22698  dchrisumlema  22706  dchrisumlem2  22708  dchrisumlem3  22709  dchrmusumlema  22711  dchrvmasumlem2  22716  dchrvmasumiflem1  22719  dchrisum0flblem1  22726  dchrisum0flblem2  22727  dchrisum0re  22731  dchrisum0lema  22732  dchrisum0  22738  dirith2  22746  mulog2sumlem1  22752  vmalogdivsum2  22756  log2sumbnd  22762  selberg2lem  22768  chpdifbndlem1  22771  chpdifbndlem2  22772  chpdifbnd  22773  selberg3lem1  22775  pntrmax  22782  pntrsumo1  22783  pntrlog2bndlem4  22798  pntrlog2bndlem5  22799  pntpbnd1a  22803  pntpbnd1  22804  pntpbnd2  22805  pntlemg  22816  pntlemj  22821  pntlemk  22824  pntlem3  22827  pntleml  22829  pnt2  22831  pnt  22832  ostth2lem1  22836  padicabv  22848  padicabvcxp  22850  ostth2lem3  22853  ostth2lem4  22854  ostth3  22856  nvnencycllem  23474  minvecolem5  24227  minvecolem6  24228  htthlem  24264  pjhthlem1  24739  eulerpartlemgc  26693  areaquad  29535  stoweidlem1  29739  stoweidlem7  29745  stoweidlem11  29749  stoweidlem25  29763  stoweidlem26  29764  stoweidlem34  29772  stoweidlem36  29774  stoweidlem41  29779  stoweidlem42  29780  stoweidlem44  29782  stoweidlem45  29783  frgraogt3nreg  30656  friendshipgt3  30657  bj-pinftynminfty  32308
  Copyright terms: Public domain W3C validator