Theorem rpne0d 12286

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

Syntax hints:   → wi 4   ∈ wcel 2081   ≠ wne 2984  0cc0 10383  ℝ⁺crp 12239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-resscn 10440  ax-1cn 10441  ax-addrcl 10444  ax-rnegex 10454  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-po 5362  df-so 5363  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-pnf 10523  df-mnf 10524  df-ltxr 10526  df-rp 12240

This theorem is referenced by:  rprene0d  12289  rpcnne0d  12290  iccf1o  12732  ltexp2r  13387  discr  13451  bcpasc  13531  sqrtdiv  14459  abs00  14483  absdiv  14489  o1rlimmul  14809  geomulcvg  15065  mertenslem1  15073  retanhcl  15345  tanhlt1  15346  tanhbnd  15347  sylow1lem1  18453  nrginvrcnlem  22983  nmoi2  23022  reperflem  23109  icchmeo  23228  icopnfcnv  23229  nmoleub2lem  23401  nmoleub2lem2  23403  nmoleub3  23406  pjthlem1  23723  sca2rab  23796  ovolscalem1  23797  ovolsca  23799  itg2mulclem  24030  itg2mulc  24031  c1liplem1  24276  aalioulem4  24607  aaliou3lem8  24617  itgulm  24679  dvradcnv  24692  abelthlem7  24709  abelthlem8  24710  tanrpcl  24773  tanregt0  24804  efiarg  24871  argregt0  24874  argrege0  24875  argimgt0  24876  tanarg  24883  logdivlti  24884  logno1  24900  logcnlem4  24909  divcxp  24951  cxple2  24961  cxpcn3lem  25009  cxpcn3  25010  cxpaddlelem  25013  cxpaddle  25014  logbrec  25041  asinlem3  25130  rlimcnp  25225  rlimcnp2  25226  rlimcxp  25233  cxp2limlem  25235  cxp2lim  25236  cxploglim2  25238  jensenlem2  25247  amgmlem  25249  logdiflbnd  25254  lgamgulmlem2  25289  lgamucov  25297  basellem3  25342  basellem8  25347  isppw  25373  chpeq0  25466  chteq0  25467  bposlem9  25550  chebbnd1lem2  25728  chebbnd1  25730  chtppilimlem1  25731  chebbnd2  25735  chto1lb  25736  chpchtlim  25737  chpo1ubb  25739  rplogsumlem1  25742  rplogsumlem2  25743  dchrvmasumlem1  25753  dchrvmasum2lem  25754  dchrisum0lema  25772  dchrisum0lem1b  25773  dchrisum0lem1  25774  dchrisum0lem2a  25775  dchrisum0lem2  25776  dchrisum0lem3  25777  dchrisum0  25778  mulog2sumlem1  25792  vmalogdivsum2  25796  vmalogdivsum  25797  2vmadivsumlem  25798  chpdifbndlem1  25811  selberg3lem1  25815  selberg3lem2  25816  selberg3  25817  selberg4lem1  25818  selberg4  25819  selberg3r  25827  selberg4r  25828  selberg34r  25829  pntrlog2bndlem1  25835  pntrlog2bndlem2  25836  pntrlog2bndlem3  25837  pntrlog2bndlem4  25838  pntrlog2bndlem5  25839  pntrlog2bndlem6  25841  pntpbnd2  25845  pntibndlem2  25849  pntlemr  25860  pntlemo  25865  pnt2  25871  pnt  25872  padicabv  25888  padicabvcxp  25890  ostth2lem3  25893  ostth2lem4  25894  ostth3  25896  smcnlem  28165  pjhthlem1  28859  rpxdivcld  30294  xrmulc1cn  30790  esumdivc  30959  probmeasb  31305  signsply0  31438  divsqrtid  31482  hgt750leme  31546  circum  32525  iprodgam  32582  faclimlem1  32583  faclimlem3  32585  knoppndvlem17  33476  knoppndvlem18  33477  itg2addnclem3  34476  geomcau  34566  cntotbnd  34606  bfplem1  34632  rrncmslem  34642  rrnequiv  34645  cxpgt0d  38702  exp11d  38711  irrapxlem5  38908  pellfund14  38980  rmxyneg  39002  rmxyadd  39003  modabsdifz  39068  binomcxplemnotnn0  40226  oddfl  41084  xralrple3  41183  ioodvbdlimc1lem2  41758  ioodvbdlimc2lem  41760  stoweidlem1  41828  stoweidlem14  41841  stoweidlem60  41887  wallispilem4  41895  wallispilem5  41896  wallispi  41897  wallispi2lem1  41898  stirlinglem1  41901  stirlinglem3  41903  stirlinglem4  41904  stirlinglem5  41905  stirlinglem8  41908  stirlinglem12  41912  stirlinglem15  41915  dirkertrigeqlem1  41925  dirkercncflem1  41930  dirkercncflem4  41933  fourierdlem30  41964  fourierdlem39  41973  fourierdlem47  41980  fourierdlem65  41998  fourierdlem73  42006  fourierdlem87  42020  qndenserrnbllem  42121  sge0rpcpnf  42245  hoiqssbllem2  42447  young2d  44386