Theorem rpne0d 12976

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 12944	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ≠ 0)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≠ 0)

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  0cc0 11044  ℝ⁺crp 12927

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-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-addrcl 11105  ax-rnegex 11115  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-ltxr 11189  df-rp 12928

This theorem is referenced by:  rprene0d  12979  rpcnne0d  12980  iccf1o  13433  ltexp2r  14114  discr  14181  bcpasc  14262  sqrtdiv  15207  abs00  15231  absdiv  15237  o1rlimmul  15561  geomulcvg  15818  mertenslem1  15826  retanhcl  16103  tanhlt1  16104  tanhbnd  16105  sylow1lem1  19512  nrginvrcnlem  24612  nmoi2  24651  reperflem  24740  icchmeoOLD  24872  icopnfcnv  24873  nmoleub2lem  25047  nmoleub2lem2  25049  nmoleub3  25052  pjthlem1  25370  sca2rab  25446  ovolscalem1  25447  ovolsca  25449  itg2mulclem  25680  itg2mulc  25681  c1liplem1  25934  aalioulem4  26276  aaliou3lem8  26286  itgulm  26350  dvradcnv  26363  abelthlem7  26381  abelthlem8  26382  tanrpcl  26446  tanregt0  26481  efiarg  26549  argregt0  26552  argrege0  26553  argimgt0  26554  tanarg  26561  logdivlti  26562  logno1  26578  logcnlem4  26587  divcxp  26629  cxple2  26639  cxpcn3lem  26690  cxpcn3  26691  cxpaddlelem  26694  cxpaddle  26695  logbrec  26725  asinlem3  26814  rlimcnp  26908  rlimcnp2  26909  rlimcxp  26917  cxp2limlem  26919  cxp2lim  26920  cxploglim2  26922  jensenlem2  26931  amgmlem  26933  logdiflbnd  26938  lgamgulmlem2  26973  lgamucov  26981  basellem3  27026  basellem8  27031  isppw  27057  chpeq0  27152  chteq0  27153  bposlem9  27236  chebbnd1lem2  27414  chebbnd1  27416  chtppilimlem1  27417  chebbnd2  27421  chto1lb  27422  chpchtlim  27423  chpo1ubb  27425  rplogsumlem1  27428  rplogsumlem2  27429  dchrvmasumlem1  27439  dchrvmasum2lem  27440  dchrisum0lema  27458  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2a  27461  dchrisum0lem2  27462  dchrisum0lem3  27463  dchrisum0  27464  mulog2sumlem1  27478  vmalogdivsum2  27482  vmalogdivsum  27483  2vmadivsumlem  27484  chpdifbndlem1  27497  selberg3lem1  27501  selberg3lem2  27502  selberg3  27503  selberg4lem1  27504  selberg4  27505  selberg3r  27513  selberg4r  27514  selberg34r  27515  pntrlog2bndlem1  27521  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntrlog2bndlem6  27527  pntpbnd2  27531  pntibndlem2  27535  pntlemr  27546  pntlemo  27551  pnt2  27557  pnt  27558  padicabv  27574  padicabvcxp  27576  ostth2lem3  27579  ostth2lem4  27580  ostth3  27582  smcnlem  30676  pjhthlem1  31370  rpxdivcld  32904  xrmulc1cn  33913  esumdivc  34066  probmeasb  34414  signsply0  34535  divsqrtid  34578  hgt750leme  34642  circum  35654  iprodgam  35722  faclimlem1  35723  faclimlem3  35725  knoppndvlem17  36509  knoppndvlem18  36510  itg2addnclem3  37660  geomcau  37746  cntotbnd  37783  bfplem1  37809  rrncmslem  37819  rrnequiv  37822  relogbzexpd  41956  aks4d1p1p1  42044  dvrelogpow2b  42049  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p5  42061  aks4d1p6  42062  exp11d  42307  rplog11d  42328  irrapxlem5  42807  pellfund14  42879  rmxyneg  42902  rmxyadd  42903  modabsdifz  42968  binomcxplemnotnn0  44338  oddfl  45269  xralrple3  45363  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweidlem1  45992  stoweidlem14  46005  stoweidlem60  46051  wallispilem4  46059  wallispilem5  46060  wallispi  46061  wallispi2lem1  46062  stirlinglem1  46065  stirlinglem3  46067  stirlinglem4  46068  stirlinglem5  46069  stirlinglem8  46072  stirlinglem12  46076  stirlinglem15  46079  dirkertrigeqlem1  46089  dirkercncflem1  46094  dirkercncflem4  46097  fourierdlem30  46128  fourierdlem39  46137  fourierdlem47  46144  fourierdlem65  46162  fourierdlem73  46170  fourierdlem87  46184  qndenserrnbllem  46285  sge0rpcpnf  46412  hoiqssbllem2  46614  young2d  49787