Theorem 0red 11199

Description: The number 0 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
0red	⊢ (𝜑 → 0 ∈ ℝ)

Proof of Theorem 0red

Step	Hyp	Ref	Expression
1		0re 11198	. 2 ⊢ 0 ∈ ℝ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2145  ℝcr 11087  0cc0 11088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-1cn 11146  ax-addrcl 11149  ax-rnegex 11159  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-clel 2840  df-rex 3090

This theorem is referenced by:  gt0ne0  11667  add20  11714  subge0  11715  lesub0  11719  mulge0  11720  msqgt0  11722  msqge0  11723  gt0ne0d  11766  addgt0d  11777  sublt0d  11828  prodgt0  12053  mulgt1  12067  lt2msq1  12090  fiminre2  12154  supmul1  12175  supmul  12178  nnne0  12261  0mnnnnn0  12527  nn0negleid  12547  neglt  13027  rpgecl  13037  ge0p1rp  13040  ledivge1le  13080  mul2lt0rlt0  13111  mul2lt0rgt0  13112  mul2lt0bi  13115  prodge0rd  13116  max0sub  13213  reltxrnmnf  13360  infmrp1  13362  lincmb01cmp  13513  iccf1o  13514  xov1plusxeqvd  13516  elfz0fzfz0  13652  fz0fzelfz0  13653  elfzo0z  13721  fzofzim  13729  fzo1fzo0n0  13735  elfzodifsumelfzo  13751  ssfzoulel  13780  elfznelfzo  13793  muladdmodid  13937  modltm1p1mod  13950  addmodlteq  13973  expgt1  14127  ltexp2a  14193  expcan  14196  ltexp2  14197  leexp2  14198  leexp2a  14199  zzlesq  14233  expnlbnd2  14261  discr  14267  fi1uzind  14534  ccatsymb  14610  ccat2s1fvw  14666  swrdnd  14682  swrdnnn0nd  14684  swrdswrdlem  14731  swrdswrd  14732  repswswrd  14811  swrd2lsw  14979  2swrd2eqwrdeq  14980  sgnneg  15127  sgnsub  15133  sgnmul  15134  leabs  15340  max0add  15351  absgt0  15366  rlimrege0  15620  iseraltlem2  15724  fsumrecl  15775  o1fsum  15855  cvgcmp  15858  cvgcmpce  15860  geomulcvg  15920  mertenslem2  15929  fprodle  16040  rpnnen2lem4  16263  p1modz1  16307  moddvds  16311  oddge22np1  16397  bitsfzolem  16482  bitsinv1lem  16489  sadcaddlem  16505  nn0rppwr  16609  nn0expgcd  16612  lcmgcdlem  16654  dvdsnprmd  16738  2mulprm  16741  isprm7  16757  qnumgt0  16799  modprm0  16855  qexpz  16951  prmreclem4  16969  4sqlem6  16993  prmgaplem7  17107  gzrngunit  21543  regsumfsum  21545  regsumsupp  21732  fvmptnn04ifd  22971  chfacffsupp  22974  chfacfscmul0  22976  chfacfscmulgsum  22978  chfacfpmmul0  22980  chfacfpmmulgsum  22982  prdsmet  24488  metustexhalf  24674  nlmvscnlem2  24803  nlmvscnlem1  24804  nmo0  24853  blcvx  24916  iihalf1cn  25052  evth  25079  lebnumlem1  25081  lebnumii  25086  htpycc  25100  pcohtpylem  25139  pcoass  25144  pcorevlem  25146  nmoleub2lem3  25235  ipcnlem2  25364  ipcnlem1  25365  rrxcph  25512  rrxmetlem  25527  rrxmet  25528  rrxdstprj1  25529  ehlbase  25535  minveclem3b  25548  minveclem6  25554  pjthlem1  25557  ovolicopnf  25644  ioorcl2  25692  volivth  25727  mbfposr  25772  i1fmulc  25823  itg1mulc  25824  itg1ge0a  25831  mbfi1flim  25843  itg2split  25869  itg2monolem1  25870  itg2monolem3  25872  itg2mono  25873  itg2cnlem2  25882  itgge0  25931  bddiblnc  25962  dvlip  26113  dvlipcn  26114  dveq0  26120  dv11cn  26121  dvlt0  26125  dvfsumge  26142  dgradd2  26386  plydivlem3  26417  mtest  26525  radcnvlem1  26534  radcnv0  26537  radcnvlt1  26539  radcnvle  26541  pserulm  26543  pserdvlem1  26548  pserdv  26550  abelthlem2  26553  abelthlem7  26559  pilem2  26573  pilem3  26574  coseq00topi  26625  tanabsge  26629  cosq34lt1  26650  tanord1  26660  tanord  26661  rplogcl  26727  logdivle  26745  logcnlem3  26767  logcnlem4  26768  dvloglem  26771  logtayl  26783  abscxp2  26816  cxplt  26817  cxple  26818  cxple2a  26822  cxpcn3lem  26870  abscxpbnd  26876  rtprmirr  26883  chordthmlem4  26958  chordthmlem5  26959  asinlem3  26994  atanre  27008  atanlogaddlem  27036  atanlogadd  27037  atanlogsublem  27038  atantan  27046  atans2  27054  efrlim  27092  cxp2limlem  27098  cxp2lim  27099  cxploglim2  27101  divsqrtsumlem  27102  jensenlem2  27110  harmonicubnd  27132  fsumharmonic  27134  dmlogdmgm  27146  lgamgulmlem1  27151  lgamgulmlem2  27152  ftalem1  27195  ftalem2  27196  ftalem5  27199  vmacl  27240  chtwordi  27278  ppiwordi  27284  chtrpcl  27297  fsumfldivdiaglem  27311  fsumvma2  27336  chpval2  27340  chpchtsum  27341  chpub  27342  logfacbnd3  27345  logexprlim  27347  mersenne  27349  lgsdilem  27446  lgsne0  27457  gausslemma2dlem1a  27487  lgseisen  27501  lgsquadlem1  27502  lgsquadlem2  27503  2sqmod  27558  2sqnn0  27560  chebbnd1lem2  27592  chebbnd1lem3  27593  chebbnd1  27594  chtppilimlem1  27595  chtppilimlem2  27596  chtppilim  27597  chebbnd2  27599  chto1lb  27600  chpchtlim  27601  chpo1ub  27602  dchrisumlema  27610  dchrisumlem2  27612  dchrisumlem3  27613  dchrmusumlema  27615  dchrvmasumlem2  27620  dchrvmasumiflem1  27623  dchrisum0flblem1  27630  dchrisum0flblem2  27631  dchrisum0re  27635  dchrisum0lema  27636  dchrisum0  27642  dirith2  27650  mulog2sumlem1  27656  vmalogdivsum2  27660  log2sumbnd  27666  selberg2lem  27672  chpdifbndlem1  27675  chpdifbnd  27677  selberg3lem1  27679  pntrmax  27686  pntrsumo1  27687  pntrlog2bndlem4  27702  pntrlog2bndlem5  27703  pntpbnd1a  27707  pntpbnd1  27708  pntpbnd2  27709  pntlemg  27720  pntlemj  27725  pntlemk  27728  pntlem3  27731  pnt2  27735  pnt  27736  ostth2lem1  27740  padicabv  27752  padicabvcxp  27754  ostth2lem3  27757  ostth2lem4  27758  ostth3  27760  trgcgrg  28742  tgcgr4  28758  axsegconlem7  29182  axsegconlem10  29185  axcontlem2  29224  axcontlem4  29226  axcontlem7  29229  axcontlem10  29232  crctcshwlkn0lem3  30070  crctcshwlkn0  30079  clwlkclwwlklem2a2  30253  clwlkclwwlklem2a  30258  wwlksubclwwlk  30318  frgrogt3nreg  30657  friendshipgt3  30658  minvecolem5  31142  minvecolem6  31143  htthlem  31178  pjhthlem1  31652  sgnval2  32992  nndiffz1  33043  bcm1n  33052  fzo0opth  33060  expgt0b  33074  nexple  33090  oexpled  33093  indf1o  33097  wrdt2ind  33186  cycpmrn  33376  cyc3conja  33390  ccfldextdgrr  33979  constrsslem  34048  constrresqrtcl  34084  constrsqrtcl  34086  cos9thpiminplylem1  34089  pnfneige0  34258  measinb  34528  eulerpartlems  34667  eulerpartlemgc  34669  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemodife  34805  signsply0  34855  signslema  34866  signsvtp  34887  itgexpif  34910  breprexplemc  34936  circlemeth  34944  logdivsqrle  34954  0nn0m1nnn0  35475  cvmliftlem2  35649  dnibndlem9  36937  unbdqndv2lem2  36961  knoppndvlem1  36963  knoppndvlem2  36964  knoppndvlem7  36969  knoppndvlem11  36973  knoppndvlem14  36976  knoppndvlem15  36977  knoppndvlem17  36979  knoppndvlem19  36981  knoppndvlem20  36982  bj-pinftynminfty  37731  poimirlem10  38141  poimirlem11  38142  poimirlem24  38155  poimirlem29  38160  poimirlem31  38162  poimirlem32  38163  poimir  38164  mblfinlem2  38169  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  areacirclem1  38219  areacirclem4  38222  areacirc  38224  geomcau  38270  isbnd3b  38296  prdsbnd  38304  bfp  38335  rrnequiv  38346  resdvopclptsd  42657  lcmineqlem2  42659  lcmineqlem3  42660  lcmineqlem10  42667  lcmineqlem12  42669  lcmineqlem23  42680  3lexlogpow5ineq1  42683  3lexlogpow5ineq2  42684  3lexlogpow5ineq4  42685  3lexlogpow5ineq3  42686  3lexlogpow2ineq2  42688  3lexlogpow5ineq5  42689  aks4d1lem1  42691  dvrelog2  42693  dvrelog3  42694  dvrelog2b  42695  0nonelalab  42696  dvrelogpow2b  42697  aks4d1p1p3  42698  aks4d1p1p2  42699  aks4d1p1p4  42700  aks4d1p1p6  42702  aks4d1p1p7  42703  aks4d1p1p5  42704  aks4d1p1  42705  aks4d1p2  42706  aks4d1p3  42707  aks4d1p5  42709  aks4d1p6  42710  aks4d1p7d1  42711  aks4d1p7  42712  aks4d1p8d2  42714  aks4d1p8d3  42715  aks4d1p8  42716  aks4d1p9  42717  posbezout  42729  primrootspoweq0  42735  aks6d1c1  42745  hashscontpow1  42750  aks6d1c2lem4  42756  aks6d1c5lem2  42767  deg1gprod  42769  2np3bcnp1  42773  2ap1caineq  42774  sticksstones7  42781  sticksstones10  42784  sticksstones12a  42786  sticksstones12  42787  sticksstones22  42797  aks6d1c6lem3  42801  bcled  42807  bcle2d  42808  aks6d1c7lem1  42809  aks6d1c7lem2  42810  aks6d1c7  42813  aks5lem6  42821  unitscyglem5  42828  aks5lem8  42830  sn-1ne2  42892  oexpreposd  42943  posqsqznn  42957  redvmptabs  42981  readvrec  42983  re1m1e0m0  43018  re0m0e0  43023  remul01  43028  sn-remul0ord  43029  remulneg2d  43036  rediveq0d  43070  sn-rediv0d  43074  sn-addlt0d  43092  sn-addgt0d  43093  renegmulnnass  43099  zmulcomlem  43101  mulgt0con1dlem  43103  sn-mulgt1d  43113  mulltgt0d  43116  mullt0b2d  43118  sn-mullt0d  43119  sn-msqgt0d  43120  fimgmcyc  43164  dffltz  43228  3cubeslem1  43277  irrapxlem1  43411  irrapxlem2  43412  irrapxlem3  43413  irrapxlem4  43414  pellexlem6  43423  pell14qrgt0  43448  pell1qrgaplem  43462  pellfundex  43475  pellfundrp  43477  monotoddzzfi  43531  jm2.24  43552  jm2.23  43585  jm2.26lem3  43590  jm3.1lem3  43608  sqrtcvallem1  44219  reabsifneg  44220  reabsifpos  44222  sqrtcval  44229  k0004ss2  44740  imo72b2lem1  44757  dvgrat  44886  hashnzfz2  44895  binomcxplemnn0  44923  binomcxplemnotnn0  44930  divlt0gt0d  45863  upbdrech2  45885  xralrple2  45928  xralrple3  45947  reclt0d  45960  reclt0  45964  xrpnf  46057  fsumnncl  46146  fsumsupp0  46152  sumnnodd  46204  lptre2pt  46212  limsupubuz  46285  liminfresre  46351  liminf0  46365  dvmptconst  46487  dvdivbd  46495  dvcosax  46498  dvbdfbdioolem1  46500  dvbdfbdioolem2  46501  ioodvbdlimc1lem1  46503  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  dvxpaek  46512  dvnxpaek  46514  volioc  46544  volico  46555  stoweidlem1  46573  stoweidlem7  46579  stoweidlem11  46583  stoweidlem25  46597  stoweidlem26  46598  stoweidlem34  46606  stoweidlem36  46608  stoweidlem41  46613  stoweidlem42  46614  stoweidlem44  46616  stoweidlem45  46617  wallispilem3  46639  wallispilem4  46640  wallispi  46642  stirlinglem3  46648  stirlinglem5  46650  stirlinglem6  46651  stirlinglem7  46652  stirlinglem10  46655  stirlinglem11  46656  stirlinglem12  46657  dirkeritg  46674  dirkercncflem2  46676  fourierdlem9  46688  fourierdlem11  46690  fourierdlem12  46691  fourierdlem14  46693  fourierdlem15  46694  fourierdlem19  46698  fourierdlem24  46703  fourierdlem28  46707  fourierdlem30  46709  fourierdlem40  46719  fourierdlem41  46720  fourierdlem43  46722  fourierdlem44  46723  fourierdlem47  46725  fourierdlem50  46728  fourierdlem51  46729  fourierdlem57  46735  fourierdlem60  46738  fourierdlem61  46739  fourierdlem66  46744  fourierdlem68  46746  fourierdlem73  46751  fourierdlem74  46752  fourierdlem75  46753  fourierdlem78  46756  fourierdlem79  46757  fourierdlem83  46761  fourierdlem88  46766  fourierdlem92  46770  fourierdlem93  46771  fourierdlem97  46775  fourierdlem103  46781  fourierdlem104  46782  fourierdlem109  46787  fourierdlem111  46789  sqwvfoura  46800  sqwvfourb  46801  fourierswlem  46802  fouriersw  46803  elaa2lem  46805  etransclem4  46810  etransclem18  46824  etransclem19  46825  etransclem23  46829  etransclem27  46833  etransclem31  46837  etransclem32  46838  etransclem35  46841  etransclem41  46847  etransclem46  46852  etransclem48  46854  rrxtopnfi  46859  qndenserrnbllem  46866  salgencntex  46915  sge0tsms  46952  sge0isum  46999  volicorecl  47118  hoiprodcl  47119  ovnlerp  47134  ovnsubaddlem1  47142  hoiprodcl3  47152  volicore  47153  hoidmvcl  47154  hoidmvlelem1  47167  hoidmvlelem2  47168  hoidmvlelem3  47169  ovnhoi  47175  hoiqssbllem2  47195  volicorege0  47209  vonhoire  47244  pimrecltpos  47280  pimrecltneg  47296  smfmbfcex  47332  nsssmfmbflem  47350  smfrec  47361  smfmullem3  47365  smfdivdmmbl  47410  sharhght  47437  et-sqrtnegnre  47445  ormkglobd  47449  natglobalincr  47451  chnsubseqwl  47453  zm1nn  47894  eluzge0nn0  47904  elfz2z  47907  2ffzoeq  47920  m1modmmod  47956  modm1p1ne  47968  muldvdsfacm1  47979  iccpartigtl  48027  iccpartgt  48031  nprmdvdsfacm1lem4  48230  requad01  48241  requad1  48242  requad2  48243  stgrusgra  48579  gpgedgvtx1  48682  expnegico01  49149  regt1loggt0  49167  refdivmptf  49173  elbigolo1  49188  rege1logbrege0  49189  fllog2  49199  dignn0flhalflem1  49246  eenglngeehlnmlem2  49369  line2  49383  line2xlem  49384  line2x  49385  line2y  49386  itsclc0yqsol  49395  2itscp  49412  inlinecirc02plem  49417  amgmwlem  50431