Theorem 0red 11112

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11002  0cc0 11003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11061  ax-addrcl 11064  ax-rnegex 11074  ax-cnre 11076

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-rex 3057

This theorem is referenced by:  gt0ne0  11579  add20  11626  subge0  11627  lesub0  11631  mulge0  11632  msqgt0  11634  msqge0  11635  gt0ne0d  11678  addgt0d  11689  sublt0d  11740  prodgt0  11965  mulgt1  11980  lt2msq1  12003  fiminre2  12067  supmul1  12088  supmul  12091  nnne0  12156  0mnnnnn0  12410  nn0negleid  12430  neglt  12907  rpgecl  12917  ge0p1rp  12920  ledivge1le  12960  mul2lt0rlt0  12991  mul2lt0rgt0  12992  mul2lt0bi  12995  prodge0rd  12996  max0sub  13092  reltxrnmnf  13239  infmrp1  13241  lincmb01cmp  13392  iccf1o  13393  xov1plusxeqvd  13395  elfz0fzfz0  13530  fz0fzelfz0  13531  elfzo0z  13598  fzofzim  13606  fzo1fzo0n0  13612  elfzodifsumelfzo  13628  ssfzoulel  13657  elfznelfzo  13670  muladdmodid  13814  modltm1p1mod  13827  addmodlteq  13850  expgt1  14004  ltexp2a  14070  expcan  14073  ltexp2  14074  leexp2  14075  leexp2a  14076  zzlesq  14110  expnlbnd2  14138  discr  14144  fi1uzind  14411  ccatsymb  14487  ccat2s1fvw  14543  swrdnd  14559  swrdnnn0nd  14561  swrdswrdlem  14608  swrdswrd  14609  repswswrd  14688  swrd2lsw  14856  2swrd2eqwrdeq  14857  leabs  15203  max0add  15214  absgt0  15229  rlimrege0  15483  iseraltlem2  15587  fsumrecl  15638  o1fsum  15717  cvgcmp  15720  cvgcmpce  15722  geomulcvg  15780  mertenslem2  15789  fprodle  15900  rpnnen2lem4  16123  p1modz1  16167  moddvds  16171  oddge22np1  16257  bitsfzolem  16342  bitsinv1lem  16349  sadcaddlem  16365  nn0rppwr  16469  nn0expgcd  16472  lcmgcdlem  16514  dvdsnprmd  16598  2mulprm  16601  isprm7  16616  qnumgt0  16658  modprm0  16714  qexpz  16810  prmreclem4  16828  4sqlem6  16852  prmgaplem7  16966  gzrngunit  21368  regsumfsum  21370  regsumsupp  21557  fvmptnn04ifd  22766  chfacffsupp  22769  chfacfscmul0  22771  chfacfscmulgsum  22773  chfacfpmmul0  22775  chfacfpmmulgsum  22777  prdsmet  24283  metustexhalf  24469  nlmvscnlem2  24598  nlmvscnlem1  24599  nmo0  24648  blcvx  24711  iihalf1cn  24851  evth  24883  lebnumlem1  24885  lebnumii  24890  htpycc  24904  pcohtpylem  24944  pcoass  24949  pcorevlem  24951  nmoleub2lem3  25040  ipcnlem2  25169  ipcnlem1  25170  rrxcph  25317  rrxmetlem  25332  rrxmet  25333  rrxdstprj1  25334  ehlbase  25340  minveclem3b  25353  minveclem6  25359  pjthlem1  25362  ovolicopnf  25450  ioorcl2  25498  volivth  25533  mbfposr  25578  i1fmulc  25629  itg1mulc  25630  itg1ge0a  25637  mbfi1flim  25649  itg2split  25675  itg2monolem1  25676  itg2monolem3  25678  itg2mono  25679  itg2cnlem2  25688  itgge0  25737  bddiblnc  25768  dvlip  25923  dvlipcn  25924  dveq0  25930  dv11cn  25931  dvlt0  25935  dvfsumge  25953  dgradd2  26199  plydivlem3  26228  mtest  26338  radcnvlem1  26347  radcnv0  26350  radcnvlt1  26352  radcnvle  26354  pserulm  26356  pserdvlem1  26362  pserdv  26364  abelthlem2  26367  abelthlem7  26373  pilem2  26387  pilem3  26388  coseq00topi  26436  tanabsge  26440  cosq34lt1  26461  tanord1  26471  tanord  26472  rplogcl  26538  logdivle  26556  logcnlem3  26578  logcnlem4  26579  dvloglem  26582  logtayl  26594  abscxp2  26627  cxplt  26628  cxple  26629  cxple2a  26633  cxpcn3lem  26682  abscxpbnd  26688  rtprmirr  26695  chordthmlem4  26770  chordthmlem5  26771  asinlem3  26806  atanre  26820  atanlogaddlem  26848  atanlogadd  26849  atanlogsublem  26850  atantan  26858  atans2  26866  efrlim  26904  efrlimOLD  26905  cxp2limlem  26911  cxp2lim  26912  cxploglim2  26914  divsqrtsumlem  26915  jensenlem2  26923  harmonicubnd  26945  fsumharmonic  26947  dmlogdmgm  26959  lgamgulmlem1  26964  lgamgulmlem2  26965  ftalem1  27008  ftalem2  27009  ftalem5  27012  vmacl  27053  chtwordi  27091  ppiwordi  27097  chtrpcl  27110  fsumfldivdiaglem  27124  fsumvma2  27150  chpval2  27154  chpchtsum  27155  chpub  27156  logfacbnd3  27159  logexprlim  27161  mersenne  27163  lgsdilem  27260  lgsne0  27271  gausslemma2dlem1a  27301  lgseisen  27315  lgsquadlem1  27316  lgsquadlem2  27317  2sqmod  27372  2sqnn0  27374  chebbnd1lem2  27406  chebbnd1lem3  27407  chebbnd1  27408  chtppilimlem1  27409  chtppilimlem2  27410  chtppilim  27411  chebbnd2  27413  chto1lb  27414  chpchtlim  27415  chpo1ub  27416  dchrisumlema  27424  dchrisumlem2  27426  dchrisumlem3  27427  dchrmusumlema  27429  dchrvmasumlem2  27434  dchrvmasumiflem1  27437  dchrisum0flblem1  27444  dchrisum0flblem2  27445  dchrisum0re  27449  dchrisum0lema  27450  dchrisum0  27456  dirith2  27464  mulog2sumlem1  27470  vmalogdivsum2  27474  log2sumbnd  27480  selberg2lem  27486  chpdifbndlem1  27489  chpdifbnd  27491  selberg3lem1  27493  pntrmax  27500  pntrsumo1  27501  pntrlog2bndlem4  27516  pntrlog2bndlem5  27517  pntpbnd1a  27521  pntpbnd1  27522  pntpbnd2  27523  pntlemg  27534  pntlemj  27539  pntlemk  27542  pntlem3  27545  pnt2  27549  pnt  27550  ostth2lem1  27554  padicabv  27566  padicabvcxp  27568  ostth2lem3  27571  ostth2lem4  27572  ostth3  27574  trgcgrg  28491  tgcgr4  28507  axsegconlem7  28899  axsegconlem10  28902  axcontlem2  28941  axcontlem4  28943  axcontlem7  28946  axcontlem10  28949  crctcshwlkn0lem3  29788  crctcshwlkn0  29797  clwlkclwwlklem2a2  29968  clwlkclwwlklem2a  29973  wwlksubclwwlk  30033  frgrogt3nreg  30372  friendshipgt3  30373  minvecolem5  30856  minvecolem6  30857  htthlem  30892  pjhthlem1  31366  sgnval2  32713  nndiffz1  32764  bcm1n  32772  fzo0opth  32780  expgt0b  32794  sgnneg  32811  sgnmul  32813  sgnsub  32815  nexple  32822  oexpled  32825  indf1o  32840  wrdt2ind  32929  cycpmrn  33107  cyc3conja  33121  ccfldextdgrr  33680  constrsslem  33749  constrresqrtcl  33785  constrsqrtcl  33787  cos9thpiminplylem1  33790  pnfneige0  33959  measinb  34229  eulerpartlems  34368  eulerpartlemgc  34370  ballotlemfc0  34501  ballotlemfcc  34502  ballotlemodife  34506  signsply0  34559  signslema  34570  signsvtp  34591  itgexpif  34614  breprexplemc  34640  circlemeth  34648  logdivsqrle  34658  0nn0m1nnn0  35145  cvmliftlem2  35318  dnibndlem9  36519  unbdqndv2lem2  36543  knoppndvlem1  36545  knoppndvlem2  36546  knoppndvlem7  36551  knoppndvlem11  36555  knoppndvlem14  36558  knoppndvlem15  36559  knoppndvlem17  36561  knoppndvlem19  36563  knoppndvlem20  36564  bj-pinftynminfty  37260  poimirlem10  37669  poimirlem11  37670  poimirlem24  37683  poimirlem29  37688  poimirlem31  37690  poimirlem32  37691  poimir  37692  mblfinlem2  37697  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  areacirclem1  37747  areacirclem4  37750  areacirc  37752  geomcau  37798  isbnd3b  37824  prdsbnd  37832  bfp  37863  rrnequiv  37874  resdvopclptsd  42060  lcmineqlem2  42062  lcmineqlem3  42063  lcmineqlem10  42070  lcmineqlem12  42072  lcmineqlem23  42083  3lexlogpow5ineq1  42086  3lexlogpow5ineq2  42087  3lexlogpow5ineq4  42088  3lexlogpow5ineq3  42089  3lexlogpow2ineq2  42091  3lexlogpow5ineq5  42092  aks4d1lem1  42094  dvrelog2  42096  dvrelog3  42097  dvrelog2b  42098  0nonelalab  42099  dvrelogpow2b  42100  aks4d1p1p3  42101  aks4d1p1p2  42102  aks4d1p1p4  42103  aks4d1p1p6  42105  aks4d1p1p7  42106  aks4d1p1p5  42107  aks4d1p1  42108  aks4d1p2  42109  aks4d1p3  42110  aks4d1p5  42112  aks4d1p6  42113  aks4d1p7d1  42114  aks4d1p7  42115  aks4d1p8d2  42117  aks4d1p8d3  42118  aks4d1p8  42119  aks4d1p9  42120  posbezout  42132  primrootspoweq0  42138  aks6d1c1  42148  hashscontpow1  42153  aks6d1c2lem4  42159  aks6d1c5lem2  42170  deg1gprod  42172  2np3bcnp1  42176  2ap1caineq  42177  sticksstones7  42184  sticksstones10  42187  sticksstones12a  42189  sticksstones12  42190  sticksstones22  42200  aks6d1c6lem3  42204  bcled  42210  bcle2d  42211  aks6d1c7lem1  42212  aks6d1c7lem2  42213  aks6d1c7  42216  aks5lem6  42224  unitscyglem5  42231  aks5lem8  42233  sn-1ne2  42297  oexpreposd  42354  posqsqznn  42368  redvmptabs  42392  readvrec  42394  re1m1e0m0  42429  re0m0e0  42434  remul01  42439  sn-remul0ord  42440  remulneg2d  42447  sn-addlt0d  42490  sn-addgt0d  42491  renegmulnnass  42497  zmulcomlem  42499  mulgt0con1dlem  42501  sn-mulgt1d  42511  mulltgt0d  42514  mullt0b2d  42516  sn-mullt0d  42517  sn-msqgt0d  42518  fimgmcyc  42566  dffltz  42666  3cubeslem1  42716  irrapxlem1  42854  irrapxlem2  42855  irrapxlem3  42856  irrapxlem4  42857  pellexlem6  42866  pell14qrgt0  42891  pell1qrgaplem  42905  pellfundex  42918  pellfundrp  42920  monotoddzzfi  42974  jm2.24  42995  jm2.23  43028  jm2.26lem3  43033  jm3.1lem3  43051  sqrtcvallem1  43663  reabsifneg  43664  reabsifpos  43666  sqrtcval  43673  k0004ss2  44184  imo72b2lem1  44201  dvgrat  44344  hashnzfz2  44353  binomcxplemnn0  44381  binomcxplemnotnn0  44388  divlt0gt0d  45326  upbdrech2  45348  xralrple2  45392  xralrple3  45411  reclt0d  45424  reclt0  45428  xrpnf  45522  fsumnncl  45611  fsumsupp0  45617  sumnnodd  45669  lptre2pt  45677  limsupubuz  45750  liminfresre  45816  liminf0  45830  dvmptconst  45952  dvdivbd  45960  dvcosax  45963  dvbdfbdioolem1  45965  dvbdfbdioolem2  45966  ioodvbdlimc1lem1  45968  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvxpaek  45977  dvnxpaek  45979  volioc  46009  volico  46020  stoweidlem1  46038  stoweidlem7  46044  stoweidlem11  46048  stoweidlem25  46062  stoweidlem26  46063  stoweidlem34  46071  stoweidlem36  46073  stoweidlem41  46078  stoweidlem42  46079  stoweidlem44  46081  stoweidlem45  46082  wallispilem3  46104  wallispilem4  46105  wallispi  46107  stirlinglem3  46113  stirlinglem5  46115  stirlinglem6  46116  stirlinglem7  46117  stirlinglem10  46120  stirlinglem11  46121  stirlinglem12  46122  dirkeritg  46139  dirkercncflem2  46141  fourierdlem9  46153  fourierdlem11  46155  fourierdlem12  46156  fourierdlem14  46158  fourierdlem15  46159  fourierdlem19  46163  fourierdlem24  46168  fourierdlem28  46172  fourierdlem30  46174  fourierdlem40  46184  fourierdlem41  46185  fourierdlem43  46187  fourierdlem44  46188  fourierdlem47  46190  fourierdlem50  46193  fourierdlem51  46194  fourierdlem57  46200  fourierdlem60  46203  fourierdlem61  46204  fourierdlem66  46209  fourierdlem68  46211  fourierdlem73  46216  fourierdlem74  46217  fourierdlem75  46218  fourierdlem78  46221  fourierdlem79  46222  fourierdlem83  46226  fourierdlem88  46231  fourierdlem92  46235  fourierdlem93  46236  fourierdlem97  46240  fourierdlem103  46246  fourierdlem104  46247  fourierdlem109  46252  fourierdlem111  46254  sqwvfoura  46265  sqwvfourb  46266  fourierswlem  46267  fouriersw  46268  elaa2lem  46270  etransclem4  46275  etransclem18  46289  etransclem19  46290  etransclem23  46294  etransclem27  46298  etransclem31  46302  etransclem32  46303  etransclem35  46306  etransclem41  46312  etransclem46  46317  etransclem48  46319  rrxtopnfi  46324  qndenserrnbllem  46331  salgencntex  46380  sge0tsms  46417  sge0isum  46464  volicorecl  46583  hoiprodcl  46584  ovnlerp  46599  ovnsubaddlem1  46607  hoiprodcl3  46617  volicore  46618  hoidmvcl  46619  hoidmvlelem1  46632  hoidmvlelem2  46633  hoidmvlelem3  46634  ovnhoi  46640  hoiqssbllem2  46660  volicorege0  46674  vonhoire  46709  pimrecltpos  46745  pimrecltneg  46761  smfmbfcex  46797  nsssmfmbflem  46815  smfrec  46826  smfmullem3  46830  smfdivdmmbl  46875  sharhght  46902  et-sqrtnegnre  46910  ormkglobd  46912  natglobalincr  46914  zm1nn  47332  eluzge0nn0  47342  elfz2z  47345  2ffzoeq  47357  m1modmmod  47388  modm1p1ne  47400  iccpartigtl  47453  iccpartgt  47457  requad01  47651  requad1  47652  requad2  47653  stgrusgra  47989  gpgedgvtx1  48092  expnegico01  48549  regt1loggt0  48567  refdivmptf  48573  elbigolo1  48588  rege1logbrege0  48589  fllog2  48599  dignn0flhalflem1  48646  eenglngeehlnmlem2  48769  line2  48783  line2xlem  48784  line2x  48785  line2y  48786  itsclc0yqsol  48795  2itscp  48812  inlinecirc02plem  48817  amgmwlem  49833