Theorem 0red 11181

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 11069  0cc0 11070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11128  ax-addrcl 11131  ax-rnegex 11141  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836  df-rex 3086

This theorem is referenced by:  gt0ne0  11649  add20  11696  subge0  11697  lesub0  11701  mulge0  11702  msqgt0  11704  msqge0  11705  gt0ne0d  11748  addgt0d  11759  sublt0d  11810  prodgt0  12035  mulgt1  12050  lt2msq1  12073  fiminre2  12137  supmul1  12158  supmul  12161  nnne0  12244  0mnnnnn0  12510  nn0negleid  12530  neglt  13010  rpgecl  13020  ge0p1rp  13023  ledivge1le  13063  mul2lt0rlt0  13094  mul2lt0rgt0  13095  mul2lt0bi  13098  prodge0rd  13099  max0sub  13196  reltxrnmnf  13343  infmrp1  13345  lincmb01cmp  13496  iccf1o  13497  xov1plusxeqvd  13499  elfz0fzfz0  13635  fz0fzelfz0  13636  elfzo0z  13704  fzofzim  13712  fzo1fzo0n0  13718  elfzodifsumelfzo  13734  ssfzoulel  13763  elfznelfzo  13776  muladdmodid  13920  modltm1p1mod  13933  addmodlteq  13956  expgt1  14110  ltexp2a  14176  expcan  14179  ltexp2  14180  leexp2  14181  leexp2a  14182  zzlesq  14216  expnlbnd2  14244  discr  14250  fi1uzind  14517  ccatsymb  14593  ccat2s1fvw  14649  swrdnd  14665  swrdnnn0nd  14667  swrdswrdlem  14714  swrdswrd  14715  repswswrd  14794  swrd2lsw  14962  2swrd2eqwrdeq  14963  leabs  15309  max0add  15320  absgt0  15335  rlimrege0  15589  iseraltlem2  15693  fsumrecl  15744  o1fsum  15824  cvgcmp  15827  cvgcmpce  15829  geomulcvg  15889  mertenslem2  15898  fprodle  16009  rpnnen2lem4  16232  p1modz1  16276  moddvds  16280  oddge22np1  16366  bitsfzolem  16451  bitsinv1lem  16458  sadcaddlem  16474  nn0rppwr  16578  nn0expgcd  16581  lcmgcdlem  16623  dvdsnprmd  16707  2mulprm  16710  isprm7  16726  qnumgt0  16768  modprm0  16824  qexpz  16920  prmreclem4  16938  4sqlem6  16962  prmgaplem7  17076  gzrngunit  21465  regsumfsum  21467  regsumsupp  21654  fvmptnn04ifd  22893  chfacffsupp  22896  chfacfscmul0  22898  chfacfscmulgsum  22900  chfacfpmmul0  22902  chfacfpmmulgsum  22904  prdsmet  24410  metustexhalf  24596  nlmvscnlem2  24725  nlmvscnlem1  24726  nmo0  24775  blcvx  24838  iihalf1cn  24974  evth  25001  lebnumlem1  25003  lebnumii  25008  htpycc  25022  pcohtpylem  25061  pcoass  25066  pcorevlem  25068  nmoleub2lem3  25157  ipcnlem2  25286  ipcnlem1  25287  rrxcph  25434  rrxmetlem  25449  rrxmet  25450  rrxdstprj1  25451  ehlbase  25457  minveclem3b  25470  minveclem6  25476  pjthlem1  25479  ovolicopnf  25566  ioorcl2  25614  volivth  25649  mbfposr  25694  i1fmulc  25745  itg1mulc  25746  itg1ge0a  25753  mbfi1flim  25765  itg2split  25791  itg2monolem1  25792  itg2monolem3  25794  itg2mono  25795  itg2cnlem2  25804  itgge0  25853  bddiblnc  25884  dvlip  26035  dvlipcn  26036  dveq0  26042  dv11cn  26043  dvlt0  26047  dvfsumge  26064  dgradd2  26308  plydivlem3  26336  mtest  26444  radcnvlem1  26453  radcnv0  26456  radcnvlt1  26458  radcnvle  26460  pserulm  26462  pserdvlem1  26467  pserdv  26469  abelthlem2  26472  abelthlem7  26478  pilem2  26492  pilem3  26493  coseq00topi  26544  tanabsge  26548  cosq34lt1  26569  tanord1  26579  tanord  26580  rplogcl  26646  logdivle  26664  logcnlem3  26686  logcnlem4  26687  dvloglem  26690  logtayl  26702  abscxp2  26735  cxplt  26736  cxple  26737  cxple2a  26741  cxpcn3lem  26789  abscxpbnd  26795  rtprmirr  26802  chordthmlem4  26877  chordthmlem5  26878  asinlem3  26913  atanre  26927  atanlogaddlem  26955  atanlogadd  26956  atanlogsublem  26957  atantan  26965  atans2  26973  efrlim  27011  cxp2limlem  27017  cxp2lim  27018  cxploglim2  27020  divsqrtsumlem  27021  jensenlem2  27029  harmonicubnd  27051  fsumharmonic  27053  dmlogdmgm  27065  lgamgulmlem1  27070  lgamgulmlem2  27071  ftalem1  27114  ftalem2  27115  ftalem5  27118  vmacl  27159  chtwordi  27197  ppiwordi  27203  chtrpcl  27216  fsumfldivdiaglem  27230  fsumvma2  27255  chpval2  27259  chpchtsum  27260  chpub  27261  logfacbnd3  27264  logexprlim  27266  mersenne  27268  lgsdilem  27365  lgsne0  27376  gausslemma2dlem1a  27406  lgseisen  27420  lgsquadlem1  27421  lgsquadlem2  27422  2sqmod  27477  2sqnn0  27479  chebbnd1lem2  27511  chebbnd1lem3  27512  chebbnd1  27513  chtppilimlem1  27514  chtppilimlem2  27515  chtppilim  27516  chebbnd2  27518  chto1lb  27519  chpchtlim  27520  chpo1ub  27521  dchrisumlema  27529  dchrisumlem2  27531  dchrisumlem3  27532  dchrmusumlema  27534  dchrvmasumlem2  27539  dchrvmasumiflem1  27542  dchrisum0flblem1  27549  dchrisum0flblem2  27550  dchrisum0re  27554  dchrisum0lema  27555  dchrisum0  27561  dirith2  27569  mulog2sumlem1  27575  vmalogdivsum2  27579  log2sumbnd  27585  selberg2lem  27591  chpdifbndlem1  27594  chpdifbnd  27596  selberg3lem1  27598  pntrmax  27605  pntrsumo1  27606  pntrlog2bndlem4  27621  pntrlog2bndlem5  27622  pntpbnd1a  27626  pntpbnd1  27627  pntpbnd2  27628  pntlemg  27639  pntlemj  27644  pntlemk  27647  pntlem3  27650  pnt2  27654  pnt  27655  ostth2lem1  27659  padicabv  27671  padicabvcxp  27673  ostth2lem3  27676  ostth2lem4  27677  ostth3  27679  trgcgrg  28661  tgcgr4  28677  axsegconlem7  29070  axsegconlem10  29073  axcontlem2  29112  axcontlem4  29114  axcontlem7  29117  axcontlem10  29120  crctcshwlkn0lem3  29958  crctcshwlkn0  29967  clwlkclwwlklem2a2  30141  clwlkclwwlklem2a  30146  wwlksubclwwlk  30206  frgrogt3nreg  30545  friendshipgt3  30546  minvecolem5  31030  minvecolem6  31031  htthlem  31066  pjhthlem1  31540  sgnval2  32887  nndiffz1  32938  bcm1n  32947  fzo0opth  32955  expgt0b  32969  sgnneg  32985  sgnmul  32987  sgnsub  32989  nexple  32996  oexpled  32999  indf1o  33003  wrdt2ind  33092  cycpmrn  33284  cyc3conja  33298  ccfldextdgrr  33930  constrsslem  33999  constrresqrtcl  34035  constrsqrtcl  34037  cos9thpiminplylem1  34040  pnfneige0  34209  measinb  34479  eulerpartlems  34618  eulerpartlemgc  34620  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemodife  34756  signsply0  34809  signslema  34820  signsvtp  34841  itgexpif  34864  breprexplemc  34890  circlemeth  34898  logdivsqrle  34908  0nn0m1nnn0  35427  cvmliftlem2  35600  dnibndlem9  36888  unbdqndv2lem2  36912  knoppndvlem1  36914  knoppndvlem2  36915  knoppndvlem7  36920  knoppndvlem11  36924  knoppndvlem14  36927  knoppndvlem15  36928  knoppndvlem17  36930  knoppndvlem19  36932  knoppndvlem20  36933  bj-pinftynminfty  37683  poimirlem10  38093  poimirlem11  38094  poimirlem24  38107  poimirlem29  38112  poimirlem31  38114  poimirlem32  38115  poimir  38116  mblfinlem2  38121  ftc1anclem7  38162  ftc1anclem8  38163  ftc1anc  38164  areacirclem1  38171  areacirclem4  38174  areacirc  38176  geomcau  38222  isbnd3b  38248  prdsbnd  38256  bfp  38287  rrnequiv  38298  resdvopclptsd  42609  lcmineqlem2  42611  lcmineqlem3  42612  lcmineqlem10  42619  lcmineqlem12  42621  lcmineqlem23  42632  3lexlogpow5ineq1  42635  3lexlogpow5ineq2  42636  3lexlogpow5ineq4  42637  3lexlogpow5ineq3  42638  3lexlogpow2ineq2  42640  3lexlogpow5ineq5  42641  aks4d1lem1  42643  dvrelog2  42645  dvrelog3  42646  dvrelog2b  42647  0nonelalab  42648  dvrelogpow2b  42649  aks4d1p1p3  42650  aks4d1p1p2  42651  aks4d1p1p4  42652  aks4d1p1p6  42654  aks4d1p1p7  42655  aks4d1p1p5  42656  aks4d1p1  42657  aks4d1p2  42658  aks4d1p3  42659  aks4d1p5  42661  aks4d1p6  42662  aks4d1p7d1  42663  aks4d1p7  42664  aks4d1p8d2  42666  aks4d1p8d3  42667  aks4d1p8  42668  aks4d1p9  42669  posbezout  42681  primrootspoweq0  42687  aks6d1c1  42697  hashscontpow1  42702  aks6d1c2lem4  42708  aks6d1c5lem2  42719  deg1gprod  42721  2np3bcnp1  42725  2ap1caineq  42726  sticksstones7  42733  sticksstones10  42736  sticksstones12a  42738  sticksstones12  42739  sticksstones22  42749  aks6d1c6lem3  42753  bcled  42759  bcle2d  42760  aks6d1c7lem1  42761  aks6d1c7lem2  42762  aks6d1c7  42765  aks5lem6  42773  unitscyglem5  42780  aks5lem8  42782  sn-1ne2  42844  oexpreposd  42895  posqsqznn  42909  redvmptabs  42933  readvrec  42935  re1m1e0m0  42970  re0m0e0  42975  remul01  42980  sn-remul0ord  42981  remulneg2d  42988  rediveq0d  43022  sn-rediv0d  43026  sn-addlt0d  43044  sn-addgt0d  43045  renegmulnnass  43051  zmulcomlem  43053  mulgt0con1dlem  43055  sn-mulgt1d  43065  mulltgt0d  43068  mullt0b2d  43070  sn-mullt0d  43071  sn-msqgt0d  43072  fimgmcyc  43116  dffltz  43180  3cubeslem1  43229  irrapxlem1  43363  irrapxlem2  43364  irrapxlem3  43365  irrapxlem4  43366  pellexlem6  43375  pell14qrgt0  43400  pell1qrgaplem  43414  pellfundex  43427  pellfundrp  43429  monotoddzzfi  43483  jm2.24  43504  jm2.23  43537  jm2.26lem3  43542  jm3.1lem3  43560  sqrtcvallem1  44171  reabsifneg  44172  reabsifpos  44174  sqrtcval  44181  k0004ss2  44692  imo72b2lem1  44709  dvgrat  44852  hashnzfz2  44861  binomcxplemnn0  44889  binomcxplemnotnn0  44896  divlt0gt0d  45829  upbdrech2  45851  xralrple2  45894  xralrple3  45913  reclt0d  45926  reclt0  45930  xrpnf  46023  fsumnncl  46112  fsumsupp0  46118  sumnnodd  46170  lptre2pt  46178  limsupubuz  46251  liminfresre  46317  liminf0  46331  dvmptconst  46453  dvdivbd  46461  dvcosax  46464  dvbdfbdioolem1  46466  dvbdfbdioolem2  46467  ioodvbdlimc1lem1  46469  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvxpaek  46478  dvnxpaek  46480  volioc  46510  volico  46521  stoweidlem1  46539  stoweidlem7  46545  stoweidlem11  46549  stoweidlem25  46563  stoweidlem26  46564  stoweidlem34  46572  stoweidlem36  46574  stoweidlem41  46579  stoweidlem42  46580  stoweidlem44  46582  stoweidlem45  46583  wallispilem3  46605  wallispilem4  46606  wallispi  46608  stirlinglem3  46614  stirlinglem5  46616  stirlinglem6  46617  stirlinglem7  46618  stirlinglem10  46621  stirlinglem11  46622  stirlinglem12  46623  dirkeritg  46640  dirkercncflem2  46642  fourierdlem9  46654  fourierdlem11  46656  fourierdlem12  46657  fourierdlem14  46659  fourierdlem15  46660  fourierdlem19  46664  fourierdlem24  46669  fourierdlem28  46673  fourierdlem30  46675  fourierdlem40  46685  fourierdlem41  46686  fourierdlem43  46688  fourierdlem44  46689  fourierdlem47  46691  fourierdlem50  46694  fourierdlem51  46695  fourierdlem57  46701  fourierdlem60  46704  fourierdlem61  46705  fourierdlem66  46710  fourierdlem68  46712  fourierdlem73  46717  fourierdlem74  46718  fourierdlem75  46719  fourierdlem78  46722  fourierdlem79  46723  fourierdlem83  46727  fourierdlem88  46732  fourierdlem92  46736  fourierdlem93  46737  fourierdlem97  46741  fourierdlem103  46747  fourierdlem104  46748  fourierdlem109  46753  fourierdlem111  46755  sqwvfoura  46766  sqwvfourb  46767  fourierswlem  46768  fouriersw  46769  elaa2lem  46771  etransclem4  46776  etransclem18  46790  etransclem19  46791  etransclem23  46795  etransclem27  46799  etransclem31  46803  etransclem32  46804  etransclem35  46807  etransclem41  46813  etransclem46  46818  etransclem48  46820  rrxtopnfi  46825  qndenserrnbllem  46832  salgencntex  46881  sge0tsms  46918  sge0isum  46965  volicorecl  47084  hoiprodcl  47085  ovnlerp  47100  ovnsubaddlem1  47108  hoiprodcl3  47118  volicore  47119  hoidmvcl  47120  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem3  47135  ovnhoi  47141  hoiqssbllem2  47161  volicorege0  47175  vonhoire  47210  pimrecltpos  47246  pimrecltneg  47262  smfmbfcex  47298  nsssmfmbflem  47316  smfrec  47327  smfmullem3  47331  smfdivdmmbl  47376  sharhght  47403  et-sqrtnegnre  47411  ormkglobd  47415  natglobalincr  47417  chnsubseqwl  47419  zm1nn  47860  eluzge0nn0  47870  elfz2z  47873  2ffzoeq  47886  m1modmmod  47922  modm1p1ne  47934  muldvdsfacm1  47945  iccpartigtl  47993  iccpartgt  47997  nprmdvdsfacm1lem4  48196  requad01  48207  requad1  48208  requad2  48209  stgrusgra  48545  gpgedgvtx1  48648  expnegico01  49104  regt1loggt0  49122  refdivmptf  49128  elbigolo1  49143  rege1logbrege0  49144  fllog2  49154  dignn0flhalflem1  49201  eenglngeehlnmlem2  49324  line2  49338  line2xlem  49339  line2x  49340  line2y  49341  itsclc0yqsol  49350  2itscp  49367  inlinecirc02plem  49372  amgmwlem  50387