Theorem 0red 10041

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

Step	Hyp	Ref	Expression
1		0re 10040	. 2 |- 0 e. RR
2	1	a1i 11	1 |- ( ph -> 0 e. RR )

Syntax hints:   -> wi 4   e. wcel 1990   RRcr 9935   0cc0 9936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  gt0ne0  10493  add20  10540  subge0  10541  lesub0  10545  mulge0  10546  msqgt0  10548  msqge0  10549  addgt0d  10602  sublt0d  10653  prodgt0  10868  prodge0  10870  lt2msq1  10907  supmul1  10992  supmul  10995  0mnnnnn0  11325  nn0negleid  11345  rpgecl  11859  ge0p1rp  11862  ledivge1le  11901  mul2lt0rlt0  11932  mul2lt0rgt0  11933  mul2lt0bi  11936  max0sub  12027  reltxrnmnf  12172  infmrp1  12174  iccf1o  12316  xov1plusxeqvd  12318  elfz0fzfz0  12444  fz0fzelfz0  12445  elfzo0z  12509  fzofzim  12514  fzo1fzo0n0  12518  elfzodifsumelfzo  12533  ssfzoulel  12562  elfznelfzo  12573  muladdmodid  12710  modltm1p1mod  12722  addmodlteq  12745  expgt1  12898  ltexp2a  12912  expcan  12913  ltexp2  12914  leexp2  12915  leexp2a  12916  expnlbnd2  12995  discr  13001  fi1uzind  13279  fi1uzindOLD  13285  ccatsymb  13366  ccat2s1fvw  13415  swrdnd  13432  swrdswrdlem  13459  swrdswrd  13460  swrdccatin2  13487  swrdccatin12lem3  13490  repswswrd  13531  swrd2lsw  13695  2swrd2eqwrdeq  13696  leabs  14039  max0add  14050  absgt0  14064  rlimrege0  14310  iseraltlem2  14413  fsumrecl  14465  o1fsum  14545  cvgcmp  14548  cvgcmpce  14550  geomulcvg  14607  mertenslem2  14617  fprodle  14727  rpnnen2lem4  14946  moddvds  14991  oddge22np1  15073  bitsfzolem  15156  bitsinv1lem  15163  sadcaddlem  15179  lcmgcdlem  15319  dvdsnprmd  15403  isprm7  15420  qnumgt0  15458  modprm0  15510  qexpz  15605  prmreclem4  15623  4sqlem6  15647  prmgaplem7  15761  gzrngunit  19812  regsumfsum  19814  regsumsupp  19968  fvmptnn04ifd  20658  chfacffsupp  20661  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulgsum  20669  prdsmet  22175  metustexhalf  22361  nlmvscnlem2  22489  nlmvscnlem1  22490  nmo0  22539  evth  22758  lebnumlem1  22760  lebnumii  22765  htpycc  22779  pcohtpylem  22819  pcoass  22824  pcorevlem  22826  nmoleub2lem3  22915  ipcnlem2  23043  ipcnlem1  23044  rrxcph  23180  rrxmetlem  23190  rrxmet  23191  rrxdstprj1  23192  ehlbase  23194  minveclem3b  23199  minveclem6  23205  pjthlem1  23208  ovolicopnf  23292  ioorcl2  23340  volivth  23375  mbfposr  23419  i1fmulc  23470  itg1mulc  23471  itg1ge0a  23478  mbfi1flim  23490  itg2split  23516  itg2monolem1  23517  itg2monolem3  23519  itg2mono  23520  itg2cnlem2  23529  itgge0  23577  dvlip  23756  dvlipcn  23757  dveq0  23763  dv11cn  23764  dvlt0  23768  dvfsumge  23785  dgradd2  24024  plydivlem3  24050  mtest  24158  radcnvlem1  24167  radcnv0  24170  radcnvlt1  24172  radcnvle  24174  pserulm  24176  pserdvlem1  24181  pserdv  24183  abelthlem2  24186  abelthlem7  24192  pilem2  24206  coseq00topi  24254  tanabsge  24258  tanord1  24283  tanord  24284  rplogcl  24350  logdivle  24368  logcnlem3  24390  logcnlem4  24391  dvloglem  24394  logtayl  24406  abscxp2  24439  cxplt  24440  cxple  24441  cxple2a  24445  cxpcn3lem  24488  abscxpbnd  24494  chordthmlem5  24563  asinlem3  24598  atanre  24612  atanlogaddlem  24640  atanlogadd  24641  atanlogsublem  24642  atantan  24650  atans2  24658  efrlim  24696  cxp2limlem  24702  cxp2lim  24703  cxploglim2  24705  divsqrtsumlem  24706  jensenlem2  24714  harmonicubnd  24736  fsumharmonic  24738  dmlogdmgm  24750  lgamgulmlem1  24755  lgamgulmlem2  24756  ftalem1  24799  ftalem2  24800  ftalem5  24803  vmacl  24844  chtwordi  24882  ppiwordi  24888  chtrpcl  24901  fsumfldivdiaglem  24915  fsumvma2  24939  chpval2  24943  chpchtsum  24944  chpub  24945  logfacbnd3  24948  logexprlim  24950  mersenne  24952  lgslem4  25025  lgsdilem  25049  lgsne0  25060  gausslemma2dlem1a  25090  lgseisen  25104  lgsquadlem1  25105  lgsquadlem2  25106  chebbnd1lem2  25159  chebbnd1lem3  25160  chebbnd1  25161  chtppilimlem1  25162  chtppilimlem2  25163  chtppilim  25164  chebbnd2  25166  chto1lb  25167  chpchtlim  25168  chpo1ub  25169  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  dchrmusumlema  25182  dchrvmasumlem2  25187  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0re  25202  dchrisum0lema  25203  dchrisum0  25209  dirith2  25217  mulog2sumlem1  25223  vmalogdivsum2  25227  log2sumbnd  25233  selberg2lem  25239  chpdifbndlem1  25242  chpdifbndlem2  25243  chpdifbnd  25244  selberg3lem1  25246  pntrmax  25253  pntrsumo1  25254  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntlemg  25287  pntlemj  25292  pntlemk  25295  pntlem3  25298  pntleml  25300  pnt2  25302  pnt  25303  ostth2lem1  25307  padicabv  25319  padicabvcxp  25321  ostth2lem3  25324  ostth2lem4  25325  ostth3  25327  trgcgrg  25410  tgcgr4  25426  axsegconlem7  25803  axsegconlem10  25806  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem10  25853  crctcshwlkn0lem3  26704  crctcshwlkn0  26713  clwlkclwwlklem2a2  26894  clwlkclwwlklem2a  26899  wwlksubclwwlks  26925  frgrogt3nreg  27255  friendshipgt3  27256  minvecolem5  27737  minvecolem6  27738  htthlem  27774  pjhthlem1  28250  nndiffz1  29548  bcm1n  29554  2sqmod  29648  pnfneige0  29997  nexple  30071  indf1o  30086  measinb  30284  eulerpartlems  30422  eulerpartlemgc  30424  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemodife  30559  sgnneg  30602  sgnmul  30604  sgnsub  30606  signsply0  30628  signslema  30639  signsvtp  30660  signshf  30665  itgexpif  30684  breprexplemc  30710  circlemeth  30718  logdivsqrle  30728  cvmliftlem2  31268  dnibndlem9  32476  unbdqndv2lem2  32501  knoppndvlem1  32503  knoppndvlem2  32504  knoppndvlem7  32509  knoppndvlem11  32513  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem19  32521  knoppndvlem20  32522  bj-pinftynminfty  33114  poimirlem10  33419  poimirlem11  33420  poimirlem24  33433  poimirlem29  33438  poimirlem31  33440  poimirlem32  33441  poimir  33442  mblfinlem2  33447  bddiblnc  33480  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  areacirclem1  33500  areacirclem4  33503  areacirc  33505  geomcau  33555  isbnd3b  33584  prdsbnd  33592  bfp  33623  rrnequiv  33634  irrapxlem1  37386  irrapxlem2  37387  irrapxlem3  37388  irrapxlem4  37389  pellexlem6  37398  pell14qrgt0  37423  pell1qrgaplem  37437  pellfundex  37450  pellfundrp  37452  monotoddzzfi  37507  jm2.24  37530  jm2.23  37563  jm2.26lem3  37568  jm3.1lem3  37586  k0004ss2  38450  imo72b2lem1  38471  dvgrat  38511  hashnzfz2  38520  binomcxplemnn0  38548  binomcxplemnotnn0  38555  neglt  39496  divlt0gt0d  39498  upbdrech2  39522  xralrple2  39570  xralrple3  39590  fiminre2  39594  reclt0d  39607  reclt0  39614  fsumnncl  39803  fsumsupp0  39810  sumnnodd  39862  lptre2pt  39872  limsupubuz  39945  liminfresre  40011  liminf0  40025  dvmptconst  40129  dvdivbd  40138  dvcosax  40141  dvbdfbdioolem1  40143  dvbdfbdioolem2  40144  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvxpaek  40155  dvnxpaek  40157  volioc  40188  volico  40200  stoweidlem1  40218  stoweidlem7  40224  stoweidlem11  40228  stoweidlem25  40242  stoweidlem26  40243  stoweidlem34  40251  stoweidlem36  40253  stoweidlem41  40258  stoweidlem42  40259  stoweidlem44  40261  stoweidlem45  40262  wallispilem3  40284  wallispilem4  40285  wallispi  40287  stirlinglem3  40293  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  dirkeritg  40319  dirkercncflem2  40321  fourierdlem9  40333  fourierdlem11  40335  fourierdlem12  40336  fourierdlem14  40338  fourierdlem15  40339  fourierdlem19  40343  fourierdlem24  40348  fourierdlem28  40352  fourierdlem30  40354  fourierdlem40  40364  fourierdlem41  40365  fourierdlem43  40367  fourierdlem44  40368  fourierdlem47  40370  fourierdlem50  40373  fourierdlem51  40374  fourierdlem57  40380  fourierdlem60  40383  fourierdlem61  40384  fourierdlem66  40389  fourierdlem68  40391  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem78  40401  fourierdlem79  40402  fourierdlem83  40406  fourierdlem88  40411  fourierdlem92  40415  fourierdlem93  40416  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem109  40432  fourierdlem111  40434  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  elaa2lem  40450  etransclem4  40455  etransclem18  40469  etransclem19  40470  etransclem23  40474  etransclem27  40478  etransclem31  40482  etransclem32  40483  etransclem35  40486  etransclem41  40492  etransclem46  40497  etransclem48  40499  rrxtopnfi  40506  qndenserrnbllem  40514  salgencntex  40561  sge0tsms  40597  sge0isum  40644  volicorecl  40760  hoiprodcl  40761  ovnlerp  40776  ovnsubaddlem1  40784  hoiprodcl3  40794  volicore  40795  hoidmvcl  40796  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnhoi  40817  hoiqssbllem2  40837  volicorege0  40851  vonhoire  40886  pimrecltpos  40919  pimrecltneg  40933  smfmbfcex  40968  nsssmfmbflem  40986  smfrec  40996  smfmullem3  41000  sharhght  41054  zm1nn  41316  eluzge0nn0  41322  elfz2z  41325  2ffzoeq  41338  iccpartigtl  41359  iccpartgt  41363  expnegico01  42308  m1modmmod  42316  difmodm1lt  42317  regt1loggt0  42330  refdivmptf  42336  elbigolo1  42351  rege1logbrege0  42352  fllog2  42362  dignn0flhalflem1  42409  amgmwlem  42548