Theorem rpne0d 11297

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

Syntax hints:   -> wi 4   e. wcel 1872   =/= wne 2599   0cc0 9490   RR+crp 11253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-i2m1 9558  ax-1ne0 9559  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-po 4717  df-so 4718  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-ov 6252  df-er 7318  df-en 7525  df-dom 7526  df-sdom 7527  df-pnf 9628  df-mnf 9629  df-ltxr 9631  df-rp 11254

This theorem is referenced by:  rprene0d  11300  rpcnne0d  11301  iccf1o  11727  ltexp2r  12279  discr  12359  bcpasc  12456  sqrtdiv  13273  abs00  13296  absdiv  13302  o1rlimmul  13625  geomulcvg  13875  mertenslem1  13883  retanhcl  14156  tanhlt1  14157  tanhbnd  14158  sylow1lem1  17193  nrginvrcnlem  21635  nmoi2  21677  nmoi2OLD  21693  reperflem  21778  icchmeo  21911  icopnfcnv  21912  nmoleub2lem  22070  nmoleub2lem2  22072  nmoleub3  22075  pjthlem1  22333  sca2rab  22407  ovolscalem1  22408  ovolsca  22410  itg2mulclem  22646  itg2mulc  22647  c1liplem1  22890  aalioulem4  23233  aaliou3lem8  23243  itgulm  23305  dvradcnv  23318  abelthlem7  23335  abelthlem8  23336  tanrpcl  23401  tanregt0  23430  efiarg  23498  argregt0  23501  argrege0  23502  argimgt0  23503  tanarg  23510  logdivlti  23511  logno1  23523  logcnlem4  23532  divcxp  23574  cxple2  23584  cxpcn3lem  23629  cxpcn3  23630  cxpaddlelem  23633  cxpaddle  23634  logbrec  23661  asinlem3  23739  rlimcnp  23833  rlimcnp2  23834  rlimcxp  23841  cxp2limlem  23843  cxp2lim  23844  cxploglim2  23846  jensenlem2  23855  amgmlem  23857  logdiflbnd  23862  lgamgulmlem2  23897  lgamucov  23905  basellem3  23951  basellem8  23956  isppw  23983  chpeq0  24078  chteq0  24079  bposlem9  24162  chebbnd1lem2  24250  chebbnd1  24252  chtppilimlem1  24253  chebbnd2  24257  chto1lb  24258  chpchtlim  24259  chpo1ubb  24261  rplogsumlem1  24264  rplogsumlem2  24265  dchrvmasumlem1  24275  dchrvmasum2lem  24276  dchrisum0lema  24294  dchrisum0lem1b  24295  dchrisum0lem1  24296  dchrisum0lem2a  24297  dchrisum0lem2  24298  dchrisum0lem3  24299  dchrisum0  24300  mulog2sumlem1  24314  vmalogdivsum2  24318  vmalogdivsum  24319  2vmadivsumlem  24320  chpdifbndlem1  24333  selberg3lem1  24337  selberg3lem2  24338  selberg3  24339  selberg4lem1  24340  selberg4  24341  selberg3r  24349  selberg4r  24350  selberg34r  24351  pntrlog2bndlem1  24357  pntrlog2bndlem2  24358  pntrlog2bndlem3  24359  pntrlog2bndlem4  24360  pntrlog2bndlem5  24361  pntrlog2bndlem6  24363  pntpbnd2  24367  pntibndlem2  24371  pntlemr  24382  pntlemo  24387  pnt2  24393  pnt  24394  padicabv  24410  ostth2lem3  24415  ostth2lem4  24416  ostth3  24418  smcnlem  26275  pjhthlem1  26986  rpxdivcld  28354  xrmulc1cn  28688  esumdivc  28856  probmeasb  29215  signsply0  29392  circum  30270  iprodgam  30329  faclimlem1  30330  faclimlem3  30332  itg2addnclem3  31902  geomcau  31995  cntotbnd  32035  bfplem1  32061  rrncmslem  32071  rrnequiv  32074  irrapxlem5  35583  pellfund14  35659  rmxyneg  35681  rmxyadd  35682  modabsdifz  35752  binomcxplemnotnn0  36618  oddfl  37384  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  stoweidlem1  37744  stoweidlem14  37757  stoweidlem60  37804  wallispilem4  37813  wallispilem5  37814  wallispi  37815  wallispi2lem1  37816  stirlinglem1  37819  stirlinglem3  37821  stirlinglem4  37822  stirlinglem5  37823  stirlinglem8  37826  stirlinglem12  37830  stirlinglem15  37833  dirkertrigeqlem1  37843  dirkercncflem1  37848  dirkercncflem4  37851  fourierdlem30  37882  fourierdlem39  37892  fourierdlem47  37900  fourierdlem65  37918  fourierdlem73  37926  fourierdlem87  37940  sge0rpcpnf  38114