Theorem rpne0d 13124

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2955  0cc0 11157  ℝ⁺crp 13075

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-resscn 11214  ax-1cn 11215  ax-addrcl 11218  ax-rnegex 11228  ax-cnre 11230  ax-pre-lttri 11231  ax-pre-lttrn 11232

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 2100  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 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11302  df-mnf 11303  df-ltxr 11305  df-rp 13076

This theorem is used by:  rprene0d  13127  rpcnne0d  13128  iccf1o  13582  ltexp2r  14270  discr  14337  bcpasc  14418  sqrtdiv  15385  abs00  15409  absdiv  15415  o1rlimmul  15739  geomulcvg  15998  mertenslem1  16006  retanhcl  16280  tanhlt1  16281  tanhbnd  16282  sylow1lem1  19759  nrginvrcnlem  24957  nmoi2  24996  reperflem  25085  icopnfcnv  25210  nmoleub2lem  25382  nmoleub2lem2  25384  nmoleub3  25387  pjthlem1  25705  sca2rab  25780  ovolscalem1  25781  ovolsca  25783  itg2mulclem  26014  itg2mulc  26015  c1liplem1  26263  aalioulem4  26611  aaliou3lem8  26621  itgulm  26684  dvradcnv  26697  abelthlem7  26714  abelthlem8  26715  tanrpcl  26782  tanregt0  26816  efiarg  26884  argregt0  26887  argrege0  26888  argimgt0  26889  tanarg  26896  logdivlti  26897  logno1  26913  logcnlem4  26922  divcxp  26964  cxple2  26974  cxpcn3lem  27024  cxpcn3  27025  cxpaddlelem  27028  cxpaddle  27029  logbrec  27059  asinlem3  27148  rlimcnp  27242  rlimcnp2  27243  rlimcxp  27250  cxp2limlem  27252  cxp2lim  27253  cxploglim2  27255  jensenlem2  27264  amgmlem  27266  logdiflbnd  27271  lgamgulmlem2  27306  lgamucov  27314  basellem3  27359  basellem8  27364  isppw  27390  chpeq0  27484  chteq0  27485  bposlem9  27568  chebbnd1lem2  27746  chebbnd1  27748  chtppilimlem1  27749  chebbnd2  27753  chto1lb  27754  chpchtlim  27755  chpo1ubb  27757  rplogsumlem1  27760  rplogsumlem2  27761  dchrvmasumlem1  27771  dchrvmasum2lem  27772  dchrisum0lema  27790  dchrisum0lem1b  27791  dchrisum0lem1  27792  dchrisum0lem2a  27793  dchrisum0lem2  27794  dchrisum0lem3  27795  dchrisum0  27796  mulog2sumlem1  27810  vmalogdivsum2  27814  vmalogdivsum  27815  2vmadivsumlem  27816  chpdifbndlem1  27829  selberg3lem1  27833  selberg3lem2  27834  selberg3  27835  selberg4lem1  27836  selberg4  27837  selberg3r  27845  selberg4r  27846  selberg34r  27847  pntrlog2bndlem1  27853  pntrlog2bndlem2  27854  pntrlog2bndlem3  27855  pntrlog2bndlem4  27856  pntrlog2bndlem5  27857  pntrlog2bndlem6  27859  pntpbnd2  27863  pntibndlem2  27867  pntlemr  27878  pntlemo  27883  pnt2  27889  pnt  27890  padicabv  27906  padicabvcxp  27908  ostth2lem3  27911  ostth2lem4  27912  ostth3  27914  smcnlem  31218  pjhthlem1  31912  rpxdivcld  33419  xrmulc1cn  34481  esumdivc  34634  probmeasb  34982  signsply0  35100  divsqrtid  35143  hgt750leme  35207  circum  36354  iprodgam  36422  faclimlem1  36423  faclimlem3  36425  knoppndvlem17  37310  knoppndvlem18  37311  itg2addnclem3  38505  geomcau  38607  cntotbnd  38644  bfplem1  38670  rrncmslem  38680  rrnequiv  38683  relogbzexpd  42940  aks4d1p1p1  43027  dvrelogpow2b  43032  aks4d1p1p4  43035  aks4d1p1p6  43037  aks4d1p1p7  43038  aks4d1p5  43044  aks4d1p6  43045  exp11d  43299  rplog11d  43320  irrapxlem5  43765  pellfund14  43837  rmxyneg  43859  rmxyadd  43860  modabsdifz  43925  binomcxplemnotnn0  45278  oddfl  46209  xralrple3  46301  ioodvbdlimc1lem2  46858  ioodvbdlimc2lem  46860  stoweidlem1  46927  stoweidlem14  46940  stoweidlem60  46986  wallispilem4  46994  wallispilem5  46995  wallispi  46996  wallispi2lem1  46997  stirlinglem1  47000  stirlinglem3  47002  stirlinglem4  47003  stirlinglem5  47004  stirlinglem8  47007  stirlinglem12  47011  stirlinglem15  47014  dirkertrigeqlem1  47024  dirkercncflem1  47029  dirkercncflem4  47032  fourierdlem30  47063  fourierdlem39  47072  fourierdlem47  47079  fourierdlem65  47097  fourierdlem73  47105  fourierdlem87  47119  qndenserrnbllem  47220  sge0rpcpnf  47347  hoiqssbllem2  47549  young2d  50906