Theorem 0red 11229

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 11228	. 2 ⊢ 0 ∈ ℝ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11117  0cc0 11118

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176  ax-addrcl 11179  ax-rnegex 11189  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-clel 2841  df-rex 3093

This theorem is used by:  gt0ne0  11697  add20  11744  subge0  11745  lesub0  11749  mulge0  11750  msqgt0  11752  msqge0  11753  gt0ne0d  11796  addgt0d  11807  sublt0d  11858  prodgt0  12080  mulgt1  12094  lt2msq1  12117  fiminre2  12181  supmul1  12202  supmul  12205  nnne0  12288  0mnnnnn0  12554  nn0negleid  12574  neglt  13054  rpgecl  13064  ge0p1rp  13067  ledivge1le  13107  mul2lt0rlt0  13138  mul2lt0rgt0  13139  mul2lt0bi  13142  prodge0rd  13143  max0sub  13240  reltxrnmnf  13387  infmrp1  13389  lincmb01cmp  13540  iccf1o  13541  xov1plusxeqvd  13543  elfz0fzfz0  13680  fz0fzelfz0  13681  elfzo0z  13749  fzofzim  13757  fzo1fzo0n0  13763  elfzodifsumelfzo  13779  ssfzoulel  13808  elfznelfzo  13821  muladdmodid  13966  modltm1p1mod  13979  addmodlteq  14002  expgt1  14156  ltexp2a  14222  expcan  14225  ltexp2  14226  leexp2  14227  leexp2a  14228  zzlesq  14262  expnlbnd2  14290  discr  14296  fi1uzind  14564  ccatsymb  14640  ccat2s1fvw  14698  swrdnd  14716  swrdnnn0nd  14718  swrdswrdlem  14765  swrdswrd  14766  repswswrd  14847  swrd2lsw  15015  2swrd2eqwrdeq  15016  sgnneg  15163  sgnsub  15169  sgnmul  15170  leabs  15376  max0add  15387  absgt0  15402  rlimrege0  15656  iseraltlem2  15760  fsumrecl  15811  o1fsum  15891  cvgcmp  15894  cvgcmpce  15896  geomulcvg  15956  mertenslem2  15965  fprodle  16076  rpnnen2lem4  16298  p1modz1  16342  moddvds  16346  oddge22np1  16432  bitsfzolem  16517  bitsinv1lem  16524  sadcaddlem  16540  nn0rppwr  16644  nn0expgcd  16647  lcmgcdlem  16689  dvdsnprmd  16773  2mulprm  16776  isprm7  16792  qnumgt0  16834  modprm0  16890  qexpz  16986  prmreclem4  17004  4sqlem6  17028  prmgaplem7  17142  gzrngunit  21620  regsumfsum  21622  regsumsupp  21809  fvmptnn04ifd  23047  chfacffsupp  23050  chfacfscmul0  23052  chfacfscmulgsum  23054  chfacfpmmul0  23056  chfacfpmmulgsum  23058  prdsmet  24564  metustexhalf  24750  nlmvscnlem2  24879  nlmvscnlem1  24880  nmo0  24929  blcvx  24992  iihalf1cn  25128  evth  25155  lebnumlem1  25157  lebnumii  25162  htpycc  25176  pcohtpylem  25215  pcoass  25220  pcorevlem  25222  nmoleub2lem3  25311  ipcnlem2  25440  ipcnlem1  25441  rrxcph  25588  rrxmetlem  25603  rrxmet  25604  rrxdstprj1  25605  ehlbase  25611  minveclem3b  25624  minveclem6  25630  pjthlem1  25633  ovolicopnf  25720  ioorcl2  25768  volivth  25803  mbfposr  25848  i1fmulc  25899  itg1mulc  25900  itg1ge0a  25907  mbfi1flim  25919  itg2split  25945  itg2monolem1  25946  itg2monolem3  25948  itg2mono  25949  itg2cnlem2  25958  itgge0  26007  bddiblnc  26038  dvlip  26189  dvlipcn  26190  dveq0  26196  dv11cn  26197  dvlt0  26201  dvfsumge  26218  dgradd2  26462  plydivlem3  26493  mtest  26604  radcnvlem1  26613  radcnv0  26616  radcnvlt1  26618  radcnvle  26620  pserulm  26622  pserdvlem1  26627  pserdv  26629  abelthlem2  26632  abelthlem7  26638  pilem2  26652  pilem3  26653  coseq00topi  26704  tanabsge  26708  cosq34lt1  26729  tanord1  26739  tanord  26740  rplogcl  26806  logdivle  26824  logcnlem3  26846  logcnlem4  26847  dvloglem  26850  logtayl  26862  abscxp2  26895  cxplt  26896  cxple  26897  cxple2a  26901  cxpcn3lem  26949  abscxpbnd  26955  rtprmirr  26962  chordthmlem4  27037  chordthmlem5  27038  asinlem3  27073  atanre  27087  atanlogaddlem  27115  atanlogadd  27116  atanlogsublem  27117  atantan  27125  atans2  27133  efrlim  27171  cxp2limlem  27177  cxp2lim  27178  cxploglim2  27180  divsqrtsumlem  27181  jensenlem2  27189  harmonicubnd  27211  fsumharmonic  27213  dmlogdmgm  27225  lgamgulmlem1  27230  lgamgulmlem2  27231  ftalem1  27274  ftalem2  27275  ftalem5  27278  vmacl  27319  chtwordi  27357  ppiwordi  27363  chtrpcl  27376  fsumfldivdiaglem  27390  fsumvma2  27415  chpval2  27419  chpchtsum  27420  chpub  27421  logfacbnd3  27424  logexprlim  27426  mersenne  27428  lgsdilem  27525  lgsne0  27536  gausslemma2dlem1a  27566  lgseisen  27580  lgsquadlem1  27581  lgsquadlem2  27582  2sqmod  27637  2sqnn0  27639  chebbnd1lem2  27671  chebbnd1lem3  27672  chebbnd1  27673  chtppilimlem1  27674  chtppilimlem2  27675  chtppilim  27676  chebbnd2  27678  chto1lb  27679  chpchtlim  27680  chpo1ub  27681  dchrisumlema  27689  dchrisumlem2  27691  dchrisumlem3  27692  dchrmusumlema  27694  dchrvmasumlem2  27699  dchrvmasumiflem1  27702  dchrisum0flblem1  27709  dchrisum0flblem2  27710  dchrisum0re  27714  dchrisum0lema  27715  dchrisum0  27721  dirith2  27729  mulog2sumlem1  27735  vmalogdivsum2  27739  log2sumbnd  27745  selberg2lem  27751  chpdifbndlem1  27754  chpdifbnd  27756  selberg3lem1  27758  pntrmax  27765  pntrsumo1  27766  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  pntpbnd1a  27786  pntpbnd1  27787  pntpbnd2  27788  pntlemg  27799  pntlemj  27804  pntlemk  27807  pntlem3  27810  pnt2  27814  pnt  27815  ostth2lem1  27819  padicabv  27831  padicabvcxp  27833  ostth2lem3  27836  ostth2lem4  27837  ostth3  27839  trgcgrg  28821  tgcgr4  28837  axsegconlem7  29310  axsegconlem10  29313  axcontlem2  29352  axcontlem4  29354  axcontlem7  29357  axcontlem10  29360  crctcshwlkn0lem3  30198  crctcshwlkn0  30207  clwlkclwwlklem2a2  30381  clwlkclwwlklem2a  30386  wwlksubclwwlk  30446  frgrogt3nreg  30785  friendshipgt3  30786  minvecolem5  31270  minvecolem6  31271  htthlem  31306  pjhthlem1  31780  sgnval2  33117  nndiffz1  33168  bcm1n  33177  fzo0opth  33185  expgt0b  33198  nexple  33214  oexpled  33217  indf1o  33221  wrdt2ind  33306  cycpmrn  33494  cyc3conja  33508  ccfldextdgrr  34093  constrsslem  34162  constrresqrtcl  34198  constrsqrtcl  34200  cos9thpiminplylem1  34203  pnfneige0  34372  measinb  34642  eulerpartlems  34781  eulerpartlemgc  34783  ballotlemfc0  34914  ballotlemfcc  34915  ballotlemodife  34919  signsply0  34969  signslema  34980  signsvtp  35001  itgexpif  35024  breprexplemc  35050  circlemeth  35058  logdivsqrle  35068  0nn0m1nnn0  35627  cvmliftlem2  35798  dnibndlem9  37115  unbdqndv2lem2  37139  knoppndvlem1  37141  knoppndvlem2  37142  knoppndvlem7  37147  knoppndvlem11  37151  knoppndvlem14  37154  knoppndvlem15  37155  knoppndvlem17  37157  knoppndvlem19  37159  knoppndvlem20  37160  bj-pinftynminfty  37911  poimirlem10  38321  poimirlem11  38322  poimirlem24  38335  poimirlem29  38340  poimirlem31  38342  poimirlem32  38343  poimir  38344  mblfinlem2  38349  ftc1anclem7  38390  ftc1anclem8  38391  ftc1anc  38392  areacirclem1  38399  areacirclem4  38402  areacirc  38404  geomcau  38450  isbnd3b  38476  prdsbnd  38484  bfp  38515  rrnequiv  38526  resdvopclptsd  42835  lcmineqlem2  42837  lcmineqlem3  42838  lcmineqlem10  42845  lcmineqlem12  42847  lcmineqlem23  42858  3lexlogpow5ineq1  42861  3lexlogpow5ineq2  42862  3lexlogpow5ineq4  42863  3lexlogpow5ineq3  42864  3lexlogpow2ineq2  42866  3lexlogpow5ineq5  42867  aks4d1lem1  42869  dvrelog2  42871  dvrelog3  42872  dvrelog2b  42873  0nonelalab  42874  dvrelogpow2b  42875  aks4d1p1p3  42876  aks4d1p1p2  42877  aks4d1p1p4  42878  aks4d1p1p6  42880  aks4d1p1p7  42881  aks4d1p1p5  42882  aks4d1p1  42883  aks4d1p2  42884  aks4d1p3  42885  aks4d1p5  42887  aks4d1p6  42888  aks4d1p7d1  42889  aks4d1p7  42890  aks4d1p8d2  42892  aks4d1p8d3  42893  aks4d1p8  42894  aks4d1p9  42895  posbezout  42907  primrootspoweq0  42913  aks6d1c1  42923  hashscontpow1  42928  aks6d1c2lem4  42934  aks6d1c5lem2  42945  deg1gprod  42947  2np3bcnp1  42951  2ap1caineq  42952  sticksstones7  42959  sticksstones10  42962  sticksstones12a  42964  sticksstones12  42965  sticksstones22  42975  aks6d1c6lem3  42979  bcled  42985  bcle2d  42986  aks6d1c7lem1  42987  aks6d1c7lem2  42988  aks6d1c7  42991  aks5lem6  42999  unitscyglem5  43006  aks5lem8  43008  sn-1ne2  43072  oexpreposd  43123  posqsqznn  43137  redvmptabs  43161  readvrec  43163  re1m1e0m0  43198  re0m0e0  43203  remul01  43208  sn-remul0ord  43209  remulneg2d  43216  rediveq0d  43250  sn-rediv0d  43254  sn-addlt0d  43272  sn-addgt0d  43273  renegmulnnass  43279  zmulcomlem  43281  mulgt0con1dlem  43283  sn-mulgt1d  43293  mulltgt0d  43296  mullt0b2d  43298  sn-mullt0d  43299  sn-msqgt0d  43300  fimgmcyc  43342  dffltz  43406  3cubeslem1  43455  irrapxlem1  43589  irrapxlem2  43590  irrapxlem3  43591  irrapxlem4  43592  pellexlem6  43601  pell14qrgt0  43626  pell1qrgaplem  43640  pellfundex  43653  pellfundrp  43655  monotoddzzfi  43709  jm2.24  43730  jm2.23  43763  jm2.26lem3  43768  jm3.1lem3  43786  sqrtcvallem1  44397  reabsifneg  44398  reabsifpos  44400  sqrtcval  44407  k0004ss2  44918  imo72b2lem1  44935  dvgrat  45062  hashnzfz2  45071  binomcxplemnn0  45099  binomcxplemnotnn0  45106  divlt0gt0d  46045  upbdrech2  46067  xralrple2  46110  xralrple3  46129  reclt0d  46142  reclt0  46146  xrpnf  46239  fsumnncl  46328  fsumsupp0  46334  sumnnodd  46386  lptre2pt  46394  limsupubuz  46467  liminfresre  46533  liminf0  46547  dvmptconst  46669  dvdivbd  46677  dvcosax  46680  dvbdfbdioolem1  46682  dvbdfbdioolem2  46683  ioodvbdlimc1lem1  46685  ioodvbdlimc1lem2  46686  ioodvbdlimc2lem  46688  dvxpaek  46694  dvnxpaek  46696  volioc  46726  volico  46737  stoweidlem1  46755  stoweidlem7  46761  stoweidlem11  46765  stoweidlem25  46779  stoweidlem26  46780  stoweidlem34  46788  stoweidlem36  46790  stoweidlem41  46795  stoweidlem42  46796  stoweidlem44  46798  stoweidlem45  46799  wallispilem3  46821  wallispilem4  46822  wallispi  46824  stirlinglem3  46830  stirlinglem5  46832  stirlinglem6  46833  stirlinglem7  46834  stirlinglem10  46837  stirlinglem11  46838  stirlinglem12  46839  dirkeritg  46856  dirkercncflem2  46858  fourierdlem9  46870  fourierdlem11  46872  fourierdlem12  46873  fourierdlem14  46875  fourierdlem15  46876  fourierdlem19  46880  fourierdlem24  46885  fourierdlem28  46889  fourierdlem30  46891  fourierdlem40  46901  fourierdlem41  46902  fourierdlem43  46904  fourierdlem44  46905  fourierdlem47  46907  fourierdlem50  46910  fourierdlem51  46911  fourierdlem57  46917  fourierdlem60  46920  fourierdlem61  46921  fourierdlem66  46926  fourierdlem68  46928  fourierdlem73  46933  fourierdlem74  46934  fourierdlem75  46935  fourierdlem78  46938  fourierdlem79  46939  fourierdlem83  46943  fourierdlem88  46948  fourierdlem92  46952  fourierdlem93  46953  fourierdlem97  46957  fourierdlem103  46963  fourierdlem104  46964  fourierdlem109  46969  fourierdlem111  46971  sqwvfoura  46982  sqwvfourb  46983  fourierswlem  46984  fouriersw  46985  elaa2lem  46987  etransclem4  46992  etransclem18  47006  etransclem19  47007  etransclem23  47011  etransclem27  47015  etransclem31  47019  etransclem32  47020  etransclem35  47023  etransclem41  47029  etransclem46  47034  etransclem48  47036  rrxtopnfi  47041  qndenserrnbllem  47048  salgencntex  47097  sge0tsms  47134  sge0isum  47181  volicorecl  47300  hoiprodcl  47301  ovnlerp  47316  ovnsubaddlem1  47324  hoiprodcl3  47334  volicore  47335  hoidmvcl  47336  hoidmvlelem1  47349  hoidmvlelem2  47350  hoidmvlelem3  47351  ovnhoi  47357  hoiqssbllem2  47377  volicorege0  47391  vonhoire  47426  pimrecltpos  47462  pimrecltneg  47478  smfmbfcex  47514  nsssmfmbflem  47532  smfrec  47543  smfmullem3  47547  smfdivdmmbl  47592  sharhght  47619  et-sqrtnegnre  47627  ormkglobd  47631  natglobalincr  47633  chnsubseqwl  47635  zm1nn  48079  eluzge0nn0  48089  elfz2z  48092  2ffzoeq  48105  m1modmmod  48141  modm1p1ne  48153  muldvdsfacm1  48164  iccpartigtl  48212  iccpartgt  48216  nprmdvdsfacm1lem4  48415  requad01  48426  requad1  48427  requad2  48428  stgrusgra  48764  gpgedgvtx1  48867  expnegico01  49338  regt1loggt0  49356  refdivmptf  49362  elbigolo1  49377  rege1logbrege0  49378  fllog2  49388  dignn0flhalflem1  49435  eenglngeehlnmlem2  49558  line2  49572  line2xlem  49573  line2x  49574  line2y  49575  itsclc0yqsol  49584  2itscp  49601  inlinecirc02plem  49606  amgmwlem  50690