Theorem 0red 11215

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

Syntax hints:   → wi 4   ∈ wcel 2098  ℝcr 11106  0cc0 11107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-1cn 11165  ax-addrcl 11168  ax-rnegex 11178  ax-cnre 11180

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-clel 2802  df-rex 3063

This theorem is referenced by:  gt0ne0  11677  add20  11724  subge0  11725  lesub0  11729  mulge0  11730  msqgt0  11732  msqge0  11733  addgt0d  11787  sublt0d  11838  prodgt0  12059  lt2msq1  12096  fiminre2  12160  supmul1  12181  supmul  12184  nnne0  12244  0mnnnnn0  12502  nn0negleid  12522  rpgecl  13000  ge0p1rp  13003  ledivge1le  13043  mul2lt0rlt0  13074  mul2lt0rgt0  13075  mul2lt0bi  13078  prodge0rd  13079  max0sub  13173  reltxrnmnf  13319  infmrp1  13321  lincmb01cmp  13470  iccf1o  13471  xov1plusxeqvd  13473  elfz0fzfz0  13604  fz0fzelfz0  13605  elfzo0z  13672  fzofzim  13677  fzo1fzo0n0  13681  elfzodifsumelfzo  13696  ssfzoulel  13724  elfznelfzo  13735  muladdmodid  13874  modltm1p1mod  13886  addmodlteq  13909  expgt1  14064  ltexp2a  14129  expcan  14132  ltexp2  14133  leexp2  14134  leexp2a  14135  zzlesq  14168  expnlbnd2  14195  discr  14201  fi1uzind  14456  ccatsymb  14530  ccat2s1fvw  14586  swrdnd  14602  swrdnnn0nd  14604  swrdswrdlem  14652  swrdswrd  14653  repswswrd  14732  swrd2lsw  14901  2swrd2eqwrdeq  14902  leabs  15244  max0add  15255  absgt0  15269  rlimrege0  15521  iseraltlem2  15627  fsumrecl  15678  o1fsum  15757  cvgcmp  15760  cvgcmpce  15762  geomulcvg  15820  mertenslem2  15829  fprodle  15938  rpnnen2lem4  16159  p1modz1  16203  moddvds  16207  oddge22np1  16291  bitsfzolem  16374  bitsinv1lem  16381  sadcaddlem  16397  lcmgcdlem  16542  dvdsnprmd  16626  2mulprm  16629  isprm7  16644  qnumgt0  16687  modprm0  16739  qexpz  16835  prmreclem4  16853  4sqlem6  16877  prmgaplem7  16991  gzrngunit  21297  regsumfsum  21299  regsumsupp  21485  fvmptnn04ifd  22679  chfacffsupp  22682  chfacfscmul0  22684  chfacfscmulgsum  22686  chfacfpmmul0  22688  chfacfpmmulgsum  22690  prdsmet  24200  metustexhalf  24389  nlmvscnlem2  24526  nlmvscnlem1  24527  nmo0  24576  blcvx  24638  iihalf1cn  24777  evth  24809  lebnumlem1  24811  lebnumii  24816  htpycc  24830  pcohtpylem  24870  pcoass  24875  pcorevlem  24877  nmoleub2lem3  24966  ipcnlem2  25096  ipcnlem1  25097  rrxcph  25244  rrxmetlem  25259  rrxmet  25260  rrxdstprj1  25261  ehlbase  25267  minveclem3b  25280  minveclem6  25286  pjthlem1  25289  ovolicopnf  25377  ioorcl2  25425  volivth  25460  mbfposr  25505  i1fmulc  25557  itg1mulc  25558  itg1ge0a  25565  mbfi1flim  25577  itg2split  25603  itg2monolem1  25604  itg2monolem3  25606  itg2mono  25607  itg2cnlem2  25616  itgge0  25664  bddiblnc  25695  dvlip  25850  dvlipcn  25851  dveq0  25857  dv11cn  25858  dvlt0  25862  dvfsumge  25880  dgradd2  26125  plydivlem3  26151  mtest  26259  radcnvlem1  26268  radcnv0  26271  radcnvlt1  26273  radcnvle  26275  pserulm  26277  pserdvlem1  26283  pserdv  26285  abelthlem2  26288  abelthlem7  26294  pilem2  26308  pilem3  26309  coseq00topi  26356  tanabsge  26360  cosq34lt1  26380  tanord1  26390  tanord  26391  rplogcl  26457  logdivle  26475  logcnlem3  26497  logcnlem4  26498  dvloglem  26501  logtayl  26513  abscxp2  26546  cxplt  26547  cxple  26548  cxple2a  26552  cxpcn3lem  26601  abscxpbnd  26607  chordthmlem4  26686  chordthmlem5  26687  asinlem3  26722  atanre  26736  atanlogaddlem  26764  atanlogadd  26765  atanlogsublem  26766  atantan  26774  atans2  26782  efrlim  26820  efrlimOLD  26821  cxp2limlem  26827  cxp2lim  26828  cxploglim2  26830  divsqrtsumlem  26831  jensenlem2  26839  harmonicubnd  26861  fsumharmonic  26863  dmlogdmgm  26875  lgamgulmlem1  26880  lgamgulmlem2  26881  ftalem1  26924  ftalem2  26925  ftalem5  26928  vmacl  26969  chtwordi  27007  ppiwordi  27013  chtrpcl  27026  fsumfldivdiaglem  27040  fsumvma2  27066  chpval2  27070  chpchtsum  27071  chpub  27072  logfacbnd3  27075  logexprlim  27077  mersenne  27079  lgsdilem  27176  lgsne0  27187  gausslemma2dlem1a  27217  lgseisen  27231  lgsquadlem1  27232  lgsquadlem2  27233  2sqmod  27288  2sqnn0  27290  chebbnd1lem2  27322  chebbnd1lem3  27323  chebbnd1  27324  chtppilimlem1  27325  chtppilimlem2  27326  chtppilim  27327  chebbnd2  27329  chto1lb  27330  chpchtlim  27331  chpo1ub  27332  dchrisumlema  27340  dchrisumlem2  27342  dchrisumlem3  27343  dchrmusumlema  27345  dchrvmasumlem2  27350  dchrvmasumiflem1  27353  dchrisum0flblem1  27360  dchrisum0flblem2  27361  dchrisum0re  27365  dchrisum0lema  27366  dchrisum0  27372  dirith2  27380  mulog2sumlem1  27386  vmalogdivsum2  27390  log2sumbnd  27396  selberg2lem  27402  chpdifbndlem1  27405  chpdifbnd  27407  selberg3lem1  27409  pntrmax  27416  pntrsumo1  27417  pntrlog2bndlem4  27432  pntrlog2bndlem5  27433  pntpbnd1a  27437  pntpbnd1  27438  pntpbnd2  27439  pntlemg  27450  pntlemj  27455  pntlemk  27458  pntlem3  27461  pnt2  27465  pnt  27466  ostth2lem1  27470  padicabv  27482  padicabvcxp  27484  ostth2lem3  27487  ostth2lem4  27488  ostth3  27490  trgcgrg  28238  tgcgr4  28254  axsegconlem7  28653  axsegconlem10  28656  axcontlem2  28695  axcontlem4  28697  axcontlem7  28700  axcontlem10  28703  crctcshwlkn0lem3  29538  crctcshwlkn0  29547  clwlkclwwlklem2a2  29718  clwlkclwwlklem2a  29723  wwlksubclwwlk  29783  frgrogt3nreg  30122  friendshipgt3  30123  minvecolem5  30606  minvecolem6  30607  htthlem  30642  pjhthlem1  31116  nndiffz1  32469  bcm1n  32478  wrdt2ind  32587  cycpmrn  32773  cyc3conja  32787  ccfldextdgrr  33229  pnfneige0  33423  nexple  33499  indf1o  33514  measinb  33711  eulerpartlems  33851  eulerpartlemgc  33853  ballotlemfc0  33983  ballotlemfcc  33984  ballotlemodife  33988  sgnneg  34031  sgnmul  34033  sgnsub  34035  signsply0  34054  signslema  34065  signsvtp  34086  itgexpif  34109  breprexplemc  34135  circlemeth  34143  logdivsqrle  34153  0nn0m1nnn0  34593  cvmliftlem2  34768  dnibndlem9  35853  unbdqndv2lem2  35877  knoppndvlem1  35879  knoppndvlem2  35880  knoppndvlem7  35885  knoppndvlem11  35889  knoppndvlem14  35892  knoppndvlem15  35893  knoppndvlem17  35895  knoppndvlem19  35897  knoppndvlem20  35898  bj-pinftynminfty  36599  poimirlem10  36992  poimirlem11  36993  poimirlem24  37006  poimirlem29  37011  poimirlem31  37013  poimirlem32  37014  poimir  37015  mblfinlem2  37020  ftc1anclem7  37061  ftc1anclem8  37062  ftc1anc  37063  areacirclem1  37070  areacirclem4  37073  areacirc  37075  geomcau  37121  isbnd3b  37147  prdsbnd  37155  bfp  37186  rrnequiv  37197  resdvopclptsd  41390  lcmineqlem2  41392  lcmineqlem3  41393  lcmineqlem10  41400  lcmineqlem12  41402  lcmineqlem23  41413  3lexlogpow5ineq1  41416  3lexlogpow5ineq2  41417  3lexlogpow5ineq4  41418  3lexlogpow5ineq3  41419  3lexlogpow2ineq2  41421  3lexlogpow5ineq5  41422  aks4d1lem1  41424  dvrelog2  41426  dvrelog3  41427  dvrelog2b  41428  0nonelalab  41429  dvrelogpow2b  41430  aks4d1p1p3  41431  aks4d1p1p2  41432  aks4d1p1p4  41433  aks4d1p1p6  41435  aks4d1p1p7  41436  aks4d1p1p5  41437  aks4d1p1  41438  aks4d1p2  41439  aks4d1p3  41440  aks4d1p5  41442  aks4d1p6  41443  aks4d1p7d1  41444  aks4d1p7  41445  aks4d1p8d2  41447  aks4d1p8d3  41448  aks4d1p8  41449  aks4d1p9  41450  2np3bcnp1  41457  2ap1caineq  41458  sticksstones7  41465  sticksstones10  41468  sticksstones12a  41470  sticksstones12  41471  sticksstones22  41481  metakunt2  41483  metakunt29  41510  sn-1ne2  41672  oexpreposd  41713  nn0rppwr  41725  nn0expgcd  41727  posqsqznn  41735  rtprmirr  41738  re1m1e0m0  41784  re0m0e0  41789  remul01  41794  remulneg2d  41801  sn-addlt0d  41833  sn-addgt0d  41834  renegmulnnass  41840  zmulcomlem  41842  mulgt0con1dlem  41844  dffltz  41890  3cubeslem1  41936  irrapxlem1  42074  irrapxlem2  42075  irrapxlem3  42076  irrapxlem4  42077  pellexlem6  42086  pell14qrgt0  42111  pell1qrgaplem  42125  pellfundex  42138  pellfundrp  42140  monotoddzzfi  42195  jm2.24  42216  jm2.23  42249  jm2.26lem3  42254  jm3.1lem3  42272  sqrtcvallem1  42896  reabsifneg  42897  reabsifpos  42899  sqrtcval  42906  k0004ss2  43417  imo72b2lem1  43435  dvgrat  43585  hashnzfz2  43594  binomcxplemnn0  43622  binomcxplemnotnn0  43629  neglt  44504  divlt0gt0d  44506  upbdrech2  44528  xralrple2  44574  xralrple3  44594  reclt0d  44607  reclt0  44611  xrpnf  44706  fsumnncl  44798  fsumsupp0  44804  sumnnodd  44856  lptre2pt  44866  limsupubuz  44939  liminfresre  45005  liminf0  45019  dvmptconst  45141  dvdivbd  45149  dvcosax  45152  dvbdfbdioolem1  45154  dvbdfbdioolem2  45155  ioodvbdlimc1lem1  45157  ioodvbdlimc1lem2  45158  ioodvbdlimc2lem  45160  dvxpaek  45166  dvnxpaek  45168  volioc  45198  volico  45209  stoweidlem1  45227  stoweidlem7  45233  stoweidlem11  45237  stoweidlem25  45251  stoweidlem26  45252  stoweidlem34  45260  stoweidlem36  45262  stoweidlem41  45267  stoweidlem42  45268  stoweidlem44  45270  stoweidlem45  45271  wallispilem3  45293  wallispilem4  45294  wallispi  45296  stirlinglem3  45302  stirlinglem5  45304  stirlinglem6  45305  stirlinglem7  45306  stirlinglem10  45309  stirlinglem11  45310  stirlinglem12  45311  dirkeritg  45328  dirkercncflem2  45330  fourierdlem9  45342  fourierdlem11  45344  fourierdlem12  45345  fourierdlem14  45347  fourierdlem15  45348  fourierdlem19  45352  fourierdlem24  45357  fourierdlem28  45361  fourierdlem30  45363  fourierdlem40  45373  fourierdlem41  45374  fourierdlem43  45376  fourierdlem44  45377  fourierdlem47  45379  fourierdlem50  45382  fourierdlem51  45383  fourierdlem57  45389  fourierdlem60  45392  fourierdlem61  45393  fourierdlem66  45398  fourierdlem68  45400  fourierdlem73  45405  fourierdlem74  45406  fourierdlem75  45407  fourierdlem78  45410  fourierdlem79  45411  fourierdlem83  45415  fourierdlem88  45420  fourierdlem92  45424  fourierdlem93  45425  fourierdlem97  45429  fourierdlem103  45435  fourierdlem104  45436  fourierdlem109  45441  fourierdlem111  45443  sqwvfoura  45454  sqwvfourb  45455  fourierswlem  45456  fouriersw  45457  elaa2lem  45459  etransclem4  45464  etransclem18  45478  etransclem19  45479  etransclem23  45483  etransclem27  45487  etransclem31  45491  etransclem32  45492  etransclem35  45495  etransclem41  45501  etransclem46  45506  etransclem48  45508  rrxtopnfi  45513  qndenserrnbllem  45520  salgencntex  45569  sge0tsms  45606  sge0isum  45653  volicorecl  45772  hoiprodcl  45773  ovnlerp  45788  ovnsubaddlem1  45796  hoiprodcl3  45806  volicore  45807  hoidmvcl  45808  hoidmvlelem1  45821  hoidmvlelem2  45822  hoidmvlelem3  45823  ovnhoi  45829  hoiqssbllem2  45849  volicorege0  45863  vonhoire  45898  pimrecltpos  45934  pimrecltneg  45950  smfmbfcex  45986  nsssmfmbflem  46004  smfrec  46015  smfmullem3  46019  smfdivdmmbl  46064  sharhght  46091  et-sqrtnegnre  46099  natglobalincr  46101  upwordnul  46104  zm1nn  46520  eluzge0nn0  46530  elfz2z  46533  2ffzoeq  46546  iccpartigtl  46601  iccpartgt  46605  requad01  46799  requad1  46800  requad2  46801  expnegico01  47412  m1modmmod  47420  difmodm1lt  47421  regt1loggt0  47435  refdivmptf  47441  elbigolo1  47456  rege1logbrege0  47457  fllog2  47467  dignn0flhalflem1  47514  eenglngeehlnmlem2  47637  line2  47651  line2xlem  47652  line2x  47653  line2y  47654  itsclc0yqsol  47663  2itscp  47680  inlinecirc02plem  47685  amgmwlem  48061