Theorem rpne0d 13169

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ≠ wne 2955  0cc0 11200  ℝ⁺crp 13120

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-addrcl 11261  ax-rnegex 11271  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-rp 13121

This theorem is used by:  rprene0d  13172  rpcnne0d  13173  iccf1o  13627  ltexp2r  14316  discr  14384  bcpasc  14465  sqrtdiv  15432  abs00  15456  absdiv  15462  o1rlimmul  15786  geomulcvg  16045  mertenslem1  16053  retanhcl  16327  tanhlt1  16328  tanhbnd  16329  sylow1lem1  19812  nrginvrcnlem  25010  nmoi2  25049  reperflem  25138  icopnfcnv  25263  nmoleub2lem  25435  nmoleub2lem2  25437  nmoleub3  25440  pjthlem1  25758  sca2rab  25833  ovolscalem1  25834  ovolsca  25836  itg2mulclem  26067  itg2mulc  26068  c1liplem1  26316  aalioulem4  26662  aaliou3lem8  26672  itgulm  26735  dvradcnv  26748  abelthlem7  26765  abelthlem8  26766  tanrpcl  26833  tanregt0  26867  efiarg  26935  argregt0  26938  argrege0  26939  argimgt0  26940  tanarg  26947  logdivlti  26948  logno1  26964  logcnlem4  26973  divcxp  27015  cxple2  27025  cxpcn3lem  27075  cxpcn3  27076  cxpaddlelem  27079  cxpaddle  27080  logbrec  27110  asinlem3  27199  rlimcnp  27293  rlimcnp2  27294  rlimcxp  27301  cxp2limlem  27303  cxp2lim  27304  cxploglim2  27306  jensenlem2  27315  amgmlem  27317  logdiflbnd  27322  lgamgulmlem2  27357  lgamucov  27365  basellem3  27410  basellem8  27415  isppw  27441  chpeq0  27535  chteq0  27536  bposlem9  27619  chebbnd1lem2  27797  chebbnd1  27799  chtppilimlem1  27800  chebbnd2  27804  chto1lb  27805  chpchtlim  27806  chpo1ubb  27808  rplogsumlem1  27811  rplogsumlem2  27812  dchrvmasumlem1  27822  dchrvmasum2lem  27823  dchrisum0lema  27841  dchrisum0lem1b  27842  dchrisum0lem1  27843  dchrisum0lem2a  27844  dchrisum0lem2  27845  dchrisum0lem3  27846  dchrisum0  27847  mulog2sumlem1  27861  vmalogdivsum2  27865  vmalogdivsum  27866  2vmadivsumlem  27867  chpdifbndlem1  27880  selberg3lem1  27884  selberg3lem2  27885  selberg3  27886  selberg4lem1  27887  selberg4  27888  selberg3r  27896  selberg4r  27897  selberg34r  27898  pntrlog2bndlem1  27904  pntrlog2bndlem2  27905  pntrlog2bndlem3  27906  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntrlog2bndlem6  27910  pntpbnd2  27914  pntibndlem2  27918  pntlemr  27929  pntlemo  27934  pnt2  27940  pnt  27941  padicabv  27957  padicabvcxp  27959  ostth2lem3  27962  ostth2lem4  27963  ostth3  27965  smcnlem  31299  pjhthlem1  31993  rpxdivcld  33500  xrmulc1cn  34562  esumdivc  34715  probmeasb  35062  signsply0  35180  divsqrtid  35223  hgt750leme  35287  circum  36439  iprodgam  36507  faclimlem1  36508  faclimlem3  36510  knoppndvlem17  37394  knoppndvlem18  37395  itg2addnclem3  38592  geomcau  38694  cntotbnd  38731  bfplem1  38757  rrncmslem  38767  rrnequiv  38770  relogbzexpd  43027  aks4d1p1p1  43114  dvrelogpow2b  43119  aks4d1p1p4  43122  aks4d1p1p6  43124  aks4d1p1p7  43125  aks4d1p5  43131  aks4d1p6  43132  exp11d  43384  rplog11d  43399  irrapxlem5  43833  pellfund14  43905  rmxyneg  43927  rmxyadd  43928  modabsdifz  43993  binomcxplemnotnn0  45340  oddfl  46294  xralrple3  46385  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  stoweidlem1  47011  stoweidlem14  47024  stoweidlem60  47070  wallispilem4  47078  wallispilem5  47079  wallispi  47080  wallispi2lem1  47081  stirlinglem1  47084  stirlinglem3  47086  stirlinglem4  47087  stirlinglem5  47088  stirlinglem8  47091  stirlinglem12  47095  stirlinglem15  47098  dirkertrigeqlem1  47108  dirkercncflem1  47113  dirkercncflem4  47116  fourierdlem30  47147  fourierdlem39  47156  fourierdlem47  47163  fourierdlem65  47181  fourierdlem73  47189  fourierdlem87  47203  qndenserrnbllem  47304  sge0rpcpnf  47431  hoiqssbllem2  47633  young2d  50990