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

Theorem 0red 9586
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 9585 . 2  |-  0  e.  RR
21a1i 11 1  |-  ( ph  ->  0  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762   RRcr 9480   0cc0 9481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278
This theorem is referenced by:  gt0ne0  10006  add20  10053  subge0  10054  lesub0  10058  mulge0  10059  msqgt0  10062  msqge0  10063  addgt0d  10116  prodgt0  10376  prodge0  10378  lt2msq1  10417  supmul1  10497  supmul  10500  0mnnnnn0  10817  rpgecl  11234  ge0p1rp  11237  max0sub  11384  iccf1o  11653  xov1plusxeqvd  11655  elfz1b  11737  elfz0fzfz0  11766  fz0fzelfz0  11767  fzo1fzo0n0  11821  elfzo0z  11822  fzofzim  11826  elfzodifsumelfzo  11839  ssfzoulel  11863  elfznelfzo  11872  modltm1p1mod  11995  expgt1  12159  ltexp2a  12172  expcan  12173  ltexp2  12174  leexp2  12175  leexp2a  12176  expnlbnd2  12252  discr  12258  brfi1uzind  12485  ccatsymb  12552  swrdnd  12607  swrdvalodm2  12614  swrdswrdlem  12634  swrdswrd  12635  swrdccatin2  12662  swrdccatin12lem3  12665  repswswrd  12706  swrd2lsw  12840  2swrd2eqwrdeq  12841  leabs  13082  max0add  13093  absgt0  13106  rlimrege0  13351  iseraltlem2  13454  fsumrecl  13505  o1fsum  13576  cvgcmp  13579  cvgcmpce  13581  geomulcvg  13637  mertenslem2  13646  rpnnen2lem4  13801  moddvds  13843  bitsfzolem  13932  bitsinv1lem  13939  sadcaddlem  13955  qnumgt0  14131  modprm0  14178  qexpz  14268  prmreclem4  14285  4sqlem6  14309  gzrngunit  18244  regsumsupp  18418  fvmptnn04ifd  19114  chfacffsupp  19117  chfacfscmul0  19119  chfacfscmulgsum  19121  chfacfpmmul0  19123  chfacfpmmulgsum  19125  prdsmet  20601  metustexhalf  20795  nlmvscnlem2  20922  nlmvscnlem1  20923  nmo0  20970  evth  21187  lebnumlem1  21189  lebnumii  21194  htpycc  21208  pcohtpylem  21247  pcoass  21252  pcorevlem  21254  nmoleub2lem3  21326  ipcnlem2  21412  ipcnlem1  21413  rrxcph  21552  rrxmetlem  21562  rrxmet  21563  rrxdstprj1  21564  ehlbase  21566  minveclem3b  21571  minveclem6  21577  pjthlem1  21580  ovolicopnf  21663  ioorcl2  21709  volivth  21744  mbfposr  21787  i1fmulc  21838  itg1mulc  21839  itg1ge0a  21846  mbfi1flim  21858  itg2split  21884  itg2monolem1  21885  itg2monolem3  21887  itg2mono  21888  itgge0  21945  dvlip  22122  dvlipcn  22123  dveq0  22129  dv11cn  22130  dvlt0  22134  dvfsumge  22151  dgradd2  22392  plydivlem3  22418  mtest  22526  radcnvlem1  22535  radcnv0  22538  radcnvlt1  22540  radcnvle  22542  pserulm  22544  pserdvlem1  22549  pserdv  22551  abelthlem2  22554  abelthlem7  22560  pilem2  22574  coseq00topi  22621  tanabsge  22625  tanord1  22650  tanord  22651  logne0  22708  rplogcl  22710  logdivle  22728  logcnlem3  22746  logcnlem4  22747  dvloglem  22750  logtayl  22762  abscxp2  22795  cxplt  22796  cxple  22797  cxple2a  22801  cxpcn3lem  22842  abscxpbnd  22848  chordthmlem5  22888  asinlem3  22923  atanre  22937  atanlogaddlem  22965  atanlogadd  22966  atanlogsublem  22967  atantan  22975  atans2  22983  cxp2limlem  23026  cxp2lim  23027  cxploglim2  23029  divsqrsumlem  23030  jensenlem2  23038  harmonicubnd  23060  fsumharmonic  23062  ftalem1  23067  ftalem2  23068  ftalem5  23071  vmacl  23113  chtwordi  23151  ppiwordi  23157  chtrpcl  23170  fsumfldivdiaglem  23186  fsumvma2  23210  chpval2  23214  chpchtsum  23215  chpub  23216  logfacbnd3  23219  logexprlim  23221  mersenne  23223  lgslem4  23295  lgsdilem  23318  lgsne0  23329  lgseisen  23349  lgsquadlem1  23350  lgsquadlem2  23351  chebbnd1lem2  23376  chebbnd1lem3  23377  chebbnd1  23378  chtppilimlem1  23379  chtppilimlem2  23380  chtppilim  23381  chebbnd2  23383  chto1lb  23384  chpchtlim  23385  chpo1ub  23386  dchrisumlema  23394  dchrisumlem2  23396  dchrisumlem3  23397  dchrmusumlema  23399  dchrvmasumlem2  23404  dchrvmasumiflem1  23407  dchrisum0flblem1  23414  dchrisum0flblem2  23415  dchrisum0re  23419  dchrisum0lema  23420  dchrisum0  23426  dirith2  23434  mulog2sumlem1  23440  vmalogdivsum2  23444  log2sumbnd  23450  selberg2lem  23456  chpdifbndlem1  23459  chpdifbndlem2  23460  chpdifbnd  23461  selberg3lem1  23463  pntrmax  23470  pntrsumo1  23471  pntrlog2bndlem4  23486  pntrlog2bndlem5  23487  pntpbnd1a  23491  pntpbnd1  23492  pntpbnd2  23493  pntlemg  23504  pntlemj  23509  pntlemk  23512  pntlem3  23515  pntleml  23517  pnt2  23519  pnt  23520  ostth2lem1  23524  padicabv  23536  padicabvcxp  23538  ostth2lem3  23541  ostth2lem4  23542  ostth3  23544  nvnencycllem  24305  frgraogt3nreg  24783  friendshipgt3  24784  minvecolem5  25459  minvecolem6  25460  htthlem  25496  pjhthlem1  25971  eulerpartlemgc  27927  sumnnodd  31127  dvcosax  31211  dvbdfbdioolem1  31213  dvbdfbdioolem2  31214  ioodvbdlimc1lem1  31216  ioodvbdlimc1lem2  31217  ioodvbdlimc2lem  31219  stoweidlem1  31256  stoweidlem7  31262  stoweidlem11  31266  stoweidlem25  31280  stoweidlem26  31281  stoweidlem34  31289  stoweidlem36  31291  stoweidlem41  31296  stoweidlem42  31297  stoweidlem44  31299  stoweidlem45  31300  fourierdlem6  31368  fourierdlem12  31374  fourierdlem19  31381  fourierdlem41  31403  fourierdlem45  31407  fourierdlem48  31410  fourierdlem51  31413  fourierdlem71  31433  bj-pinftynminfty  33577
  Copyright terms: Public domain W3C validator