Theorem 0red 11338

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11226  0cc0 11227

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11285  ax-addrcl 11288  ax-rnegex 11298  ax-cnre 11300

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-rex 3091

This theorem is used by:  gt0ne0  11808  add20  11855  subge0  11856  lesub0  11860  mulge0  11861  msqgt0  11863  msqge0  11864  gt0ne0d  11907  addgt0d  11918  sublt0d  11969  prodgt0  12191  mulgt1  12205  lt2msq1  12228  fiminre2  12292  supmul1  12313  supmul  12316  nnne0  12399  0mnnnnn0  12665  nn0negleid  12685  0nn0m1nnn0  12780  neglt  13167  rpgecl  13177  ge0p1rp  13180  ledivge1le  13220  mul2lt0rlt0  13251  mul2lt0rgt0  13252  mul2lt0bi  13255  prodge0rd  13256  max0sub  13353  reltxrnmnf  13500  infmrp1  13502  lincmb01cmp  13653  iccf1o  13654  xov1plusxeqvd  13656  elfz0fzfz0  13794  fz0fzelfz0  13795  elfzo0z  13863  fzofzim  13871  fzo1fzo0n0  13877  elfzodifsumelfzo  13893  ssfzoulel  13922  elfznelfzo  13935  muladdmodid  14080  modltm1p1mod  14093  addmodlteq  14116  expgt1  14270  ltexp2a  14336  expcan  14339  ltexp2  14340  leexp2  14341  leexp2a  14342  zzlesq  14377  expnlbnd2  14405  discr  14411  fi1uzind  14679  ccatsymb  14755  ccat2s1fvw  14814  swrdnd  14832  swrdnnn0nd  14834  swrdswrdlem  14881  swrdswrd  14882  repswswrd  14963  swrd2lsw  15134  2swrd2eqwrdeq  15135  sgnneg  15282  sgnsub  15288  sgnmul  15289  leabs  15495  max0add  15506  absgt0  15521  rlimrege0  15775  iseraltlem2  15879  fsumrecl  15929  o1fsum  16009  cvgcmp  16012  cvgcmpce  16014  geomulcvg  16074  mertenslem2  16083  fprodle  16192  rpnnen2lem4  16414  p1modz1  16458  moddvds  16462  oddge22np1  16548  bitsfzolem  16633  bitsinv1lem  16640  sadcaddlem  16656  nn0rppwr  16764  nn0expgcd  16767  lcmgcdlem  16810  dvdsnprmd  16894  2mulprm  16897  isprm7  16913  qnumgt0  16955  posqsqznn  16965  modprm0  17012  qexpz  17108  prmreclem4  17126  4sqlem6  17150  prmgaplem7  17264  gzrngunit  21769  regsumfsum  21771  regsumsupp  21958  fvmptnn04ifd  23201  chfacffsupp  23204  chfacfscmul0  23206  chfacfscmulgsum  23208  chfacfpmmul0  23210  chfacfpmmulgsum  23212  prdsmet  24719  metustexhalf  24905  nlmvscnlem2  25034  nlmvscnlem1  25035  nmo0  25084  blcvx  25147  iihalf1cn  25283  evth  25310  lebnumlem1  25312  lebnumii  25317  htpycc  25331  pcohtpylem  25370  pcoass  25375  pcorevlem  25377  nmoleub2lem3  25466  ipcnlem2  25595  ipcnlem1  25596  rrxcph  25743  rrxmetlem  25758  rrxmet  25759  rrxdstprj1  25760  minveclem3b  25779  minveclem6  25785  pjthlem1  25788  ovolicopnf  25875  ioorcl2  25923  volivth  25958  mbfposr  26003  i1fmulc  26054  itg1mulc  26055  itg1ge0a  26062  mbfi1flim  26074  itg2split  26100  itg2monolem1  26101  itg2monolem3  26103  itg2mono  26104  itg2cnlem2  26113  itgge0  26161  bddiblnc  26192  dvlip  26343  dvlipcn  26344  dveq0  26350  dv11cn  26351  dvlt0  26355  dvfsumge  26372  dgradd2  26617  plydivlem3  26646  mtest  26761  radcnvlem1  26770  radcnv0  26773  radcnvlt1  26775  radcnvle  26777  pserulm  26779  pserdvlem1  26784  pserdv  26786  abelthlem2  26789  abelthlem7  26795  pilem2  26809  pilem3  26810  coseq00topi  26861  tanabsge  26865  cosq34lt1  26885  tanord1  26895  tanord  26896  rplogcl  26962  logdivle  26980  logcnlem3  27002  logcnlem4  27003  dvloglem  27006  logtayl  27018  abscxp2  27051  cxplt  27052  cxple  27053  cxple2a  27057  cxpcn3lem  27105  abscxpbnd  27111  rtprmirr  27118  chordthmlem4  27193  chordthmlem5  27194  asinlem3  27229  atanre  27243  atanlogaddlem  27271  atanlogadd  27272  atanlogsublem  27273  atantan  27281  atans2  27289  efrlim  27327  cxp2limlem  27333  cxp2lim  27334  cxploglim2  27336  divsqrtsumlem  27337  jensenlem2  27345  harmonicubnd  27367  fsumharmonic  27369  dmlogdmgm  27381  lgamgulmlem1  27386  lgamgulmlem2  27387  ftalem1  27430  ftalem2  27431  ftalem5  27434  vmacl  27475  chtwordi  27513  ppiwordi  27519  chtrpcl  27532  fsumfldivdiaglem  27546  fsumvma2  27571  chpval2  27575  chpchtsum  27576  chpub  27577  logfacbnd3  27580  logexprlim  27582  mersenne  27584  lgsdilem  27681  lgsne0  27692  gausslemma2dlem1a  27722  lgseisen  27736  lgsquadlem1  27737  lgsquadlem2  27738  2sqmod  27793  2sqnn0  27795  chebbnd1lem2  27827  chebbnd1lem3  27828  chebbnd1  27829  chtppilimlem1  27830  chtppilimlem2  27831  chtppilim  27832  chebbnd2  27834  chto1lb  27835  chpchtlim  27836  chpo1ub  27837  dchrisumlema  27845  dchrisumlem2  27847  dchrisumlem3  27848  dchrmusumlema  27850  dchrvmasumlem2  27855  dchrvmasumiflem1  27858  dchrisum0flblem1  27865  dchrisum0flblem2  27866  dchrisum0re  27870  dchrisum0lema  27871  dchrisum0  27877  dirith2  27885  mulog2sumlem1  27891  vmalogdivsum2  27895  log2sumbnd  27901  selberg2lem  27907  chpdifbndlem1  27910  chpdifbnd  27912  selberg3lem1  27914  pntrmax  27921  pntrsumo1  27922  pntrlog2bndlem4  27937  pntrlog2bndlem5  27938  pntpbnd1a  27942  pntpbnd1  27943  pntpbnd2  27944  pntlemg  27955  pntlemj  27960  pntlemk  27963  pntlem3  27966  pnt2  27970  pnt  27971  ostth2lem1  27975  padicabv  27987  padicabvcxp  27989  ostth2lem3  27992  ostth2lem4  27993  ostth3  27995  trgcgrg  29008  tgcgr4  29024  axsegconlem7  29531  axsegconlem10  29534  axcontlem2  29573  axcontlem4  29575  axcontlem7  29578  axcontlem10  29581  crctcshwlkn0lem3  30431  crctcshwlkn0  30440  clwlkclwwlklem2a2  30614  clwlkclwwlklem2a  30619  wwlksubclwwlk  30679  frgrogt3nreg  31028  friendshipgt3  31029  minvecolem5  31513  minvecolem6  31514  htthlem  31549  pjhthlem1  32023  sgnval2  33397  nndiffz1  33448  bcm1n  33457  fzo0opth  33465  expgt0b  33478  nexple  33494  oexpled  33497  indf1o  33501  wrdt2ind  33586  cycpmrn  33774  cyc3conja  33788  ccfldextdgrr  34374  constrsslem  34443  constrresqrtcl  34479  constrsqrtcl  34481  cos9thpiminplylem1  34484  pnfneige0  34653  measinb  34924  eulerpartlems  35062  eulerpartlemgc  35064  ballotlemfc0  35195  ballotlemfcc  35196  ballotlemodife  35200  signsply0  35250  signslema  35261  signsvtp  35282  itgexpif  35305  breprexplemc  35331  circlemeth  35339  logdivsqrle  35349  cvmliftlem2  36218  dnibndlem9  37530  unbdqndv2lem2  37554  knoppndvlem1  37556  knoppndvlem2  37557  knoppndvlem7  37562  knoppndvlem11  37566  knoppndvlem14  37569  knoppndvlem15  37570  knoppndvlem17  37572  knoppndvlem19  37574  knoppndvlem20  37575  bj-pinftynminfty  38340  poimirlem10  38740  poimirlem11  38741  poimirlem24  38754  poimirlem29  38759  poimirlem31  38761  poimirlem32  38762  poimir  38763  mblfinlem2  38768  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  areacirclem1  38818  areacirclem4  38821  areacirc  38823  geomcau  38885  isbnd3b  38911  prdsbnd  38919  bfp  38950  rrnequiv  38961  resdvopclptsd  43270  lcmineqlem2  43272  lcmineqlem3  43273  lcmineqlem10  43280  lcmineqlem12  43282  lcmineqlem23  43293  3lexlogpow5ineq1  43296  3lexlogpow5ineq2  43297  3lexlogpow5ineq4  43298  3lexlogpow5ineq3  43299  3lexlogpow2ineq2  43301  3lexlogpow5ineq5  43302  aks4d1lem1  43304  dvrelog2  43306  dvrelog3  43307  dvrelog2b  43308  0nonelalab  43309  dvrelogpow2b  43310  aks4d1p1p3  43311  aks4d1p1p2  43312  aks4d1p1p4  43313  aks4d1p1p6  43315  aks4d1p1p7  43316  aks4d1p1p5  43317  aks4d1p1  43318  aks4d1p2  43319  aks4d1p3  43320  aks4d1p5  43322  aks4d1p6  43323  aks4d1p7d1  43324  aks4d1p7  43325  aks4d1p8d2  43327  aks4d1p8d3  43328  aks4d1p8  43329  aks4d1p9  43330  posbezout  43342  primrootspoweq0  43348  aks6d1c1  43358  hashscontpow1  43363  aks6d1c2lem4  43369  aks6d1c5lem2  43380  deg1gprod  43382  2np3bcnp1  43386  2ap1caineq  43387  sticksstones7  43394  sticksstones10  43397  sticksstones12a  43399  sticksstones12  43400  sticksstones22  43410  aks6d1c6lem3  43414  bcled  43420  bcle2d  43421  aks6d1c7lem1  43422  aks6d1c7lem2  43423  aks6d1c7  43426  aks5lem6  43434  unitscyglem5  43441  aks5lem8  43443  sn-1ne2  43523  oexpreposd  43572  redvmptabs  43604  readvrec  43606  re1m1e0m0  43641  re0m0e0  43646  remul01  43651  sn-remul0ord  43652  remulneg2d  43659  rediveq0d  43693  sn-rediv0d  43697  sn-addlt0d  43715  sn-addgt0d  43716  renegmulnnass  43722  zmulcomlem  43724  mulgt0con1dlem  43726  sn-mulgt1d  43736  mulltgt0d  43739  mullt0b2d  43741  sn-mullt0d  43742  sn-msqgt0d  43743  fimgmcyc  43791  dffltz  43863  3cubeslem1  43887  irrapxlem1  44022  irrapxlem2  44023  irrapxlem3  44024  irrapxlem4  44025  pellexlem6  44034  pell14qrgt0  44059  pell1qrgaplem  44073  pellfundex  44086  pellfundrp  44088  monotoddzzfi  44142  jm2.24  44163  jm2.23  44196  jm2.26lem3  44201  jm3.1lem3  44219  sqrtcvallem1  44823  reabsifneg  44824  reabsifpos  44826  sqrtcval  44833  k0004ss2  45344  imo72b2lem1  45361  dvgrat  45488  hashnzfz2  45497  binomcxplemnn0  45525  binomcxplemnotnn0  45532  divlt0gt0d  46507  upbdrech2  46529  xralrple2  46571  xralrple3  46590  reclt0d  46603  reclt0  46607  xrpnf  46700  fsumnncl  46789  fsumsupp0  46795  sumnnodd  46847  lptre2pt  46855  limsupubuz  46928  liminfresre  46994  liminf0  47008  dvmptconst  47130  dvdivbd  47138  dvcosax  47141  dvbdfbdioolem1  47143  dvbdfbdioolem2  47144  ioodvbdlimc1lem1  47146  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  dvxpaek  47155  dvnxpaek  47157  volioc  47187  volico  47198  stoweidlem1  47216  stoweidlem7  47222  stoweidlem11  47226  stoweidlem25  47240  stoweidlem26  47241  stoweidlem34  47249  stoweidlem36  47251  stoweidlem41  47256  stoweidlem42  47257  stoweidlem44  47259  stoweidlem45  47260  wallispilem3  47282  wallispilem4  47283  wallispi  47285  stirlinglem3  47291  stirlinglem5  47293  stirlinglem6  47294  stirlinglem7  47295  stirlinglem10  47298  stirlinglem11  47299  stirlinglem12  47300  dirkeritg  47317  dirkercncflem2  47319  fourierdlem9  47331  fourierdlem11  47333  fourierdlem12  47334  fourierdlem14  47336  fourierdlem15  47337  fourierdlem19  47341  fourierdlem24  47346  fourierdlem28  47350  fourierdlem30  47352  fourierdlem40  47362  fourierdlem41  47363  fourierdlem43  47365  fourierdlem44  47366  fourierdlem47  47368  fourierdlem50  47371  fourierdlem51  47372  fourierdlem57  47378  fourierdlem60  47381  fourierdlem61  47382  fourierdlem66  47387  fourierdlem68  47389  fourierdlem73  47394  fourierdlem74  47395  fourierdlem75  47396  fourierdlem78  47399  fourierdlem79  47400  fourierdlem83  47404  fourierdlem88  47409  fourierdlem92  47413  fourierdlem93  47414  fourierdlem97  47418  fourierdlem103  47424  fourierdlem104  47425  fourierdlem109  47430  fourierdlem111  47432  sqwvfoura  47443  sqwvfourb  47444  fourierswlem  47445  fouriersw  47446  elaa2lem  47448  etransclem4  47453  etransclem18  47467  etransclem19  47468  etransclem23  47472  etransclem27  47476  etransclem31  47480  etransclem32  47481  etransclem35  47484  etransclem41  47490  etransclem46  47495  etransclem48  47497  rrxtopnfi  47502  qndenserrnbllem  47509  salgencntex  47558  sge0tsms  47595  sge0isum  47642  volicorecl  47761  hoiprodcl  47762  ovnlerp  47777  ovnsubaddlem1  47785  hoiprodcl3  47795  volicore  47796  hoidmvcl  47797  hoidmvlelem1  47810  hoidmvlelem2  47811  hoidmvlelem3  47812  ovnhoi  47818  hoiqssbllem2  47838  volicorege0  47852  vonhoire  47887  pimrecltpos  47923  pimrecltneg  47939  smfmbfcex  47975  nsssmfmbflem  47993  smfrec  48004  smfmullem3  48008  smfdivdmmbl  48053  sharhght  48080  et-sqrtnegnre  48088  ormkglobd  48092  chnsubseqwl  48094  zm1nn  48577  eluzge0nn0  48587  elfz2z  48590  2ffzoeq  48603  m1modmmod  48639  modm1p1ne  48651  muldvdsfacm1  48662  iccpartigtl  48710  iccpartgt  48714  nprmdvdsfacm1lem4  48913  requad01  48924  requad1  48925  requad2  48926  stgrusgra  49262  gpgedgvtx1  49365  expnegico01  49835  regt1loggt0  49853  refdivmptf  49859  elbigolo1  49874  rege1logbrege0  49875  fllog2  49885  dignn0flhalflem1  49932  eenglngeehlnmlem2  50056  line2  50069  line2xlem  50070  line2x  50071  line2y  50072  itsclc0yqsol  50081  2itscp  50098  inlinecirc02plem  50103  veronesefvcl  51252  veronesev1lem  51253  veronesev2lem  51254  veronesev3lem  51255  veronesev4lem  51256  veronesev5lem  51257  veronesev6lem  51258  amgmwlem  51267