Theorem rpne0d 11020

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 10994	. 2 |- ( A e. RR+ -> A =/= 0 )
3	1, 2	syl 16	1 |- ( ph -> A =/= 0 )

Syntax hints:   -> wi 4   e. wcel 1755   =/= wne 2596   0cc0 9270   RR+crp 10979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-i2m1 9338  ax-1ne0 9339  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-po 4628  df-so 4629  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9408  df-mnf 9409  df-ltxr 9411  df-rp 10980

This theorem is referenced by:  rprene0d  11023  rpcnne0d  11024  iccf1o  11416  ltexp2r  11904  discr  11985  bcpasc  12081  sqrdiv  12739  abs00  12762  absdiv  12768  o1rlimmul  13080  geomulcvg  13319  mertenslem1  13327  retanhcl  13426  tanhlt1  13427  tanhbnd  13428  sylow1lem1  16077  nrginvrcnlem  20113  nmoi2  20151  reperflem  20237  icchmeo  20355  icopnfcnv  20356  nmoleub2lem  20511  nmoleub2lem2  20513  nmoleub3  20516  pjthlem1  20766  sca2rab  20837  ovolscalem1  20838  ovolsca  20840  itg2mulclem  21066  itg2mulc  21067  c1liplem1  21310  aalioulem4  21686  aaliou3lem8  21696  itgulm  21758  dvradcnv  21771  abelthlem7  21788  abelthlem8  21789  tanrpcl  21851  tanregt0  21880  efiarg  21941  argregt0  21944  argrege0  21945  argimgt0  21946  tanarg  21953  logdivlti  21954  logno1  21966  logcnlem4  21975  divcxp  22017  cxple2  22027  cxpcn3lem  22070  cxpcn3  22071  cxpaddlelem  22074  cxpaddle  22075  asinlem3  22151  rlimcnp  22244  rlimcnp2  22245  rlimcxp  22252  cxp2limlem  22254  cxp2lim  22255  cxploglim2  22257  jensenlem2  22266  amgmlem  22268  logdiflbnd  22273  basellem3  22305  basellem8  22310  isppw  22337  chpeq0  22432  chteq0  22433  bposlem9  22516  chebbnd1lem2  22604  chebbnd1  22606  chtppilimlem1  22607  chebbnd2  22611  chto1lb  22612  chpchtlim  22613  chpo1ubb  22615  rplogsumlem1  22618  rplogsumlem2  22619  dchrvmasumlem1  22629  dchrvmasum2lem  22630  dchrisum0lema  22648  dchrisum0lem1b  22649  dchrisum0lem1  22650  dchrisum0lem2a  22651  dchrisum0lem2  22652  dchrisum0lem3  22653  dchrisum0  22654  mulog2sumlem1  22668  vmalogdivsum2  22672  vmalogdivsum  22673  2vmadivsumlem  22674  chpdifbndlem1  22687  selberg3lem1  22691  selberg3lem2  22692  selberg3  22693  selberg4lem1  22694  selberg4  22695  selberg3r  22703  selberg4r  22704  selberg34r  22705  pntrlog2bndlem1  22711  pntrlog2bndlem2  22712  pntrlog2bndlem3  22713  pntrlog2bndlem4  22714  pntrlog2bndlem5  22715  pntrlog2bndlem6  22717  pntpbnd2  22721  pntibndlem2  22725  pntlemr  22736  pntlemo  22741  pnt2  22747  pnt  22748  padicabv  22764  ostth2lem3  22769  ostth2lem4  22770  ostth3  22772  smcnlem  23915  pjhthlem1  24617  rpxdivcld  25932  xrmulc1cn  26214  logbrec  26318  esumdivc  26386  probmeasb  26661  signsply0  26800  lgamgulmlem2  26864  lgamucov  26872  circum  27166  iprodgam  27353  faclimlem1  27396  faclimlem3  27398  itg2addnclem3  28289  geomcau  28499  cntotbnd  28539  bfplem1  28565  rrncmslem  28575  rrnequiv  28578  irrapxlem5  29012  pellfund14  29084  rmxyneg  29106  rmxyadd  29107  modabsdifz  29179  stoweidlem1  29642  stoweidlem14  29655  stoweidlem60  29701  wallispilem4  29709  wallispilem5  29710  wallispi  29711  wallispi2lem1  29712  stirlinglem1  29715  stirlinglem3  29717  stirlinglem4  29718  stirlinglem5  29719  stirlinglem8  29722  stirlinglem12  29726  stirlinglem15  29729