Theorem rpne0d 12968

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

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

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 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-resscn 11097  ax-1cn 11098  ax-addrcl 11101  ax-rnegex 11111  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115

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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-po 5542  df-so 5543  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-ltxr 11185  df-rp 12920

This theorem is referenced by:  rprene0d  12971  rpcnne0d  12972  iccf1o  13426  ltexp2r  14110  discr  14177  bcpasc  14258  sqrtdiv  15202  abs00  15226  absdiv  15232  o1rlimmul  15556  geomulcvg  15813  mertenslem1  15821  retanhcl  16098  tanhlt1  16099  tanhbnd  16100  sylow1lem1  19544  nrginvrcnlem  24652  nmoi2  24691  reperflem  24780  icchmeoOLD  24912  icopnfcnv  24913  nmoleub2lem  25087  nmoleub2lem2  25089  nmoleub3  25092  pjthlem1  25410  sca2rab  25486  ovolscalem1  25487  ovolsca  25489  itg2mulclem  25720  itg2mulc  25721  c1liplem1  25974  aalioulem4  26316  aaliou3lem8  26326  itgulm  26390  dvradcnv  26403  abelthlem7  26421  abelthlem8  26422  tanrpcl  26486  tanregt0  26521  efiarg  26589  argregt0  26592  argrege0  26593  argimgt0  26594  tanarg  26601  logdivlti  26602  logno1  26618  logcnlem4  26627  divcxp  26669  cxple2  26679  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  27192  chteq0  27193  bposlem9  27276  chebbnd1lem2  27454  chebbnd1  27456  chtppilimlem1  27457  chebbnd2  27461  chto1lb  27462  chpchtlim  27463  chpo1ubb  27465  rplogsumlem1  27468  rplogsumlem2  27469  dchrvmasumlem1  27479  dchrvmasum2lem  27480  dchrisum0lema  27498  dchrisum0lem1b  27499  dchrisum0lem1  27500  dchrisum0lem2a  27501  dchrisum0lem2  27502  dchrisum0lem3  27503  dchrisum0  27504  mulog2sumlem1  27518  vmalogdivsum2  27522  vmalogdivsum  27523  2vmadivsumlem  27524  chpdifbndlem1  27537  selberg3lem1  27541  selberg3lem2  27542  selberg3  27543  selberg4lem1  27544  selberg4  27545  selberg3r  27553  selberg4r  27554  selberg34r  27555  pntrlog2bndlem1  27561  pntrlog2bndlem2  27562  pntrlog2bndlem3  27563  pntrlog2bndlem4  27564  pntrlog2bndlem5  27565  pntrlog2bndlem6  27567  pntpbnd2  27571  pntibndlem2  27575  pntlemr  27586  pntlemo  27591  pnt2  27597  pnt  27598  padicabv  27614  padicabvcxp  27616  ostth2lem3  27619  ostth2lem4  27620  ostth3  27622  smcnlem  30791  pjhthlem1  31485  rpxdivcld  33032  xrmulc1cn  34114  esumdivc  34267  probmeasb  34614  signsply0  34735  divsqrtid  34778  hgt750leme  34842  circum  35896  iprodgam  35964  faclimlem1  35965  faclimlem3  35967  knoppndvlem17  36756  knoppndvlem18  36757  itg2addnclem3  37953  geomcau  38039  cntotbnd  38076  bfplem1  38102  rrncmslem  38112  rrnequiv  38115  relogbzexpd  42374  aks4d1p1p1  42462  dvrelogpow2b  42467  aks4d1p1p4  42470  aks4d1p1p6  42472  aks4d1p1p7  42473  aks4d1p5  42479  aks4d1p6  42480  exp11d  42725  rplog11d  42746  irrapxlem5  43212  pellfund14  43284  rmxyneg  43306  rmxyadd  43307  modabsdifz  43372  binomcxplemnotnn0  44741  oddfl  45669  xralrple3  45761  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  stoweidlem1  46388  stoweidlem14  46401  stoweidlem60  46447  wallispilem4  46455  wallispilem5  46456  wallispi  46457  wallispi2lem1  46458  stirlinglem1  46461  stirlinglem3  46463  stirlinglem4  46464  stirlinglem5  46465  stirlinglem8  46468  stirlinglem12  46472  stirlinglem15  46475  dirkertrigeqlem1  46485  dirkercncflem1  46490  dirkercncflem4  46493  fourierdlem30  46524  fourierdlem39  46533  fourierdlem47  46540  fourierdlem65  46558  fourierdlem73  46566  fourierdlem87  46580  qndenserrnbllem  46681  sge0rpcpnf  46808  hoiqssbllem2  47010  young2d  50193