Theorem rpne0d 11142

Description: A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	|- ( ph -> A e. RR+ )

Assertion

Ref	Expression
rpne0d	|- ( ph -> A =/= 0 )

Proof of Theorem rpne0d

Step	Hyp	Ref	Expression
1		rpred.1	. 2 |- ( ph -> A e. RR+ )
2		rpne0 11116	. 2 |- ( A e. RR+ -> A =/= 0 )
3	1, 2	syl 16	1 |- ( ph -> A =/= 0 )

Syntax hints:   -> wi 4   e. wcel 1758   =/= wne 2647   0cc0 9392   RR+crp 11101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-i2m1 9460  ax-1ne0 9461  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-po 4748  df-so 4749  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-er 7210  df-en 7420  df-dom 7421  df-sdom 7422  df-pnf 9530  df-mnf 9531  df-ltxr 9533  df-rp 11102

This theorem is referenced by:  rprene0d  11145  rpcnne0d  11146  iccf1o  11545  ltexp2r  12036  discr  12117  bcpasc  12213  sqrdiv  12872  abs00  12895  absdiv  12901  o1rlimmul  13213  geomulcvg  13453  mertenslem1  13461  retanhcl  13560  tanhlt1  13561  tanhbnd  13562  sylow1lem1  16217  nrginvrcnlem  20402  nmoi2  20440  reperflem  20526  icchmeo  20644  icopnfcnv  20645  nmoleub2lem  20800  nmoleub2lem2  20802  nmoleub3  20805  pjthlem1  21055  sca2rab  21126  ovolscalem1  21127  ovolsca  21129  itg2mulclem  21356  itg2mulc  21357  c1liplem1  21600  aalioulem4  21933  aaliou3lem8  21943  itgulm  22005  dvradcnv  22018  abelthlem7  22035  abelthlem8  22036  tanrpcl  22098  tanregt0  22127  efiarg  22188  argregt0  22191  argrege0  22192  argimgt0  22193  tanarg  22200  logdivlti  22201  logno1  22213  logcnlem4  22222  divcxp  22264  cxple2  22274  cxpcn3lem  22317  cxpcn3  22318  cxpaddlelem  22321  cxpaddle  22322  asinlem3  22398  rlimcnp  22491  rlimcnp2  22492  rlimcxp  22499  cxp2limlem  22501  cxp2lim  22502  cxploglim2  22504  jensenlem2  22513  amgmlem  22515  logdiflbnd  22520  basellem3  22552  basellem8  22557  isppw  22584  chpeq0  22679  chteq0  22680  bposlem9  22763  chebbnd1lem2  22851  chebbnd1  22853  chtppilimlem1  22854  chebbnd2  22858  chto1lb  22859  chpchtlim  22860  chpo1ubb  22862  rplogsumlem1  22865  rplogsumlem2  22866  dchrvmasumlem1  22876  dchrvmasum2lem  22877  dchrisum0lema  22895  dchrisum0lem1b  22896  dchrisum0lem1  22897  dchrisum0lem2a  22898  dchrisum0lem2  22899  dchrisum0lem3  22900  dchrisum0  22901  mulog2sumlem1  22915  vmalogdivsum2  22919  vmalogdivsum  22920  2vmadivsumlem  22921  chpdifbndlem1  22934  selberg3lem1  22938  selberg3lem2  22939  selberg3  22940  selberg4lem1  22941  selberg4  22942  selberg3r  22950  selberg4r  22951  selberg34r  22952  pntrlog2bndlem1  22958  pntrlog2bndlem2  22959  pntrlog2bndlem3  22960  pntrlog2bndlem4  22961  pntrlog2bndlem5  22962  pntrlog2bndlem6  22964  pntpbnd2  22968  pntibndlem2  22972  pntlemr  22983  pntlemo  22988  pnt2  22994  pnt  22995  padicabv  23011  ostth2lem3  23016  ostth2lem4  23017  ostth3  23019  smcnlem  24243  pjhthlem1  24945  rpxdivcld  26253  xrmulc1cn  26504  logbrec  26608  esumdivc  26676  probmeasb  26956  signsply0  27095  lgamgulmlem2  27159  lgamucov  27167  circum  27462  iprodgam  27649  faclimlem1  27692  faclimlem3  27694  itg2addnclem3  28592  geomcau  28802  cntotbnd  28842  bfplem1  28868  rrncmslem  28878  rrnequiv  28881  irrapxlem5  29314  pellfund14  29386  rmxyneg  29408  rmxyadd  29409  modabsdifz  29481  stoweidlem1  29943  stoweidlem14  29956  stoweidlem60  30002  wallispilem4  30010  wallispilem5  30011  wallispi  30012  wallispi2lem1  30013  stirlinglem1  30016  stirlinglem3  30018  stirlinglem4  30019  stirlinglem5  30020  stirlinglem8  30023  stirlinglem12  30027  stirlinglem15  30030