Theorem rpne0d 12988

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  0cc0 11035  ℝ⁺crp 12939

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 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-resscn 11092  ax-1cn 11093  ax-addrcl 11096  ax-rnegex 11106  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5523  df-po 5536  df-so 5537  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-ltxr 11181  df-rp 12940

This theorem is referenced by:  rprene0d  12991  rpcnne0d  12992  iccf1o  13446  ltexp2r  14132  discr  14199  bcpasc  14280  sqrtdiv  15224  abs00  15248  absdiv  15254  o1rlimmul  15578  geomulcvg  15838  mertenslem1  15846  retanhcl  16123  tanhlt1  16124  tanhbnd  16125  sylow1lem1  19570  nrginvrcnlem  24672  nmoi2  24711  reperflem  24800  icopnfcnv  24925  nmoleub2lem  25097  nmoleub2lem2  25099  nmoleub3  25102  pjthlem1  25420  sca2rab  25495  ovolscalem1  25496  ovolsca  25498  itg2mulclem  25729  itg2mulc  25730  c1liplem1  25979  aalioulem4  26318  aaliou3lem8  26328  itgulm  26392  dvradcnv  26405  abelthlem7  26422  abelthlem8  26423  tanrpcl  26487  tanregt0  26522  efiarg  26590  argregt0  26593  argrege0  26594  argimgt0  26595  tanarg  26602  logdivlti  26603  logno1  26619  logcnlem4  26628  divcxp  26670  cxple2  26680  cxpcn3lem  26730  cxpcn3  26731  cxpaddlelem  26734  cxpaddle  26735  logbrec  26765  asinlem3  26854  rlimcnp  26948  rlimcnp2  26949  rlimcxp  26957  cxp2limlem  26959  cxp2lim  26960  cxploglim2  26962  jensenlem2  26971  amgmlem  26973  logdiflbnd  26978  lgamgulmlem2  27013  lgamucov  27021  basellem3  27066  basellem8  27071  isppw  27097  chpeq0  27191  chteq0  27192  bposlem9  27275  chebbnd1lem2  27453  chebbnd1  27455  chtppilimlem1  27456  chebbnd2  27460  chto1lb  27461  chpchtlim  27462  chpo1ubb  27464  rplogsumlem1  27467  rplogsumlem2  27468  dchrvmasumlem1  27478  dchrvmasum2lem  27479  dchrisum0lema  27497  dchrisum0lem1b  27498  dchrisum0lem1  27499  dchrisum0lem2a  27500  dchrisum0lem2  27501  dchrisum0lem3  27502  dchrisum0  27503  mulog2sumlem1  27517  vmalogdivsum2  27521  vmalogdivsum  27522  2vmadivsumlem  27523  chpdifbndlem1  27536  selberg3lem1  27540  selberg3lem2  27541  selberg3  27542  selberg4lem1  27543  selberg4  27544  selberg3r  27552  selberg4r  27553  selberg34r  27554  pntrlog2bndlem1  27560  pntrlog2bndlem2  27561  pntrlog2bndlem3  27562  pntrlog2bndlem4  27563  pntrlog2bndlem5  27564  pntrlog2bndlem6  27566  pntpbnd2  27570  pntibndlem2  27574  pntlemr  27585  pntlemo  27590  pnt2  27596  pnt  27597  padicabv  27613  padicabvcxp  27615  ostth2lem3  27618  ostth2lem4  27619  ostth3  27621  smcnlem  30789  pjhthlem1  31483  rpxdivcld  33014  xrmulc1cn  34096  esumdivc  34249  probmeasb  34596  signsply0  34717  divsqrtid  34760  hgt750leme  34824  circum  35878  iprodgam  35946  faclimlem1  35947  faclimlem3  35949  knoppndvlem17  36810  knoppndvlem18  36811  itg2addnclem3  38016  geomcau  38102  cntotbnd  38139  bfplem1  38165  rrncmslem  38175  rrnequiv  38178  relogbzexpd  42437  aks4d1p1p1  42524  dvrelogpow2b  42529  aks4d1p1p4  42532  aks4d1p1p6  42534  aks4d1p1p7  42535  aks4d1p5  42541  aks4d1p6  42542  exp11d  42780  rplog11d  42801  irrapxlem5  43280  pellfund14  43352  rmxyneg  43374  rmxyadd  43375  modabsdifz  43440  binomcxplemnotnn0  44809  oddfl  45737  xralrple3  45829  ioodvbdlimc1lem2  46386  ioodvbdlimc2lem  46388  stoweidlem1  46455  stoweidlem14  46468  stoweidlem60  46514  wallispilem4  46522  wallispilem5  46523  wallispi  46524  wallispi2lem1  46525  stirlinglem1  46528  stirlinglem3  46530  stirlinglem4  46531  stirlinglem5  46532  stirlinglem8  46535  stirlinglem12  46539  stirlinglem15  46542  dirkertrigeqlem1  46552  dirkercncflem1  46557  dirkercncflem4  46560  fourierdlem30  46591  fourierdlem39  46600  fourierdlem47  46607  fourierdlem65  46625  fourierdlem73  46633  fourierdlem87  46647  qndenserrnbllem  46748  sge0rpcpnf  46875  hoiqssbllem2  47077  young2d  50300