Theorem rpne0d 12706

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2942  0cc0 10802  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-addrcl 10863  ax-rnegex 10873  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945  df-rp 12660

This theorem is referenced by:  rprene0d  12709  rpcnne0d  12710  iccf1o  13157  ltexp2r  13819  discr  13883  bcpasc  13963  sqrtdiv  14905  abs00  14929  absdiv  14935  o1rlimmul  15256  geomulcvg  15516  mertenslem1  15524  retanhcl  15796  tanhlt1  15797  tanhbnd  15798  sylow1lem1  19118  nrginvrcnlem  23761  nmoi2  23800  reperflem  23887  icchmeo  24010  icopnfcnv  24011  nmoleub2lem  24183  nmoleub2lem2  24185  nmoleub3  24188  pjthlem1  24506  sca2rab  24581  ovolscalem1  24582  ovolsca  24584  itg2mulclem  24816  itg2mulc  24817  c1liplem1  25065  aalioulem4  25400  aaliou3lem8  25410  itgulm  25472  dvradcnv  25485  abelthlem7  25502  abelthlem8  25503  tanrpcl  25566  tanregt0  25600  efiarg  25667  argregt0  25670  argrege0  25671  argimgt0  25672  tanarg  25679  logdivlti  25680  logno1  25696  logcnlem4  25705  divcxp  25747  cxple2  25757  cxpcn3lem  25805  cxpcn3  25806  cxpaddlelem  25809  cxpaddle  25810  logbrec  25837  asinlem3  25926  rlimcnp  26020  rlimcnp2  26021  rlimcxp  26028  cxp2limlem  26030  cxp2lim  26031  cxploglim2  26033  jensenlem2  26042  amgmlem  26044  logdiflbnd  26049  lgamgulmlem2  26084  lgamucov  26092  basellem3  26137  basellem8  26142  isppw  26168  chpeq0  26261  chteq0  26262  bposlem9  26345  chebbnd1lem2  26523  chebbnd1  26525  chtppilimlem1  26526  chebbnd2  26530  chto1lb  26531  chpchtlim  26532  chpo1ubb  26534  rplogsumlem1  26537  rplogsumlem2  26538  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  dchrisum0  26573  mulog2sumlem1  26587  vmalogdivsum2  26591  vmalogdivsum  26592  2vmadivsumlem  26593  chpdifbndlem1  26606  selberg3lem1  26610  selberg3lem2  26611  selberg3  26612  selberg4lem1  26613  selberg4  26614  selberg3r  26622  selberg4r  26623  selberg34r  26624  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntpbnd2  26640  pntibndlem2  26644  pntlemr  26655  pntlemo  26660  pnt2  26666  pnt  26667  padicabv  26683  padicabvcxp  26685  ostth2lem3  26688  ostth2lem4  26689  ostth3  26691  smcnlem  28960  pjhthlem1  29654  rpxdivcld  31110  xrmulc1cn  31782  esumdivc  31951  probmeasb  32297  signsply0  32430  divsqrtid  32474  hgt750leme  32538  circum  33532  iprodgam  33614  faclimlem1  33615  faclimlem3  33617  knoppndvlem17  34635  knoppndvlem18  34636  itg2addnclem3  35757  geomcau  35844  cntotbnd  35881  bfplem1  35907  rrncmslem  35917  rrnequiv  35920  relogbzexpd  39910  aks4d1p1p1  39999  dvrelogpow2b  40004  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p5  40016  aks4d1p6  40017  exp11d  40246  irrapxlem5  40564  pellfund14  40636  rmxyneg  40658  rmxyadd  40659  modabsdifz  40724  binomcxplemnotnn0  41863  oddfl  42705  xralrple3  42803  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem1  43432  stoweidlem14  43445  stoweidlem60  43491  wallispilem4  43499  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  stirlinglem1  43505  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem8  43512  stirlinglem12  43516  stirlinglem15  43519  dirkertrigeqlem1  43529  dirkercncflem1  43534  dirkercncflem4  43537  fourierdlem30  43568  fourierdlem39  43577  fourierdlem47  43584  fourierdlem65  43602  fourierdlem73  43610  fourierdlem87  43624  qndenserrnbllem  43725  sge0rpcpnf  43849  hoiqssbllem2  44051  young2d  46395