Theorem rpne0d 12980

Description: A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpne0d	⊢ (𝜑 → 𝐴 ≠ 0)

Proof of Theorem rpne0d

Step	Hyp	Ref	Expression
1		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpne0 12948	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2930  0cc0 11027  ℝ⁺crp 12931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-resscn 11084  ax-1cn 11085  ax-addrcl 11088  ax-rnegex 11098  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-po 5528  df-so 5529  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-rp 12932

This theorem is referenced by:  rprene0d  12983  rpcnne0d  12984  iccf1o  13438  ltexp2r  14124  discr  14191  bcpasc  14272  sqrtdiv  15216  abs00  15240  absdiv  15246  o1rlimmul  15570  geomulcvg  15830  mertenslem1  15838  retanhcl  16115  tanhlt1  16116  tanhbnd  16117  sylow1lem1  19562  nrginvrcnlem  24644  nmoi2  24683  reperflem  24772  icopnfcnv  24897  nmoleub2lem  25069  nmoleub2lem2  25071  nmoleub3  25074  pjthlem1  25392  sca2rab  25467  ovolscalem1  25468  ovolsca  25470  itg2mulclem  25701  itg2mulc  25702  c1liplem1  25951  aalioulem4  26289  aaliou3lem8  26299  itgulm  26361  dvradcnv  26374  abelthlem7  26391  abelthlem8  26392  tanrpcl  26456  tanregt0  26491  efiarg  26559  argregt0  26562  argrege0  26563  argimgt0  26564  tanarg  26571  logdivlti  26572  logno1  26588  logcnlem4  26597  divcxp  26639  cxple2  26649  cxpcn3lem  26699  cxpcn3  26700  cxpaddlelem  26703  cxpaddle  26704  logbrec  26734  asinlem3  26823  rlimcnp  26917  rlimcnp2  26918  rlimcxp  26925  cxp2limlem  26927  cxp2lim  26928  cxploglim2  26930  jensenlem2  26939  amgmlem  26941  logdiflbnd  26946  lgamgulmlem2  26981  lgamucov  26989  basellem3  27034  basellem8  27039  isppw  27065  chpeq0  27159  chteq0  27160  bposlem9  27243  chebbnd1lem2  27421  chebbnd1  27423  chtppilimlem1  27424  chebbnd2  27428  chto1lb  27429  chpchtlim  27430  chpo1ubb  27432  rplogsumlem1  27435  rplogsumlem2  27436  dchrvmasumlem1  27446  dchrvmasum2lem  27447  dchrisum0lema  27465  dchrisum0lem1b  27466  dchrisum0lem1  27467  dchrisum0lem2a  27468  dchrisum0lem2  27469  dchrisum0lem3  27470  dchrisum0  27471  mulog2sumlem1  27485  vmalogdivsum2  27489  vmalogdivsum  27490  2vmadivsumlem  27491  chpdifbndlem1  27504  selberg3lem1  27508  selberg3lem2  27509  selberg3  27510  selberg4lem1  27511  selberg4  27512  selberg3r  27520  selberg4r  27521  selberg34r  27522  pntrlog2bndlem1  27528  pntrlog2bndlem2  27529  pntrlog2bndlem3  27530  pntrlog2bndlem4  27531  pntrlog2bndlem5  27532  pntrlog2bndlem6  27534  pntpbnd2  27538  pntibndlem2  27542  pntlemr  27553  pntlemo  27558  pnt2  27564  pnt  27565  padicabv  27581  padicabvcxp  27583  ostth2lem3  27586  ostth2lem4  27587  ostth3  27589  smcnlem  30756  pjhthlem1  31450  rpxdivcld  32981  xrmulc1cn  34062  esumdivc  34215  probmeasb  34562  signsply0  34683  divsqrtid  34726  hgt750leme  34790  circum  35844  iprodgam  35912  faclimlem1  35913  faclimlem3  35915  knoppndvlem17  36776  knoppndvlem18  36777  itg2addnclem3  37982  geomcau  38068  cntotbnd  38105  bfplem1  38131  rrncmslem  38141  rrnequiv  38144  relogbzexpd  42403  aks4d1p1p1  42490  dvrelogpow2b  42495  aks4d1p1p4  42498  aks4d1p1p6  42500  aks4d1p1p7  42501  aks4d1p5  42507  aks4d1p6  42508  exp11d  42746  rplog11d  42767  irrapxlem5  43242  pellfund14  43314  rmxyneg  43336  rmxyadd  43337  modabsdifz  43402  binomcxplemnotnn0  44771  oddfl  45699  xralrple3  45791  ioodvbdlimc1lem2  46348  ioodvbdlimc2lem  46350  stoweidlem1  46417  stoweidlem14  46430  stoweidlem60  46476  wallispilem4  46484  wallispilem5  46485  wallispi  46486  wallispi2lem1  46487  stirlinglem1  46490  stirlinglem3  46492  stirlinglem4  46493  stirlinglem5  46494  stirlinglem8  46497  stirlinglem12  46501  stirlinglem15  46504  dirkertrigeqlem1  46514  dirkercncflem1  46519  dirkercncflem4  46522  fourierdlem30  46553  fourierdlem39  46562  fourierdlem47  46569  fourierdlem65  46587  fourierdlem73  46595  fourierdlem87  46609  qndenserrnbllem  46710  sge0rpcpnf  46837  hoiqssbllem2  47039  young2d  50268