Theorem rpne0d 13085

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

Syntax hints:   → wi 4   ∈ wcel 2100   ≠ wne 2933  0cc0 11165  ℝ⁺crp 13038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751  ax-resscn 11222  ax-1cn 11223  ax-addrcl 11226  ax-rnegex 11236  ax-cnre 11238  ax-pre-lttri 11239  ax-pre-lttrn 11240

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-po 5598  df-so 5599  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-er 8742  df-en 8983  df-dom 8984  df-sdom 8985  df-pnf 11307  df-mnf 11308  df-ltxr 11310  df-rp 13039

This theorem is referenced by:  rprene0d  13088  rpcnne0d  13089  iccf1o  13537  ltexp2r  14203  discr  14269  bcpasc  14350  sqrtdiv  15291  abs00  15315  absdiv  15321  o1rlimmul  15642  geomulcvg  15901  mertenslem1  15909  retanhcl  16182  tanhlt1  16183  tanhbnd  16184  sylow1lem1  19618  nrginvrcnlem  24722  nmoi2  24761  reperflem  24848  icchmeoOLD  24980  icopnfcnv  24981  nmoleub2lem  25155  nmoleub2lem2  25157  nmoleub3  25160  pjthlem1  25479  sca2rab  25555  ovolscalem1  25556  ovolsca  25558  itg2mulclem  25790  itg2mulc  25791  c1liplem1  26043  aalioulem4  26386  aaliou3lem8  26396  itgulm  26460  dvradcnv  26473  abelthlem7  26491  abelthlem8  26492  tanrpcl  26555  tanregt0  26589  efiarg  26657  argregt0  26660  argrege0  26661  argimgt0  26662  tanarg  26669  logdivlti  26670  logno1  26686  logcnlem4  26695  divcxp  26737  cxple2  26747  cxpcn3lem  26798  cxpcn3  26799  cxpaddlelem  26802  cxpaddle  26803  logbrec  26833  asinlem3  26922  rlimcnp  27016  rlimcnp2  27017  rlimcxp  27025  cxp2limlem  27027  cxp2lim  27028  cxploglim2  27030  jensenlem2  27039  amgmlem  27041  logdiflbnd  27046  lgamgulmlem2  27081  lgamucov  27089  basellem3  27134  basellem8  27139  isppw  27165  chpeq0  27260  chteq0  27261  bposlem9  27344  chebbnd1lem2  27522  chebbnd1  27524  chtppilimlem1  27525  chebbnd2  27529  chto1lb  27530  chpchtlim  27531  chpo1ubb  27533  rplogsumlem1  27536  rplogsumlem2  27537  dchrvmasumlem1  27547  dchrvmasum2lem  27548  dchrisum0lema  27566  dchrisum0lem1b  27567  dchrisum0lem1  27568  dchrisum0lem2a  27569  dchrisum0lem2  27570  dchrisum0lem3  27571  dchrisum0  27572  mulog2sumlem1  27586  vmalogdivsum2  27590  vmalogdivsum  27591  2vmadivsumlem  27592  chpdifbndlem1  27605  selberg3lem1  27609  selberg3lem2  27610  selberg3  27611  selberg4lem1  27612  selberg4  27613  selberg3r  27621  selberg4r  27622  selberg34r  27623  pntrlog2bndlem1  27629  pntrlog2bndlem2  27630  pntrlog2bndlem3  27631  pntrlog2bndlem4  27632  pntrlog2bndlem5  27633  pntrlog2bndlem6  27635  pntpbnd2  27639  pntibndlem2  27643  pntlemr  27654  pntlemo  27659  pnt2  27665  pnt  27666  padicabv  27682  padicabvcxp  27684  ostth2lem3  27687  ostth2lem4  27688  ostth3  27690  smcnlem  30653  pjhthlem1  31347  rpxdivcld  32823  xrmulc1cn  33783  esumdivc  33954  probmeasb  34302  signsply0  34435  divsqrtid  34478  hgt750leme  34542  circum  35549  iprodgam  35611  faclimlem1  35612  faclimlem3  35614  knoppndvlem17  36279  knoppndvlem18  36280  itg2addnclem3  37421  geomcau  37507  cntotbnd  37544  bfplem1  37570  rrncmslem  37580  rrnequiv  37583  relogbzexpd  41720  aks4d1p1p1  41809  dvrelogpow2b  41814  aks4d1p1p4  41817  aks4d1p1p6  41819  aks4d1p1p7  41820  aks4d1p5  41826  aks4d1p6  41827  exp11d  42086  rplog11d  42108  irrapxlem5  42554  pellfund14  42626  rmxyneg  42649  rmxyadd  42650  modabsdifz  42715  binomcxplemnotnn0  44101  oddfl  44962  xralrple3  45059  ioodvbdlimc1lem2  45623  ioodvbdlimc2lem  45625  stoweidlem1  45692  stoweidlem14  45705  stoweidlem60  45751  wallispilem4  45759  wallispilem5  45760  wallispi  45761  wallispi2lem1  45762  stirlinglem1  45765  stirlinglem3  45767  stirlinglem4  45768  stirlinglem5  45769  stirlinglem8  45772  stirlinglem12  45776  stirlinglem15  45779  dirkertrigeqlem1  45789  dirkercncflem1  45794  dirkercncflem4  45797  fourierdlem30  45828  fourierdlem39  45837  fourierdlem47  45844  fourierdlem65  45862  fourierdlem73  45870  fourierdlem87  45884  qndenserrnbllem  45985  sge0rpcpnf  46112  hoiqssbllem2  46314  young2d  48634