Theorem rpne0d 12490

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2951  0cc0 10588  ℝ⁺crp 12443

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-resscn 10645  ax-1cn 10646  ax-addrcl 10649  ax-rnegex 10659  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-po 5447  df-so 5448  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-er 8305  df-en 8541  df-dom 8542  df-sdom 8543  df-pnf 10728  df-mnf 10729  df-ltxr 10731  df-rp 12444

This theorem is referenced by:  rprene0d  12493  rpcnne0d  12494  iccf1o  12941  ltexp2r  13600  discr  13664  bcpasc  13744  sqrtdiv  14686  abs00  14710  absdiv  14716  o1rlimmul  15036  geomulcvg  15293  mertenslem1  15301  retanhcl  15573  tanhlt1  15574  tanhbnd  15575  sylow1lem1  18803  nrginvrcnlem  23406  nmoi2  23445  reperflem  23532  icchmeo  23655  icopnfcnv  23656  nmoleub2lem  23828  nmoleub2lem2  23830  nmoleub3  23833  pjthlem1  24150  sca2rab  24225  ovolscalem1  24226  ovolsca  24228  itg2mulclem  24459  itg2mulc  24460  c1liplem1  24708  aalioulem4  25043  aaliou3lem8  25053  itgulm  25115  dvradcnv  25128  abelthlem7  25145  abelthlem8  25146  tanrpcl  25209  tanregt0  25243  efiarg  25310  argregt0  25313  argrege0  25314  argimgt0  25315  tanarg  25322  logdivlti  25323  logno1  25339  logcnlem4  25348  divcxp  25390  cxple2  25400  cxpcn3lem  25448  cxpcn3  25449  cxpaddlelem  25452  cxpaddle  25453  logbrec  25480  asinlem3  25569  rlimcnp  25663  rlimcnp2  25664  rlimcxp  25671  cxp2limlem  25673  cxp2lim  25674  cxploglim2  25676  jensenlem2  25685  amgmlem  25687  logdiflbnd  25692  lgamgulmlem2  25727  lgamucov  25735  basellem3  25780  basellem8  25785  isppw  25811  chpeq0  25904  chteq0  25905  bposlem9  25988  chebbnd1lem2  26166  chebbnd1  26168  chtppilimlem1  26169  chebbnd2  26173  chto1lb  26174  chpchtlim  26175  chpo1ubb  26177  rplogsumlem1  26180  rplogsumlem2  26181  dchrvmasumlem1  26191  dchrvmasum2lem  26192  dchrisum0lema  26210  dchrisum0lem1b  26211  dchrisum0lem1  26212  dchrisum0lem2a  26213  dchrisum0lem2  26214  dchrisum0lem3  26215  dchrisum0  26216  mulog2sumlem1  26230  vmalogdivsum2  26234  vmalogdivsum  26235  2vmadivsumlem  26236  chpdifbndlem1  26249  selberg3lem1  26253  selberg3lem2  26254  selberg3  26255  selberg4lem1  26256  selberg4  26257  selberg3r  26265  selberg4r  26266  selberg34r  26267  pntrlog2bndlem1  26273  pntrlog2bndlem2  26274  pntrlog2bndlem3  26275  pntrlog2bndlem4  26276  pntrlog2bndlem5  26277  pntrlog2bndlem6  26279  pntpbnd2  26283  pntibndlem2  26287  pntlemr  26298  pntlemo  26303  pnt2  26309  pnt  26310  padicabv  26326  padicabvcxp  26328  ostth2lem3  26331  ostth2lem4  26332  ostth3  26334  smcnlem  28592  pjhthlem1  29286  rpxdivcld  30744  xrmulc1cn  31413  esumdivc  31582  probmeasb  31928  signsply0  32061  divsqrtid  32105  hgt750leme  32169  circum  33160  iprodgam  33235  faclimlem1  33236  faclimlem3  33238  knoppndvlem17  34291  knoppndvlem18  34292  itg2addnclem3  35424  geomcau  35511  cntotbnd  35548  bfplem1  35574  rrncmslem  35584  rrnequiv  35587  relogbzexpd  39575  aks4d1p1p1  39663  dvrelogpow2b  39668  aks4d1p1p4  39671  aks4d1p1p6  39673  aks4d1p1p7  39674  cxpgt0d  39859  exp11d  39872  irrapxlem5  40175  pellfund14  40247  rmxyneg  40269  rmxyadd  40270  modabsdifz  40335  binomcxplemnotnn0  41468  oddfl  42311  xralrple3  42409  ioodvbdlimc1lem2  42975  ioodvbdlimc2lem  42977  stoweidlem1  43044  stoweidlem14  43057  stoweidlem60  43103  wallispilem4  43111  wallispilem5  43112  wallispi  43113  wallispi2lem1  43114  stirlinglem1  43117  stirlinglem3  43119  stirlinglem4  43120  stirlinglem5  43121  stirlinglem8  43124  stirlinglem12  43128  stirlinglem15  43131  dirkertrigeqlem1  43141  dirkercncflem1  43146  dirkercncflem4  43149  fourierdlem30  43180  fourierdlem39  43189  fourierdlem47  43196  fourierdlem65  43214  fourierdlem73  43222  fourierdlem87  43236  qndenserrnbllem  43337  sge0rpcpnf  43461  hoiqssbllem2  43663  young2d  45818