Theorem 0red 11247

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11137  0cc0 11138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-1cn 11196  ax-addrcl 11199  ax-rnegex 11209  ax-cnre 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-clel 2808  df-rex 3060

This theorem is referenced by:  gt0ne0  11711  add20  11758  subge0  11759  lesub0  11763  mulge0  11764  msqgt0  11766  msqge0  11767  addgt0d  11821  sublt0d  11872  prodgt0  12097  mulgt1  12112  lt2msq1  12135  fiminre2  12199  supmul1  12220  supmul  12223  nnne0  12283  0mnnnnn0  12542  nn0negleid  12562  rpgecl  13046  ge0p1rp  13049  ledivge1le  13089  mul2lt0rlt0  13120  mul2lt0rgt0  13121  mul2lt0bi  13124  prodge0rd  13125  max0sub  13221  reltxrnmnf  13367  infmrp1  13369  lincmb01cmp  13518  iccf1o  13519  xov1plusxeqvd  13521  elfz0fzfz0  13656  fz0fzelfz0  13657  elfzo0z  13724  fzofzim  13732  fzo1fzo0n0  13737  elfzodifsumelfzo  13753  ssfzoulel  13782  elfznelfzo  13794  muladdmodid  13934  modltm1p1mod  13947  addmodlteq  13970  expgt1  14124  ltexp2a  14189  expcan  14192  ltexp2  14193  leexp2  14194  leexp2a  14195  zzlesq  14228  expnlbnd2  14256  discr  14262  fi1uzind  14529  ccatsymb  14603  ccat2s1fvw  14659  swrdnd  14675  swrdnnn0nd  14677  swrdswrdlem  14725  swrdswrd  14726  repswswrd  14805  swrd2lsw  14974  2swrd2eqwrdeq  14975  leabs  15321  max0add  15332  absgt0  15346  rlimrege0  15598  iseraltlem2  15702  fsumrecl  15753  o1fsum  15832  cvgcmp  15835  cvgcmpce  15837  geomulcvg  15895  mertenslem2  15904  fprodle  16015  rpnnen2lem4  16236  p1modz1  16280  moddvds  16284  oddge22np1  16369  bitsfzolem  16454  bitsinv1lem  16461  sadcaddlem  16477  nn0rppwr  16581  nn0expgcd  16584  lcmgcdlem  16626  dvdsnprmd  16710  2mulprm  16713  isprm7  16728  qnumgt0  16770  modprm0  16826  qexpz  16922  prmreclem4  16940  4sqlem6  16964  prmgaplem7  17078  gzrngunit  21418  regsumfsum  21420  regsumsupp  21607  fvmptnn04ifd  22826  chfacffsupp  22829  chfacfscmul0  22831  chfacfscmulgsum  22833  chfacfpmmul0  22835  chfacfpmmulgsum  22837  prdsmet  24344  metustexhalf  24532  nlmvscnlem2  24661  nlmvscnlem1  24662  nmo0  24711  blcvx  24774  iihalf1cn  24914  evth  24946  lebnumlem1  24948  lebnumii  24953  htpycc  24967  pcohtpylem  25007  pcoass  25012  pcorevlem  25014  nmoleub2lem3  25103  ipcnlem2  25233  ipcnlem1  25234  rrxcph  25381  rrxmetlem  25396  rrxmet  25397  rrxdstprj1  25398  ehlbase  25404  minveclem3b  25417  minveclem6  25423  pjthlem1  25426  ovolicopnf  25514  ioorcl2  25562  volivth  25597  mbfposr  25642  i1fmulc  25693  itg1mulc  25694  itg1ge0a  25701  mbfi1flim  25713  itg2split  25739  itg2monolem1  25740  itg2monolem3  25742  itg2mono  25743  itg2cnlem2  25752  itgge0  25801  bddiblnc  25832  dvlip  25987  dvlipcn  25988  dveq0  25994  dv11cn  25995  dvlt0  25999  dvfsumge  26017  dgradd2  26263  plydivlem3  26292  mtest  26402  radcnvlem1  26411  radcnv0  26414  radcnvlt1  26416  radcnvle  26418  pserulm  26420  pserdvlem1  26426  pserdv  26428  abelthlem2  26431  abelthlem7  26437  pilem2  26451  pilem3  26452  coseq00topi  26499  tanabsge  26503  cosq34lt1  26524  tanord1  26534  tanord  26535  rplogcl  26601  logdivle  26619  logcnlem3  26641  logcnlem4  26642  dvloglem  26645  logtayl  26657  abscxp2  26690  cxplt  26691  cxple  26692  cxple2a  26696  cxpcn3lem  26745  abscxpbnd  26751  rtprmirr  26758  chordthmlem4  26833  chordthmlem5  26834  asinlem3  26869  atanre  26883  atanlogaddlem  26911  atanlogadd  26912  atanlogsublem  26913  atantan  26921  atans2  26929  efrlim  26967  efrlimOLD  26968  cxp2limlem  26974  cxp2lim  26975  cxploglim2  26977  divsqrtsumlem  26978  jensenlem2  26986  harmonicubnd  27008  fsumharmonic  27010  dmlogdmgm  27022  lgamgulmlem1  27027  lgamgulmlem2  27028  ftalem1  27071  ftalem2  27072  ftalem5  27075  vmacl  27116  chtwordi  27154  ppiwordi  27160  chtrpcl  27173  fsumfldivdiaglem  27187  fsumvma2  27213  chpval2  27217  chpchtsum  27218  chpub  27219  logfacbnd3  27222  logexprlim  27224  mersenne  27226  lgsdilem  27323  lgsne0  27334  gausslemma2dlem1a  27364  lgseisen  27378  lgsquadlem1  27379  lgsquadlem2  27380  2sqmod  27435  2sqnn0  27437  chebbnd1lem2  27469  chebbnd1lem3  27470  chebbnd1  27471  chtppilimlem1  27472  chtppilimlem2  27473  chtppilim  27474  chebbnd2  27476  chto1lb  27477  chpchtlim  27478  chpo1ub  27479  dchrisumlema  27487  dchrisumlem2  27489  dchrisumlem3  27490  dchrmusumlema  27492  dchrvmasumlem2  27497  dchrvmasumiflem1  27500  dchrisum0flblem1  27507  dchrisum0flblem2  27508  dchrisum0re  27512  dchrisum0lema  27513  dchrisum0  27519  dirith2  27527  mulog2sumlem1  27533  vmalogdivsum2  27537  log2sumbnd  27543  selberg2lem  27549  chpdifbndlem1  27552  chpdifbnd  27554  selberg3lem1  27556  pntrmax  27563  pntrsumo1  27564  pntrlog2bndlem4  27579  pntrlog2bndlem5  27580  pntpbnd1a  27584  pntpbnd1  27585  pntpbnd2  27586  pntlemg  27597  pntlemj  27602  pntlemk  27605  pntlem3  27608  pnt2  27612  pnt  27613  ostth2lem1  27617  padicabv  27629  padicabvcxp  27631  ostth2lem3  27634  ostth2lem4  27635  ostth3  27637  trgcgrg  28478  tgcgr4  28494  axsegconlem7  28887  axsegconlem10  28890  axcontlem2  28929  axcontlem4  28931  axcontlem7  28934  axcontlem10  28937  crctcshwlkn0lem3  29779  crctcshwlkn0  29788  clwlkclwwlklem2a2  29959  clwlkclwwlklem2a  29964  wwlksubclwwlk  30024  frgrogt3nreg  30363  friendshipgt3  30364  minvecolem5  30847  minvecolem6  30848  htthlem  30883  pjhthlem1  31357  nndiffz1  32735  bcm1n  32744  fzo0opth  32754  expgt0b  32765  nexple  32780  indf1o  32796  wrdt2ind  32885  cycpmrn  33109  cyc3conja  33123  ccfldextdgrr  33663  constrsslem  33723  pnfneige0  33891  measinb  34163  eulerpartlems  34303  eulerpartlemgc  34305  ballotlemfc0  34436  ballotlemfcc  34437  ballotlemodife  34441  sgnneg  34484  sgnmul  34486  sgnsub  34488  signsply0  34507  signslema  34518  signsvtp  34539  itgexpif  34562  breprexplemc  34588  circlemeth  34596  logdivsqrle  34606  0nn0m1nnn0  35059  cvmliftlem2  35232  dnibndlem9  36428  unbdqndv2lem2  36452  knoppndvlem1  36454  knoppndvlem2  36455  knoppndvlem7  36460  knoppndvlem11  36464  knoppndvlem14  36467  knoppndvlem15  36468  knoppndvlem17  36470  knoppndvlem19  36472  knoppndvlem20  36473  bj-pinftynminfty  37169  poimirlem10  37578  poimirlem11  37579  poimirlem24  37592  poimirlem29  37597  poimirlem31  37599  poimirlem32  37600  poimir  37601  mblfinlem2  37606  ftc1anclem7  37647  ftc1anclem8  37648  ftc1anc  37649  areacirclem1  37656  areacirclem4  37659  areacirc  37661  geomcau  37707  isbnd3b  37733  prdsbnd  37741  bfp  37772  rrnequiv  37783  resdvopclptsd  41970  lcmineqlem2  41972  lcmineqlem3  41973  lcmineqlem10  41980  lcmineqlem12  41982  lcmineqlem23  41993  3lexlogpow5ineq1  41996  3lexlogpow5ineq2  41997  3lexlogpow5ineq4  41998  3lexlogpow5ineq3  41999  3lexlogpow2ineq2  42001  3lexlogpow5ineq5  42002  aks4d1lem1  42004  dvrelog2  42006  dvrelog3  42007  dvrelog2b  42008  0nonelalab  42009  dvrelogpow2b  42010  aks4d1p1p3  42011  aks4d1p1p2  42012  aks4d1p1p4  42013  aks4d1p1p6  42015  aks4d1p1p7  42016  aks4d1p1p5  42017  aks4d1p1  42018  aks4d1p2  42019  aks4d1p3  42020  aks4d1p5  42022  aks4d1p6  42023  aks4d1p7d1  42024  aks4d1p7  42025  aks4d1p8d2  42027  aks4d1p8d3  42028  aks4d1p8  42029  aks4d1p9  42030  posbezout  42042  primrootspoweq0  42048  aks6d1c1  42058  hashscontpow1  42063  aks6d1c2lem4  42069  aks6d1c5lem2  42080  deg1gprod  42082  2np3bcnp1  42086  2ap1caineq  42087  sticksstones7  42094  sticksstones10  42097  sticksstones12a  42099  sticksstones12  42100  sticksstones22  42110  aks6d1c6lem3  42114  bcled  42120  bcle2d  42121  aks6d1c7lem1  42122  aks6d1c7lem2  42123  aks6d1c7  42126  aks5lem6  42134  unitscyglem5  42141  aks5lem8  42143  metakunt2  42148  metakunt29  42175  sn-1ne2  42245  oexpreposd  42302  posqsqznn  42316  redvmptabs  42335  readvrec  42337  re1m1e0m0  42372  re0m0e0  42377  remul01  42382  remulneg2d  42389  sn-addlt0d  42421  sn-addgt0d  42422  renegmulnnass  42428  zmulcomlem  42430  mulgt0con1dlem  42432  sn-mulgt1d  42440  fimgmcyc  42489  dffltz  42589  3cubeslem1  42640  irrapxlem1  42778  irrapxlem2  42779  irrapxlem3  42780  irrapxlem4  42781  pellexlem6  42790  pell14qrgt0  42815  pell1qrgaplem  42829  pellfundex  42842  pellfundrp  42844  monotoddzzfi  42899  jm2.24  42920  jm2.23  42953  jm2.26lem3  42958  jm3.1lem3  42976  sqrtcvallem1  43589  reabsifneg  43590  reabsifpos  43592  sqrtcval  43599  k0004ss2  44110  imo72b2lem1  44127  dvgrat  44276  hashnzfz2  44285  binomcxplemnn0  44313  binomcxplemnotnn0  44320  neglt  45241  divlt0gt0d  45243  upbdrech2  45265  xralrple2  45310  xralrple3  45330  reclt0d  45343  reclt0  45347  xrpnf  45441  fsumnncl  45532  fsumsupp0  45538  sumnnodd  45590  lptre2pt  45600  limsupubuz  45673  liminfresre  45739  liminf0  45753  dvmptconst  45875  dvdivbd  45883  dvcosax  45886  dvbdfbdioolem1  45888  dvbdfbdioolem2  45889  ioodvbdlimc1lem1  45891  ioodvbdlimc1lem2  45892  ioodvbdlimc2lem  45894  dvxpaek  45900  dvnxpaek  45902  volioc  45932  volico  45943  stoweidlem1  45961  stoweidlem7  45967  stoweidlem11  45971  stoweidlem25  45985  stoweidlem26  45986  stoweidlem34  45994  stoweidlem36  45996  stoweidlem41  46001  stoweidlem42  46002  stoweidlem44  46004  stoweidlem45  46005  wallispilem3  46027  wallispilem4  46028  wallispi  46030  stirlinglem3  46036  stirlinglem5  46038  stirlinglem6  46039  stirlinglem7  46040  stirlinglem10  46043  stirlinglem11  46044  stirlinglem12  46045  dirkeritg  46062  dirkercncflem2  46064  fourierdlem9  46076  fourierdlem11  46078  fourierdlem12  46079  fourierdlem14  46081  fourierdlem15  46082  fourierdlem19  46086  fourierdlem24  46091  fourierdlem28  46095  fourierdlem30  46097  fourierdlem40  46107  fourierdlem41  46108  fourierdlem43  46110  fourierdlem44  46111  fourierdlem47  46113  fourierdlem50  46116  fourierdlem51  46117  fourierdlem57  46123  fourierdlem60  46126  fourierdlem61  46127  fourierdlem66  46132  fourierdlem68  46134  fourierdlem73  46139  fourierdlem74  46140  fourierdlem75  46141  fourierdlem78  46144  fourierdlem79  46145  fourierdlem83  46149  fourierdlem88  46154  fourierdlem92  46158  fourierdlem93  46159  fourierdlem97  46163  fourierdlem103  46169  fourierdlem104  46170  fourierdlem109  46175  fourierdlem111  46177  sqwvfoura  46188  sqwvfourb  46189  fourierswlem  46190  fouriersw  46191  elaa2lem  46193  etransclem4  46198  etransclem18  46212  etransclem19  46213  etransclem23  46217  etransclem27  46221  etransclem31  46225  etransclem32  46226  etransclem35  46229  etransclem41  46235  etransclem46  46240  etransclem48  46242  rrxtopnfi  46247  qndenserrnbllem  46254  salgencntex  46303  sge0tsms  46340  sge0isum  46387  volicorecl  46506  hoiprodcl  46507  ovnlerp  46522  ovnsubaddlem1  46530  hoiprodcl3  46540  volicore  46541  hoidmvcl  46542  hoidmvlelem1  46555  hoidmvlelem2  46556  hoidmvlelem3  46557  ovnhoi  46563  hoiqssbllem2  46583  volicorege0  46597  vonhoire  46632  pimrecltpos  46668  pimrecltneg  46684  smfmbfcex  46720  nsssmfmbflem  46738  smfrec  46749  smfmullem3  46753  smfdivdmmbl  46798  sharhght  46825  et-sqrtnegnre  46833  ormkglobd  46835  natglobalincr  46837  upwordnul  46840  zm1nn  47260  eluzge0nn0  47270  elfz2z  47273  2ffzoeq  47285  iccpartigtl  47356  iccpartgt  47360  requad01  47554  requad1  47555  requad2  47556  stgrusgra  47872  gpgedgvtx1  47966  expnegico01  48381  m1modmmod  48388  difmodm1lt  48389  regt1loggt0  48403  refdivmptf  48409  elbigolo1  48424  rege1logbrege0  48425  fllog2  48435  dignn0flhalflem1  48482  eenglngeehlnmlem2  48605  line2  48619  line2xlem  48620  line2x  48621  line2y  48622  itsclc0yqsol  48631  2itscp  48648  inlinecirc02plem  48653  amgmwlem  49317