Theorem 0red 11147

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  0cc0 11038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811  df-rex 3062

This theorem is referenced by:  gt0ne0  11615  add20  11662  subge0  11663  lesub0  11667  mulge0  11668  msqgt0  11670  msqge0  11671  gt0ne0d  11714  addgt0d  11725  sublt0d  11776  prodgt0  12002  mulgt1  12017  lt2msq1  12040  fiminre2  12104  supmul1  12125  supmul  12128  nnne0  12211  0mnnnnn0  12469  nn0negleid  12489  neglt  12962  rpgecl  12972  ge0p1rp  12975  ledivge1le  13015  mul2lt0rlt0  13046  mul2lt0rgt0  13047  mul2lt0bi  13050  prodge0rd  13051  max0sub  13148  reltxrnmnf  13295  infmrp1  13297  lincmb01cmp  13448  iccf1o  13449  xov1plusxeqvd  13451  elfz0fzfz0  13587  fz0fzelfz0  13588  elfzo0z  13656  fzofzim  13664  fzo1fzo0n0  13670  elfzodifsumelfzo  13686  ssfzoulel  13715  elfznelfzo  13728  muladdmodid  13872  modltm1p1mod  13885  addmodlteq  13908  expgt1  14062  ltexp2a  14128  expcan  14131  ltexp2  14132  leexp2  14133  leexp2a  14134  zzlesq  14168  expnlbnd2  14196  discr  14202  fi1uzind  14469  ccatsymb  14545  ccat2s1fvw  14601  swrdnd  14617  swrdnnn0nd  14619  swrdswrdlem  14666  swrdswrd  14667  repswswrd  14746  swrd2lsw  14914  2swrd2eqwrdeq  14915  leabs  15261  max0add  15272  absgt0  15287  rlimrege0  15541  iseraltlem2  15645  fsumrecl  15696  o1fsum  15776  cvgcmp  15779  cvgcmpce  15781  geomulcvg  15841  mertenslem2  15850  fprodle  15961  rpnnen2lem4  16184  p1modz1  16228  moddvds  16232  oddge22np1  16318  bitsfzolem  16403  bitsinv1lem  16410  sadcaddlem  16426  nn0rppwr  16530  nn0expgcd  16533  lcmgcdlem  16575  dvdsnprmd  16659  2mulprm  16662  isprm7  16678  qnumgt0  16720  modprm0  16776  qexpz  16872  prmreclem4  16890  4sqlem6  16914  prmgaplem7  17028  gzrngunit  21413  regsumfsum  21415  regsumsupp  21602  fvmptnn04ifd  22818  chfacffsupp  22821  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulgsum  22829  prdsmet  24335  metustexhalf  24521  nlmvscnlem2  24650  nlmvscnlem1  24651  nmo0  24700  blcvx  24763  iihalf1cn  24899  evth  24926  lebnumlem1  24928  lebnumii  24933  htpycc  24947  pcohtpylem  24986  pcoass  24991  pcorevlem  24993  nmoleub2lem3  25082  ipcnlem2  25211  ipcnlem1  25212  rrxcph  25359  rrxmetlem  25374  rrxmet  25375  rrxdstprj1  25376  ehlbase  25382  minveclem3b  25395  minveclem6  25401  pjthlem1  25404  ovolicopnf  25491  ioorcl2  25539  volivth  25574  mbfposr  25619  i1fmulc  25670  itg1mulc  25671  itg1ge0a  25678  mbfi1flim  25690  itg2split  25716  itg2monolem1  25717  itg2monolem3  25719  itg2mono  25720  itg2cnlem2  25729  itgge0  25778  bddiblnc  25809  dvlip  25960  dvlipcn  25961  dveq0  25967  dv11cn  25968  dvlt0  25972  dvfsumge  25989  dgradd2  26233  plydivlem3  26261  mtest  26369  radcnvlem1  26378  radcnv0  26381  radcnvlt1  26383  radcnvle  26385  pserulm  26387  pserdvlem1  26392  pserdv  26394  abelthlem2  26397  abelthlem7  26403  pilem2  26417  pilem3  26418  coseq00topi  26466  tanabsge  26470  cosq34lt1  26491  tanord1  26501  tanord  26502  rplogcl  26568  logdivle  26586  logcnlem3  26608  logcnlem4  26609  dvloglem  26612  logtayl  26624  abscxp2  26657  cxplt  26658  cxple  26659  cxple2a  26663  cxpcn3lem  26711  abscxpbnd  26717  rtprmirr  26724  chordthmlem4  26799  chordthmlem5  26800  asinlem3  26835  atanre  26849  atanlogaddlem  26877  atanlogadd  26878  atanlogsublem  26879  atantan  26887  atans2  26895  efrlim  26933  cxp2limlem  26939  cxp2lim  26940  cxploglim2  26942  divsqrtsumlem  26943  jensenlem2  26951  harmonicubnd  26973  fsumharmonic  26975  dmlogdmgm  26987  lgamgulmlem1  26992  lgamgulmlem2  26993  ftalem1  27036  ftalem2  27037  ftalem5  27040  vmacl  27081  chtwordi  27119  ppiwordi  27125  chtrpcl  27138  fsumfldivdiaglem  27152  fsumvma2  27177  chpval2  27181  chpchtsum  27182  chpub  27183  logfacbnd3  27186  logexprlim  27188  mersenne  27190  lgsdilem  27287  lgsne0  27298  gausslemma2dlem1a  27328  lgseisen  27342  lgsquadlem1  27343  lgsquadlem2  27344  2sqmod  27399  2sqnn0  27401  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  chtppilimlem2  27437  chtppilim  27438  chebbnd2  27440  chto1lb  27441  chpchtlim  27442  chpo1ub  27443  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  dchrmusumlema  27456  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0re  27476  dchrisum0lema  27477  dchrisum0  27483  dirith2  27491  mulog2sumlem1  27497  vmalogdivsum2  27501  log2sumbnd  27507  selberg2lem  27513  chpdifbndlem1  27516  chpdifbnd  27518  selberg3lem1  27520  pntrmax  27527  pntrsumo1  27528  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntlemg  27561  pntlemj  27566  pntlemk  27569  pntlem3  27572  pnt2  27576  pnt  27577  ostth2lem1  27581  padicabv  27593  padicabvcxp  27595  ostth2lem3  27598  ostth2lem4  27599  ostth3  27601  trgcgrg  28583  tgcgr4  28599  axsegconlem7  28992  axsegconlem10  28995  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  axcontlem10  29042  crctcshwlkn0lem3  29880  crctcshwlkn0  29889  clwlkclwwlklem2a2  30063  clwlkclwwlklem2a  30068  wwlksubclwwlk  30128  frgrogt3nreg  30467  friendshipgt3  30468  minvecolem5  30952  minvecolem6  30953  htthlem  30988  pjhthlem1  31462  sgnval2  32808  nndiffz1  32859  bcm1n  32868  fzo0opth  32876  expgt0b  32890  sgnneg  32906  sgnmul  32908  sgnsub  32910  nexple  32917  oexpled  32920  indf1o  32924  wrdt2ind  33013  cycpmrn  33204  cyc3conja  33218  ccfldextdgrr  33816  constrsslem  33885  constrresqrtcl  33921  constrsqrtcl  33923  cos9thpiminplylem1  33926  pnfneige0  34095  measinb  34365  eulerpartlems  34504  eulerpartlemgc  34506  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemodife  34642  signsply0  34695  signslema  34706  signsvtp  34727  itgexpif  34750  breprexplemc  34776  circlemeth  34784  logdivsqrle  34794  0nn0m1nnn0  35295  cvmliftlem2  35468  dnibndlem9  36746  unbdqndv2lem2  36770  knoppndvlem1  36772  knoppndvlem2  36773  knoppndvlem7  36778  knoppndvlem11  36782  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem19  36790  knoppndvlem20  36791  bj-pinftynminfty  37541  poimirlem10  37951  poimirlem11  37952  poimirlem24  37965  poimirlem29  37970  poimirlem31  37972  poimirlem32  37973  poimir  37974  mblfinlem2  37979  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  areacirclem1  38029  areacirclem4  38032  areacirc  38034  geomcau  38080  isbnd3b  38106  prdsbnd  38114  bfp  38145  rrnequiv  38156  resdvopclptsd  42467  lcmineqlem2  42469  lcmineqlem3  42470  lcmineqlem10  42477  lcmineqlem12  42479  lcmineqlem23  42490  3lexlogpow5ineq1  42493  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow5ineq3  42496  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1lem1  42501  dvrelog2  42503  dvrelog3  42504  dvrelog2b  42505  0nonelalab  42506  dvrelogpow2b  42507  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8d2  42524  aks4d1p8d3  42525  aks4d1p8  42526  aks4d1p9  42527  posbezout  42539  primrootspoweq0  42545  aks6d1c1  42555  hashscontpow1  42560  aks6d1c2lem4  42566  aks6d1c5lem2  42577  deg1gprod  42579  2np3bcnp1  42583  2ap1caineq  42584  sticksstones7  42591  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  aks6d1c6lem3  42611  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  aks6d1c7lem2  42620  aks6d1c7  42623  aks5lem6  42631  unitscyglem5  42638  aks5lem8  42640  sn-1ne2  42703  oexpreposd  42754  posqsqznn  42768  redvmptabs  42792  readvrec  42794  re1m1e0m0  42829  re0m0e0  42834  remul01  42839  sn-remul0ord  42840  remulneg2d  42847  rediveq0d  42881  sn-rediv0d  42885  sn-addlt0d  42903  sn-addgt0d  42904  renegmulnnass  42910  zmulcomlem  42912  mulgt0con1dlem  42914  sn-mulgt1d  42924  mulltgt0d  42927  mullt0b2d  42929  sn-mullt0d  42930  sn-msqgt0d  42931  fimgmcyc  42979  dffltz  43067  3cubeslem1  43116  irrapxlem1  43250  irrapxlem2  43251  irrapxlem3  43252  irrapxlem4  43253  pellexlem6  43262  pell14qrgt0  43287  pell1qrgaplem  43301  pellfundex  43314  pellfundrp  43316  monotoddzzfi  43370  jm2.24  43391  jm2.23  43424  jm2.26lem3  43429  jm3.1lem3  43447  sqrtcvallem1  44058  reabsifneg  44059  reabsifpos  44061  sqrtcval  44068  k0004ss2  44579  imo72b2lem1  44596  dvgrat  44739  hashnzfz2  44748  binomcxplemnn0  44776  binomcxplemnotnn0  44783  divlt0gt0d  45719  upbdrech2  45741  xralrple2  45784  xralrple3  45803  reclt0d  45816  reclt0  45820  xrpnf  45913  fsumnncl  46002  fsumsupp0  46008  sumnnodd  46060  lptre2pt  46068  limsupubuz  46141  liminfresre  46207  liminf0  46221  dvmptconst  46343  dvdivbd  46351  dvcosax  46354  dvbdfbdioolem1  46356  dvbdfbdioolem2  46357  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvxpaek  46368  dvnxpaek  46370  volioc  46400  volico  46411  stoweidlem1  46429  stoweidlem7  46435  stoweidlem11  46439  stoweidlem25  46453  stoweidlem26  46454  stoweidlem34  46462  stoweidlem36  46464  stoweidlem41  46469  stoweidlem42  46470  stoweidlem44  46472  stoweidlem45  46473  wallispilem3  46495  wallispilem4  46496  wallispi  46498  stirlinglem3  46504  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem10  46511  stirlinglem11  46512  stirlinglem12  46513  dirkeritg  46530  dirkercncflem2  46532  fourierdlem9  46544  fourierdlem11  46546  fourierdlem12  46547  fourierdlem14  46549  fourierdlem15  46550  fourierdlem19  46554  fourierdlem24  46559  fourierdlem28  46563  fourierdlem30  46565  fourierdlem40  46575  fourierdlem41  46576  fourierdlem43  46578  fourierdlem44  46579  fourierdlem47  46581  fourierdlem50  46584  fourierdlem51  46585  fourierdlem57  46591  fourierdlem60  46594  fourierdlem61  46595  fourierdlem66  46600  fourierdlem68  46602  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem78  46612  fourierdlem79  46613  fourierdlem83  46617  fourierdlem88  46622  fourierdlem92  46626  fourierdlem93  46627  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem109  46643  fourierdlem111  46645  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  elaa2lem  46661  etransclem4  46666  etransclem18  46680  etransclem19  46681  etransclem23  46685  etransclem27  46689  etransclem31  46693  etransclem32  46694  etransclem35  46697  etransclem41  46703  etransclem46  46708  etransclem48  46710  rrxtopnfi  46715  qndenserrnbllem  46722  salgencntex  46771  sge0tsms  46808  sge0isum  46855  volicorecl  46974  hoiprodcl  46975  ovnlerp  46990  ovnsubaddlem1  46998  hoiprodcl3  47008  volicore  47009  hoidmvcl  47010  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoi  47031  hoiqssbllem2  47051  volicorege0  47065  vonhoire  47100  pimrecltpos  47136  pimrecltneg  47152  smfmbfcex  47188  nsssmfmbflem  47206  smfrec  47217  smfmullem3  47221  smfdivdmmbl  47266  sharhght  47293  et-sqrtnegnre  47301  ormkglobd  47305  natglobalincr  47307  chnsubseqwl  47309  zm1nn  47750  eluzge0nn0  47760  elfz2z  47763  2ffzoeq  47776  m1modmmod  47812  modm1p1ne  47824  muldvdsfacm1  47835  iccpartigtl  47883  iccpartgt  47887  nprmdvdsfacm1lem4  48086  requad01  48097  requad1  48098  requad2  48099  stgrusgra  48435  gpgedgvtx1  48538  expnegico01  48994  regt1loggt0  49012  refdivmptf  49018  elbigolo1  49033  rege1logbrege0  49034  fllog2  49044  dignn0flhalflem1  49091  eenglngeehlnmlem2  49214  line2  49228  line2xlem  49229  line2x  49230  line2y  49231  itsclc0yqsol  49240  2itscp  49257  inlinecirc02plem  49262  amgmwlem  50277