Theorem rpne0d 13193

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959  0cc0 11224  ℝ⁺crp 13144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-resscn 11281  ax-1cn 11282  ax-addrcl 11285  ax-rnegex 11295  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-pnf 11369  df-mnf 11370  df-ltxr 11372  df-rp 13145

This theorem is used by:  rprene0d  13196  rpcnne0d  13197  iccf1o  13651  ltexp2r  14340  discr  14408  bcpasc  14489  sqrtdiv  15458  abs00  15482  absdiv  15488  o1rlimmul  15812  geomulcvg  16071  mertenslem1  16079  retanhcl  16353  tanhlt1  16354  tanhbnd  16355  sylow1lem1  19839  nrginvrcnlem  25037  nmoi2  25076  reperflem  25165  icopnfcnv  25290  nmoleub2lem  25462  nmoleub2lem2  25464  nmoleub3  25467  pjthlem1  25785  sca2rab  25860  ovolscalem1  25861  ovolsca  25863  itg2mulclem  26094  itg2mulc  26095  c1liplem1  26343  aalioulem4  26689  aaliou3lem8  26699  itgulm  26762  dvradcnv  26775  abelthlem7  26792  abelthlem8  26793  tanrpcl  26860  tanregt0  26894  efiarg  26962  argregt0  26965  argrege0  26966  argimgt0  26967  tanarg  26974  logdivlti  26975  logno1  26991  logcnlem4  27000  divcxp  27042  cxple2  27052  cxpcn3lem  27102  cxpcn3  27103  cxpaddlelem  27106  cxpaddle  27107  logbrec  27137  asinlem3  27226  rlimcnp  27320  rlimcnp2  27321  rlimcxp  27328  cxp2limlem  27330  cxp2lim  27331  cxploglim2  27333  jensenlem2  27342  amgmlem  27344  logdiflbnd  27349  lgamgulmlem2  27384  lgamucov  27392  basellem3  27437  basellem8  27442  isppw  27468  chpeq0  27562  chteq0  27563  bposlem9  27646  chebbnd1lem2  27824  chebbnd1  27826  chtppilimlem1  27827  chebbnd2  27831  chto1lb  27832  chpchtlim  27833  chpo1ubb  27835  rplogsumlem1  27838  rplogsumlem2  27839  dchrvmasumlem1  27849  dchrvmasum2lem  27850  dchrisum0lema  27868  dchrisum0lem1b  27869  dchrisum0lem1  27870  dchrisum0lem2a  27871  dchrisum0lem2  27872  dchrisum0lem3  27873  dchrisum0  27874  mulog2sumlem1  27888  vmalogdivsum2  27892  vmalogdivsum  27893  2vmadivsumlem  27894  chpdifbndlem1  27907  selberg3lem1  27911  selberg3lem2  27912  selberg3  27913  selberg4lem1  27914  selberg4  27915  selberg3r  27923  selberg4r  27924  selberg34r  27925  pntrlog2bndlem1  27931  pntrlog2bndlem2  27932  pntrlog2bndlem3  27933  pntrlog2bndlem4  27934  pntrlog2bndlem5  27935  pntrlog2bndlem6  27937  pntpbnd2  27941  pntibndlem2  27945  pntlemr  27956  pntlemo  27961  pnt2  27967  pnt  27968  padicabv  27984  padicabvcxp  27986  ostth2lem3  27989  ostth2lem4  27990  ostth3  27992  smcnlem  31326  pjhthlem1  32020  rpxdivcld  33567  xrmulc1cn  34629  esumdivc  34782  probmeasb  35129  signsply0  35247  divsqrtid  35290  hgt750leme  35354  circum  36605  iprodgam  36684  faclimlem1  36685  faclimlem3  36687  knoppndvlem17  37571  knoppndvlem18  37572  itg2addnclem3  38782  geomcau  38884  cntotbnd  38921  bfplem1  38947  rrncmslem  38957  rrnequiv  38960  relogbzexpd  43217  aks4d1p1p1  43304  dvrelogpow2b  43309  aks4d1p1p4  43312  aks4d1p1p6  43314  aks4d1p1p7  43315  aks4d1p5  43321  aks4d1p6  43322  exp11d  43574  rplog11d  43589  irrapxlem5  44024  pellfund14  44096  rmxyneg  44118  rmxyadd  44119  modabsdifz  44184  binomcxplemnotnn0  45530  oddfl  46497  xralrple3  46588  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  stoweidlem1  47214  stoweidlem14  47227  stoweidlem60  47273  wallispilem4  47281  wallispilem5  47282  wallispi  47283  wallispi2lem1  47284  stirlinglem1  47287  stirlinglem3  47289  stirlinglem4  47290  stirlinglem5  47291  stirlinglem8  47294  stirlinglem12  47298  stirlinglem15  47301  dirkertrigeqlem1  47311  dirkercncflem1  47316  dirkercncflem4  47319  fourierdlem30  47350  fourierdlem39  47359  fourierdlem47  47366  fourierdlem65  47384  fourierdlem73  47392  fourierdlem87  47406  qndenserrnbllem  47507  sge0rpcpnf  47634  hoiqssbllem2  47836  young2d  51268