Theorem rpne0d 12958

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

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

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 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-addrcl 11091  ax-rnegex 11101  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105

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 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-rp 12910

This theorem is referenced by:  rprene0d  12961  rpcnne0d  12962  iccf1o  13416  ltexp2r  14100  discr  14167  bcpasc  14248  sqrtdiv  15192  abs00  15216  absdiv  15222  o1rlimmul  15546  geomulcvg  15803  mertenslem1  15811  retanhcl  16088  tanhlt1  16089  tanhbnd  16090  sylow1lem1  19531  nrginvrcnlem  24639  nmoi2  24678  reperflem  24767  icchmeoOLD  24899  icopnfcnv  24900  nmoleub2lem  25074  nmoleub2lem2  25076  nmoleub3  25079  pjthlem1  25397  sca2rab  25473  ovolscalem1  25474  ovolsca  25476  itg2mulclem  25707  itg2mulc  25708  c1liplem1  25961  aalioulem4  26303  aaliou3lem8  26313  itgulm  26377  dvradcnv  26390  abelthlem7  26408  abelthlem8  26409  tanrpcl  26473  tanregt0  26508  efiarg  26576  argregt0  26579  argrege0  26580  argimgt0  26581  tanarg  26588  logdivlti  26589  logno1  26605  logcnlem4  26614  divcxp  26656  cxple2  26666  cxpcn3lem  26717  cxpcn3  26718  cxpaddlelem  26721  cxpaddle  26722  logbrec  26752  asinlem3  26841  rlimcnp  26935  rlimcnp2  26936  rlimcxp  26944  cxp2limlem  26946  cxp2lim  26947  cxploglim2  26949  jensenlem2  26958  amgmlem  26960  logdiflbnd  26965  lgamgulmlem2  27000  lgamucov  27008  basellem3  27053  basellem8  27058  isppw  27084  chpeq0  27179  chteq0  27180  bposlem9  27263  chebbnd1lem2  27441  chebbnd1  27443  chtppilimlem1  27444  chebbnd2  27448  chto1lb  27449  chpchtlim  27450  chpo1ubb  27452  rplogsumlem1  27455  rplogsumlem2  27456  dchrvmasumlem1  27466  dchrvmasum2lem  27467  dchrisum0lema  27485  dchrisum0lem1b  27486  dchrisum0lem1  27487  dchrisum0lem2a  27488  dchrisum0lem2  27489  dchrisum0lem3  27490  dchrisum0  27491  mulog2sumlem1  27505  vmalogdivsum2  27509  vmalogdivsum  27510  2vmadivsumlem  27511  chpdifbndlem1  27524  selberg3lem1  27528  selberg3lem2  27529  selberg3  27530  selberg4lem1  27531  selberg4  27532  selberg3r  27540  selberg4r  27541  selberg34r  27542  pntrlog2bndlem1  27548  pntrlog2bndlem2  27549  pntrlog2bndlem3  27550  pntrlog2bndlem4  27551  pntrlog2bndlem5  27552  pntrlog2bndlem6  27554  pntpbnd2  27558  pntibndlem2  27562  pntlemr  27573  pntlemo  27578  pnt2  27584  pnt  27585  padicabv  27601  padicabvcxp  27603  ostth2lem3  27606  ostth2lem4  27607  ostth3  27609  smcnlem  30776  pjhthlem1  31470  rpxdivcld  33017  xrmulc1cn  34089  esumdivc  34242  probmeasb  34589  signsply0  34710  divsqrtid  34753  hgt750leme  34817  circum  35870  iprodgam  35938  faclimlem1  35939  faclimlem3  35941  knoppndvlem17  36730  knoppndvlem18  36731  itg2addnclem3  37876  geomcau  37962  cntotbnd  37999  bfplem1  38025  rrncmslem  38035  rrnequiv  38038  relogbzexpd  42297  aks4d1p1p1  42385  dvrelogpow2b  42390  aks4d1p1p4  42393  aks4d1p1p6  42395  aks4d1p1p7  42396  aks4d1p5  42402  aks4d1p6  42403  exp11d  42648  rplog11d  42669  irrapxlem5  43135  pellfund14  43207  rmxyneg  43229  rmxyadd  43230  modabsdifz  43295  binomcxplemnotnn0  44664  oddfl  45593  xralrple3  45685  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  stoweidlem1  46312  stoweidlem14  46325  stoweidlem60  46371  wallispilem4  46379  wallispilem5  46380  wallispi  46381  wallispi2lem1  46382  stirlinglem1  46385  stirlinglem3  46387  stirlinglem4  46388  stirlinglem5  46389  stirlinglem8  46392  stirlinglem12  46396  stirlinglem15  46399  dirkertrigeqlem1  46409  dirkercncflem1  46414  dirkercncflem4  46417  fourierdlem30  46448  fourierdlem39  46457  fourierdlem47  46464  fourierdlem65  46482  fourierdlem73  46490  fourierdlem87  46504  qndenserrnbllem  46605  sge0rpcpnf  46732  hoiqssbllem2  46934  young2d  50117