Theorem 0red 11243

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11133  0cc0 11134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-1cn 11192  ax-addrcl 11195  ax-rnegex 11205  ax-cnre 11207

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

This theorem is referenced by:  gt0ne0  11707  add20  11754  subge0  11755  lesub0  11759  mulge0  11760  msqgt0  11762  msqge0  11763  addgt0d  11817  sublt0d  11868  prodgt0  12093  mulgt1  12108  lt2msq1  12131  fiminre2  12195  supmul1  12216  supmul  12219  nnne0  12279  0mnnnnn0  12538  nn0negleid  12558  rpgecl  13042  ge0p1rp  13045  ledivge1le  13085  mul2lt0rlt0  13116  mul2lt0rgt0  13117  mul2lt0bi  13120  prodge0rd  13121  max0sub  13217  reltxrnmnf  13364  infmrp1  13366  lincmb01cmp  13517  iccf1o  13518  xov1plusxeqvd  13520  elfz0fzfz0  13655  fz0fzelfz0  13656  elfzo0z  13723  fzofzim  13731  fzo1fzo0n0  13736  elfzodifsumelfzo  13752  ssfzoulel  13781  elfznelfzo  13793  muladdmodid  13933  modltm1p1mod  13946  addmodlteq  13969  expgt1  14123  ltexp2a  14189  expcan  14192  ltexp2  14193  leexp2  14194  leexp2a  14195  zzlesq  14229  expnlbnd2  14257  discr  14263  fi1uzind  14530  ccatsymb  14605  ccat2s1fvw  14661  swrdnd  14677  swrdnnn0nd  14679  swrdswrdlem  14727  swrdswrd  14728  repswswrd  14807  swrd2lsw  14976  2swrd2eqwrdeq  14977  leabs  15323  max0add  15334  absgt0  15348  rlimrege0  15600  iseraltlem2  15704  fsumrecl  15755  o1fsum  15834  cvgcmp  15837  cvgcmpce  15839  geomulcvg  15897  mertenslem2  15906  fprodle  16017  rpnnen2lem4  16240  p1modz1  16284  moddvds  16288  oddge22np1  16373  bitsfzolem  16458  bitsinv1lem  16465  sadcaddlem  16481  nn0rppwr  16585  nn0expgcd  16588  lcmgcdlem  16630  dvdsnprmd  16714  2mulprm  16717  isprm7  16732  qnumgt0  16774  modprm0  16830  qexpz  16926  prmreclem4  16944  4sqlem6  16968  prmgaplem7  17082  gzrngunit  21406  regsumfsum  21408  regsumsupp  21587  fvmptnn04ifd  22796  chfacffsupp  22799  chfacfscmul0  22801  chfacfscmulgsum  22803  chfacfpmmul0  22805  chfacfpmmulgsum  22807  prdsmet  24314  metustexhalf  24500  nlmvscnlem2  24629  nlmvscnlem1  24630  nmo0  24679  blcvx  24742  iihalf1cn  24882  evth  24914  lebnumlem1  24916  lebnumii  24921  htpycc  24935  pcohtpylem  24975  pcoass  24980  pcorevlem  24982  nmoleub2lem3  25071  ipcnlem2  25201  ipcnlem1  25202  rrxcph  25349  rrxmetlem  25364  rrxmet  25365  rrxdstprj1  25366  ehlbase  25372  minveclem3b  25385  minveclem6  25391  pjthlem1  25394  ovolicopnf  25482  ioorcl2  25530  volivth  25565  mbfposr  25610  i1fmulc  25661  itg1mulc  25662  itg1ge0a  25669  mbfi1flim  25681  itg2split  25707  itg2monolem1  25708  itg2monolem3  25710  itg2mono  25711  itg2cnlem2  25720  itgge0  25769  bddiblnc  25800  dvlip  25955  dvlipcn  25956  dveq0  25962  dv11cn  25963  dvlt0  25967  dvfsumge  25985  dgradd2  26231  plydivlem3  26260  mtest  26370  radcnvlem1  26379  radcnv0  26382  radcnvlt1  26384  radcnvle  26386  pserulm  26388  pserdvlem1  26394  pserdv  26396  abelthlem2  26399  abelthlem7  26405  pilem2  26419  pilem3  26420  coseq00topi  26468  tanabsge  26472  cosq34lt1  26493  tanord1  26503  tanord  26504  rplogcl  26570  logdivle  26588  logcnlem3  26610  logcnlem4  26611  dvloglem  26614  logtayl  26626  abscxp2  26659  cxplt  26660  cxple  26661  cxple2a  26665  cxpcn3lem  26714  abscxpbnd  26720  rtprmirr  26727  chordthmlem4  26802  chordthmlem5  26803  asinlem3  26838  atanre  26852  atanlogaddlem  26880  atanlogadd  26881  atanlogsublem  26882  atantan  26890  atans2  26898  efrlim  26936  efrlimOLD  26937  cxp2limlem  26943  cxp2lim  26944  cxploglim2  26946  divsqrtsumlem  26947  jensenlem2  26955  harmonicubnd  26977  fsumharmonic  26979  dmlogdmgm  26991  lgamgulmlem1  26996  lgamgulmlem2  26997  ftalem1  27040  ftalem2  27041  ftalem5  27044  vmacl  27085  chtwordi  27123  ppiwordi  27129  chtrpcl  27142  fsumfldivdiaglem  27156  fsumvma2  27182  chpval2  27186  chpchtsum  27187  chpub  27188  logfacbnd3  27191  logexprlim  27193  mersenne  27195  lgsdilem  27292  lgsne0  27303  gausslemma2dlem1a  27333  lgseisen  27347  lgsquadlem1  27348  lgsquadlem2  27349  2sqmod  27404  2sqnn0  27406  chebbnd1lem2  27438  chebbnd1lem3  27439  chebbnd1  27440  chtppilimlem1  27441  chtppilimlem2  27442  chtppilim  27443  chebbnd2  27445  chto1lb  27446  chpchtlim  27447  chpo1ub  27448  dchrisumlema  27456  dchrisumlem2  27458  dchrisumlem3  27459  dchrmusumlema  27461  dchrvmasumlem2  27466  dchrvmasumiflem1  27469  dchrisum0flblem1  27476  dchrisum0flblem2  27477  dchrisum0re  27481  dchrisum0lema  27482  dchrisum0  27488  dirith2  27496  mulog2sumlem1  27502  vmalogdivsum2  27506  log2sumbnd  27512  selberg2lem  27518  chpdifbndlem1  27521  chpdifbnd  27523  selberg3lem1  27525  pntrmax  27532  pntrsumo1  27533  pntrlog2bndlem4  27548  pntrlog2bndlem5  27549  pntpbnd1a  27553  pntpbnd1  27554  pntpbnd2  27555  pntlemg  27566  pntlemj  27571  pntlemk  27574  pntlem3  27577  pnt2  27581  pnt  27582  ostth2lem1  27586  padicabv  27598  padicabvcxp  27600  ostth2lem3  27603  ostth2lem4  27604  ostth3  27606  trgcgrg  28499  tgcgr4  28515  axsegconlem7  28907  axsegconlem10  28910  axcontlem2  28949  axcontlem4  28951  axcontlem7  28954  axcontlem10  28957  crctcshwlkn0lem3  29799  crctcshwlkn0  29808  clwlkclwwlklem2a2  29979  clwlkclwwlklem2a  29984  wwlksubclwwlk  30044  frgrogt3nreg  30383  friendshipgt3  30384  minvecolem5  30867  minvecolem6  30868  htthlem  30903  pjhthlem1  31377  sgnval2  32717  nndiffz1  32768  bcm1n  32777  fzo0opth  32787  expgt0b  32800  sgnneg  32817  sgnmul  32819  sgnsub  32821  nexple  32828  oexpled  32831  indf1o  32846  wrdt2ind  32934  cycpmrn  33159  cyc3conja  33173  ccfldextdgrr  33718  constrsslem  33780  constrresqrtcl  33816  constrsqrtcl  33818  cos9thpiminplylem1  33821  pnfneige0  33987  measinb  34257  eulerpartlems  34397  eulerpartlemgc  34399  ballotlemfc0  34530  ballotlemfcc  34531  ballotlemodife  34535  signsply0  34588  signslema  34599  signsvtp  34620  itgexpif  34643  breprexplemc  34669  circlemeth  34677  logdivsqrle  34687  0nn0m1nnn0  35140  cvmliftlem2  35313  dnibndlem9  36509  unbdqndv2lem2  36533  knoppndvlem1  36535  knoppndvlem2  36536  knoppndvlem7  36541  knoppndvlem11  36545  knoppndvlem14  36548  knoppndvlem15  36549  knoppndvlem17  36551  knoppndvlem19  36553  knoppndvlem20  36554  bj-pinftynminfty  37250  poimirlem10  37659  poimirlem11  37660  poimirlem24  37673  poimirlem29  37678  poimirlem31  37680  poimirlem32  37681  poimir  37682  mblfinlem2  37687  ftc1anclem7  37728  ftc1anclem8  37729  ftc1anc  37730  areacirclem1  37737  areacirclem4  37740  areacirc  37742  geomcau  37788  isbnd3b  37814  prdsbnd  37822  bfp  37853  rrnequiv  37864  resdvopclptsd  42046  lcmineqlem2  42048  lcmineqlem3  42049  lcmineqlem10  42056  lcmineqlem12  42058  lcmineqlem23  42069  3lexlogpow5ineq1  42072  3lexlogpow5ineq2  42073  3lexlogpow5ineq4  42074  3lexlogpow5ineq3  42075  3lexlogpow2ineq2  42077  3lexlogpow5ineq5  42078  aks4d1lem1  42080  dvrelog2  42082  dvrelog3  42083  dvrelog2b  42084  0nonelalab  42085  dvrelogpow2b  42086  aks4d1p1p3  42087  aks4d1p1p2  42088  aks4d1p1p4  42089  aks4d1p1p6  42091  aks4d1p1p7  42092  aks4d1p1p5  42093  aks4d1p1  42094  aks4d1p2  42095  aks4d1p3  42096  aks4d1p5  42098  aks4d1p6  42099  aks4d1p7d1  42100  aks4d1p7  42101  aks4d1p8d2  42103  aks4d1p8d3  42104  aks4d1p8  42105  aks4d1p9  42106  posbezout  42118  primrootspoweq0  42124  aks6d1c1  42134  hashscontpow1  42139  aks6d1c2lem4  42145  aks6d1c5lem2  42156  deg1gprod  42158  2np3bcnp1  42162  2ap1caineq  42163  sticksstones7  42170  sticksstones10  42173  sticksstones12a  42175  sticksstones12  42176  sticksstones22  42186  aks6d1c6lem3  42190  bcled  42196  bcle2d  42197  aks6d1c7lem1  42198  aks6d1c7lem2  42199  aks6d1c7  42202  aks5lem6  42210  unitscyglem5  42217  aks5lem8  42219  sn-1ne2  42283  oexpreposd  42340  posqsqznn  42354  redvmptabs  42378  readvrec  42380  re1m1e0m0  42415  re0m0e0  42420  remul01  42425  remulneg2d  42432  sn-addlt0d  42464  sn-addgt0d  42465  renegmulnnass  42471  zmulcomlem  42473  mulgt0con1dlem  42475  sn-mulgt1d  42483  fimgmcyc  42532  dffltz  42632  3cubeslem1  42682  irrapxlem1  42820  irrapxlem2  42821  irrapxlem3  42822  irrapxlem4  42823  pellexlem6  42832  pell14qrgt0  42857  pell1qrgaplem  42871  pellfundex  42884  pellfundrp  42886  monotoddzzfi  42941  jm2.24  42962  jm2.23  42995  jm2.26lem3  43000  jm3.1lem3  43018  sqrtcvallem1  43630  reabsifneg  43631  reabsifpos  43633  sqrtcval  43640  k0004ss2  44151  imo72b2lem1  44168  dvgrat  44311  hashnzfz2  44320  binomcxplemnn0  44348  binomcxplemnotnn0  44355  neglt  45293  divlt0gt0d  45295  upbdrech2  45317  xralrple2  45361  xralrple3  45381  reclt0d  45394  reclt0  45398  xrpnf  45492  fsumnncl  45581  fsumsupp0  45587  sumnnodd  45639  lptre2pt  45649  limsupubuz  45722  liminfresre  45788  liminf0  45802  dvmptconst  45924  dvdivbd  45932  dvcosax  45935  dvbdfbdioolem1  45937  dvbdfbdioolem2  45938  ioodvbdlimc1lem1  45940  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  dvxpaek  45949  dvnxpaek  45951  volioc  45981  volico  45992  stoweidlem1  46010  stoweidlem7  46016  stoweidlem11  46020  stoweidlem25  46034  stoweidlem26  46035  stoweidlem34  46043  stoweidlem36  46045  stoweidlem41  46050  stoweidlem42  46051  stoweidlem44  46053  stoweidlem45  46054  wallispilem3  46076  wallispilem4  46077  wallispi  46079  stirlinglem3  46085  stirlinglem5  46087  stirlinglem6  46088  stirlinglem7  46089  stirlinglem10  46092  stirlinglem11  46093  stirlinglem12  46094  dirkeritg  46111  dirkercncflem2  46113  fourierdlem9  46125  fourierdlem11  46127  fourierdlem12  46128  fourierdlem14  46130  fourierdlem15  46131  fourierdlem19  46135  fourierdlem24  46140  fourierdlem28  46144  fourierdlem30  46146  fourierdlem40  46156  fourierdlem41  46157  fourierdlem43  46159  fourierdlem44  46160  fourierdlem47  46162  fourierdlem50  46165  fourierdlem51  46166  fourierdlem57  46172  fourierdlem60  46175  fourierdlem61  46176  fourierdlem66  46181  fourierdlem68  46183  fourierdlem73  46188  fourierdlem74  46189  fourierdlem75  46190  fourierdlem78  46193  fourierdlem79  46194  fourierdlem83  46198  fourierdlem88  46203  fourierdlem92  46207  fourierdlem93  46208  fourierdlem97  46212  fourierdlem103  46218  fourierdlem104  46219  fourierdlem109  46224  fourierdlem111  46226  sqwvfoura  46237  sqwvfourb  46238  fourierswlem  46239  fouriersw  46240  elaa2lem  46242  etransclem4  46247  etransclem18  46261  etransclem19  46262  etransclem23  46266  etransclem27  46270  etransclem31  46274  etransclem32  46275  etransclem35  46278  etransclem41  46284  etransclem46  46289  etransclem48  46291  rrxtopnfi  46296  qndenserrnbllem  46303  salgencntex  46352  sge0tsms  46389  sge0isum  46436  volicorecl  46555  hoiprodcl  46556  ovnlerp  46571  ovnsubaddlem1  46579  hoiprodcl3  46589  volicore  46590  hoidmvcl  46591  hoidmvlelem1  46604  hoidmvlelem2  46605  hoidmvlelem3  46606  ovnhoi  46612  hoiqssbllem2  46632  volicorege0  46646  vonhoire  46681  pimrecltpos  46717  pimrecltneg  46733  smfmbfcex  46769  nsssmfmbflem  46787  smfrec  46798  smfmullem3  46802  smfdivdmmbl  46847  sharhght  46874  et-sqrtnegnre  46882  ormkglobd  46884  natglobalincr  46886  upwordnul  46889  zm1nn  47311  eluzge0nn0  47321  elfz2z  47324  2ffzoeq  47336  iccpartigtl  47417  iccpartgt  47421  requad01  47615  requad1  47616  requad2  47617  stgrusgra  47951  gpgedgvtx1  48046  expnegico01  48474  m1modmmod  48481  difmodm1lt  48482  regt1loggt0  48496  refdivmptf  48502  elbigolo1  48517  rege1logbrege0  48518  fllog2  48528  dignn0flhalflem1  48575  eenglngeehlnmlem2  48698  line2  48712  line2xlem  48713  line2x  48714  line2y  48715  itsclc0yqsol  48724  2itscp  48741  inlinecirc02plem  48746  amgmwlem  49646