Theorem 0red 11292

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11180  0cc0 11181

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 2147  ax-9 2155  ax-ext 2733  ax-1cn 11239  ax-addrcl 11242  ax-rnegex 11252  ax-cnre 11254

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-rex 3088

This theorem is used by:  gt0ne0  11762  add20  11809  subge0  11810  lesub0  11814  mulge0  11815  msqgt0  11817  msqge0  11818  gt0ne0d  11861  addgt0d  11872  sublt0d  11923  prodgt0  12145  mulgt1  12159  lt2msq1  12182  fiminre2  12246  supmul1  12267  supmul  12270  nnne0  12353  0mnnnnn0  12619  nn0negleid  12639  0nn0m1nnn0  12734  neglt  13121  rpgecl  13131  ge0p1rp  13134  ledivge1le  13174  mul2lt0rlt0  13205  mul2lt0rgt0  13206  mul2lt0bi  13209  prodge0rd  13210  max0sub  13307  reltxrnmnf  13454  infmrp1  13456  lincmb01cmp  13607  iccf1o  13608  xov1plusxeqvd  13610  elfz0fzfz0  13747  fz0fzelfz0  13748  elfzo0z  13816  fzofzim  13824  fzo1fzo0n0  13830  elfzodifsumelfzo  13846  ssfzoulel  13875  elfznelfzo  13888  muladdmodid  14033  modltm1p1mod  14046  addmodlteq  14069  expgt1  14223  ltexp2a  14289  expcan  14292  ltexp2  14293  leexp2  14294  leexp2a  14295  zzlesq  14330  expnlbnd2  14358  discr  14364  fi1uzind  14632  ccatsymb  14708  ccat2s1fvw  14766  swrdnd  14784  swrdnnn0nd  14786  swrdswrdlem  14833  swrdswrd  14834  repswswrd  14915  swrd2lsw  15085  2swrd2eqwrdeq  15086  sgnneg  15233  sgnsub  15239  sgnmul  15240  leabs  15446  max0add  15457  absgt0  15472  rlimrege0  15726  iseraltlem2  15830  fsumrecl  15880  o1fsum  15960  cvgcmp  15963  cvgcmpce  15965  geomulcvg  16025  mertenslem2  16034  fprodle  16143  rpnnen2lem4  16365  p1modz1  16409  moddvds  16413  oddge22np1  16499  bitsfzolem  16584  bitsinv1lem  16591  sadcaddlem  16607  nn0rppwr  16715  nn0expgcd  16718  lcmgcdlem  16761  dvdsnprmd  16845  2mulprm  16848  isprm7  16864  qnumgt0  16906  posqsqznn  16916  modprm0  16963  qexpz  17059  prmreclem4  17077  4sqlem6  17101  prmgaplem7  17215  gzrngunit  21719  regsumfsum  21721  regsumsupp  21908  fvmptnn04ifd  23151  chfacffsupp  23154  chfacfscmul0  23156  chfacfscmulgsum  23158  chfacfpmmul0  23160  chfacfpmmulgsum  23162  prdsmet  24669  metustexhalf  24855  nlmvscnlem2  24984  nlmvscnlem1  24985  nmo0  25034  blcvx  25097  iihalf1cn  25233  evth  25260  lebnumlem1  25262  lebnumii  25267  htpycc  25281  pcohtpylem  25320  pcoass  25325  pcorevlem  25327  nmoleub2lem3  25416  ipcnlem2  25545  ipcnlem1  25546  rrxcph  25693  rrxmetlem  25708  rrxmet  25709  rrxdstprj1  25710  ehlbase  25716  minveclem3b  25729  minveclem6  25735  pjthlem1  25738  ovolicopnf  25825  ioorcl2  25873  volivth  25908  mbfposr  25953  i1fmulc  26004  itg1mulc  26005  itg1ge0a  26012  mbfi1flim  26024  itg2split  26050  itg2monolem1  26051  itg2monolem3  26053  itg2mono  26054  itg2cnlem2  26063  itgge0  26111  bddiblnc  26142  dvlip  26293  dvlipcn  26294  dveq0  26300  dv11cn  26301  dvlt0  26305  dvfsumge  26322  dgradd2  26567  plydivlem3  26598  mtest  26713  radcnvlem1  26722  radcnv0  26725  radcnvlt1  26727  radcnvle  26729  pserulm  26731  pserdvlem1  26736  pserdv  26738  abelthlem2  26741  abelthlem7  26747  pilem2  26761  pilem3  26762  coseq00topi  26813  tanabsge  26817  cosq34lt1  26837  tanord1  26847  tanord  26848  rplogcl  26914  logdivle  26932  logcnlem3  26954  logcnlem4  26955  dvloglem  26958  logtayl  26970  abscxp2  27003  cxplt  27004  cxple  27005  cxple2a  27009  cxpcn3lem  27057  abscxpbnd  27063  rtprmirr  27070  chordthmlem4  27145  chordthmlem5  27146  asinlem3  27181  atanre  27195  atanlogaddlem  27223  atanlogadd  27224  atanlogsublem  27225  atantan  27233  atans2  27241  efrlim  27279  cxp2limlem  27285  cxp2lim  27286  cxploglim2  27288  divsqrtsumlem  27289  jensenlem2  27297  harmonicubnd  27319  fsumharmonic  27321  dmlogdmgm  27333  lgamgulmlem1  27338  lgamgulmlem2  27339  ftalem1  27382  ftalem2  27383  ftalem5  27386  vmacl  27427  chtwordi  27465  ppiwordi  27471  chtrpcl  27484  fsumfldivdiaglem  27498  fsumvma2  27523  chpval2  27527  chpchtsum  27528  chpub  27529  logfacbnd3  27532  logexprlim  27534  mersenne  27536  lgsdilem  27633  lgsne0  27644  gausslemma2dlem1a  27674  lgseisen  27688  lgsquadlem1  27689  lgsquadlem2  27690  2sqmod  27745  2sqnn0  27747  chebbnd1lem2  27779  chebbnd1lem3  27780  chebbnd1  27781  chtppilimlem1  27782  chtppilimlem2  27783  chtppilim  27784  chebbnd2  27786  chto1lb  27787  chpchtlim  27788  chpo1ub  27789  dchrisumlema  27797  dchrisumlem2  27799  dchrisumlem3  27800  dchrmusumlema  27802  dchrvmasumlem2  27807  dchrvmasumiflem1  27810  dchrisum0flblem1  27817  dchrisum0flblem2  27818  dchrisum0re  27822  dchrisum0lema  27823  dchrisum0  27829  dirith2  27837  mulog2sumlem1  27843  vmalogdivsum2  27847  log2sumbnd  27853  selberg2lem  27859  chpdifbndlem1  27862  chpdifbnd  27864  selberg3lem1  27866  pntrmax  27873  pntrsumo1  27874  pntrlog2bndlem4  27889  pntrlog2bndlem5  27890  pntpbnd1a  27894  pntpbnd1  27895  pntpbnd2  27896  pntlemg  27907  pntlemj  27912  pntlemk  27915  pntlem3  27918  pnt2  27922  pnt  27923  ostth2lem1  27927  padicabv  27939  padicabvcxp  27941  ostth2lem3  27944  ostth2lem4  27945  ostth3  27947  trgcgrg  28960  tgcgr4  28976  axsegconlem7  29483  axsegconlem10  29486  axcontlem2  29525  axcontlem4  29527  axcontlem7  29530  axcontlem10  29533  crctcshwlkn0lem3  30383  crctcshwlkn0  30392  clwlkclwwlklem2a2  30566  clwlkclwwlklem2a  30571  wwlksubclwwlk  30631  frgrogt3nreg  30980  friendshipgt3  30981  minvecolem5  31465  minvecolem6  31466  htthlem  31501  pjhthlem1  31975  sgnval2  33309  nndiffz1  33360  bcm1n  33369  fzo0opth  33377  expgt0b  33390  nexple  33406  oexpled  33409  indf1o  33413  wrdt2ind  33498  cycpmrn  33686  cyc3conja  33700  ccfldextdgrr  34286  constrsslem  34355  constrresqrtcl  34391  constrsqrtcl  34393  cos9thpiminplylem1  34396  pnfneige0  34565  measinb  34836  eulerpartlems  34975  eulerpartlemgc  34977  ballotlemfc0  35108  ballotlemfcc  35109  ballotlemodife  35113  signsply0  35163  signslema  35174  signsvtp  35195  itgexpif  35218  breprexplemc  35244  circlemeth  35252  logdivsqrle  35262  cvmliftlem2  36020  dnibndlem9  37322  unbdqndv2lem2  37346  knoppndvlem1  37348  knoppndvlem2  37349  knoppndvlem7  37354  knoppndvlem11  37358  knoppndvlem14  37361  knoppndvlem15  37362  knoppndvlem17  37364  knoppndvlem19  37366  knoppndvlem20  37367  bj-pinftynminfty  38116  poimirlem10  38516  poimirlem11  38517  poimirlem24  38530  poimirlem29  38535  poimirlem31  38537  poimirlem32  38538  poimir  38539  mblfinlem2  38544  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  areacirclem1  38594  areacirclem4  38597  areacirc  38599  geomcau  38661  isbnd3b  38687  prdsbnd  38695  bfp  38726  rrnequiv  38737  resdvopclptsd  43046  lcmineqlem2  43048  lcmineqlem3  43049  lcmineqlem10  43056  lcmineqlem12  43058  lcmineqlem23  43069  3lexlogpow5ineq1  43072  3lexlogpow5ineq2  43073  3lexlogpow5ineq4  43074  3lexlogpow5ineq3  43075  3lexlogpow2ineq2  43077  3lexlogpow5ineq5  43078  aks4d1lem1  43080  dvrelog2  43082  dvrelog3  43083  dvrelog2b  43084  0nonelalab  43085  dvrelogpow2b  43086  aks4d1p1p3  43087  aks4d1p1p2  43088  aks4d1p1p4  43089  aks4d1p1p6  43091  aks4d1p1p7  43092  aks4d1p1p5  43093  aks4d1p1  43094  aks4d1p2  43095  aks4d1p3  43096  aks4d1p5  43098  aks4d1p6  43099  aks4d1p7d1  43100  aks4d1p7  43101  aks4d1p8d2  43103  aks4d1p8d3  43104  aks4d1p8  43105  aks4d1p9  43106  posbezout  43118  primrootspoweq0  43124  aks6d1c1  43134  hashscontpow1  43139  aks6d1c2lem4  43145  aks6d1c5lem2  43156  deg1gprod  43158  2np3bcnp1  43162  2ap1caineq  43163  sticksstones7  43170  sticksstones10  43173  sticksstones12a  43175  sticksstones12  43176  sticksstones22  43186  aks6d1c6lem3  43190  bcled  43196  bcle2d  43197  aks6d1c7lem1  43198  aks6d1c7lem2  43199  aks6d1c7  43202  aks5lem6  43210  unitscyglem5  43217  aks5lem8  43219  sn-1ne2  43298  oexpreposd  43347  redvmptabs  43379  readvrec  43381  re1m1e0m0  43416  re0m0e0  43421  remul01  43426  sn-remul0ord  43427  remulneg2d  43434  rediveq0d  43468  sn-rediv0d  43472  sn-addlt0d  43490  sn-addgt0d  43491  renegmulnnass  43497  zmulcomlem  43499  mulgt0con1dlem  43501  sn-mulgt1d  43511  mulltgt0d  43514  mullt0b2d  43516  sn-mullt0d  43517  sn-msqgt0d  43518  fimgmcyc  43560  dffltz  43624  3cubeslem1  43648  irrapxlem1  43782  irrapxlem2  43783  irrapxlem3  43784  irrapxlem4  43785  pellexlem6  43794  pell14qrgt0  43819  pell1qrgaplem  43833  pellfundex  43846  pellfundrp  43848  monotoddzzfi  43902  jm2.24  43923  jm2.23  43956  jm2.26lem3  43961  jm3.1lem3  43979  sqrtcvallem1  44590  reabsifneg  44591  reabsifpos  44593  sqrtcval  44600  k0004ss2  45111  imo72b2lem1  45128  dvgrat  45255  hashnzfz2  45264  binomcxplemnn0  45292  binomcxplemnotnn0  45299  divlt0gt0d  46245  upbdrech2  46267  xralrple2  46310  xralrple3  46329  reclt0d  46342  reclt0  46346  xrpnf  46439  fsumnncl  46528  fsumsupp0  46534  sumnnodd  46586  lptre2pt  46594  limsupubuz  46667  liminfresre  46733  liminf0  46747  dvmptconst  46869  dvdivbd  46877  dvcosax  46880  dvbdfbdioolem1  46882  dvbdfbdioolem2  46883  ioodvbdlimc1lem1  46885  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  dvxpaek  46894  dvnxpaek  46896  volioc  46926  volico  46937  stoweidlem1  46955  stoweidlem7  46961  stoweidlem11  46965  stoweidlem25  46979  stoweidlem26  46980  stoweidlem34  46988  stoweidlem36  46990  stoweidlem41  46995  stoweidlem42  46996  stoweidlem44  46998  stoweidlem45  46999  wallispilem3  47021  wallispilem4  47022  wallispi  47024  stirlinglem3  47030  stirlinglem5  47032  stirlinglem6  47033  stirlinglem7  47034  stirlinglem10  47037  stirlinglem11  47038  stirlinglem12  47039  dirkeritg  47056  dirkercncflem2  47058  fourierdlem9  47070  fourierdlem11  47072  fourierdlem12  47073  fourierdlem14  47075  fourierdlem15  47076  fourierdlem19  47080  fourierdlem24  47085  fourierdlem28  47089  fourierdlem30  47091  fourierdlem40  47101  fourierdlem41  47102  fourierdlem43  47104  fourierdlem44  47105  fourierdlem47  47107  fourierdlem50  47110  fourierdlem51  47111  fourierdlem57  47117  fourierdlem60  47120  fourierdlem61  47121  fourierdlem66  47126  fourierdlem68  47128  fourierdlem73  47133  fourierdlem74  47134  fourierdlem75  47135  fourierdlem78  47138  fourierdlem79  47139  fourierdlem83  47143  fourierdlem88  47148  fourierdlem92  47152  fourierdlem93  47153  fourierdlem97  47157  fourierdlem103  47163  fourierdlem104  47164  fourierdlem109  47169  fourierdlem111  47171  sqwvfoura  47182  sqwvfourb  47183  fourierswlem  47184  fouriersw  47185  elaa2lem  47187  etransclem4  47192  etransclem18  47206  etransclem19  47207  etransclem23  47211  etransclem27  47215  etransclem31  47219  etransclem32  47220  etransclem35  47223  etransclem41  47229  etransclem46  47234  etransclem48  47236  rrxtopnfi  47241  qndenserrnbllem  47248  salgencntex  47297  sge0tsms  47334  sge0isum  47381  volicorecl  47500  hoiprodcl  47501  ovnlerp  47516  ovnsubaddlem1  47524  hoiprodcl3  47534  volicore  47535  hoidmvcl  47536  hoidmvlelem1  47549  hoidmvlelem2  47550  hoidmvlelem3  47551  ovnhoi  47557  hoiqssbllem2  47577  volicorege0  47591  vonhoire  47626  pimrecltpos  47662  pimrecltneg  47678  smfmbfcex  47714  nsssmfmbflem  47732  smfrec  47743  smfmullem3  47747  smfdivdmmbl  47792  sharhght  47819  et-sqrtnegnre  47827  ormkglobd  47831  chnsubseqwl  47833  zm1nn  48316  eluzge0nn0  48326  elfz2z  48329  2ffzoeq  48342  m1modmmod  48378  modm1p1ne  48390  muldvdsfacm1  48401  iccpartigtl  48449  iccpartgt  48453  nprmdvdsfacm1lem4  48652  requad01  48663  requad1  48664  requad2  48665  stgrusgra  49001  gpgedgvtx1  49104  expnegico01  49574  regt1loggt0  49592  refdivmptf  49598  elbigolo1  49613  rege1logbrege0  49614  fllog2  49624  dignn0flhalflem1  49671  eenglngeehlnmlem2  49794  line2  49808  line2xlem  49809  line2x  49810  line2y  49811  itsclc0yqsol  49820  2itscp  49837  inlinecirc02plem  49842  veronesefvcl  50916  veronesev1lem  50917  veronesev2lem  50918  veronesev3lem  50919  veronesev4lem  50920  veronesev5lem  50921  veronesev6lem  50922  amgmwlem  50931