Theorem rpne0d 12978

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  0cc0 11046  ℝ⁺crp 12929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11103  ax-1cn 11104  ax-addrcl 11107  ax-rnegex 11117  ax-cnre 11119  ax-pre-lttri 11120  ax-pre-lttrn 11121

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11188  df-mnf 11189  df-ltxr 11191  df-rp 12930

This theorem is referenced by:  rprene0d  12981  rpcnne0d  12982  iccf1o  13435  ltexp2r  14116  discr  14183  bcpasc  14264  sqrtdiv  15208  abs00  15232  absdiv  15238  o1rlimmul  15562  geomulcvg  15819  mertenslem1  15827  retanhcl  16104  tanhlt1  16105  tanhbnd  16106  sylow1lem1  19513  nrginvrcnlem  24613  nmoi2  24652  reperflem  24741  icchmeoOLD  24873  icopnfcnv  24874  nmoleub2lem  25048  nmoleub2lem2  25050  nmoleub3  25053  pjthlem1  25371  sca2rab  25447  ovolscalem1  25448  ovolsca  25450  itg2mulclem  25681  itg2mulc  25682  c1liplem1  25935  aalioulem4  26277  aaliou3lem8  26287  itgulm  26351  dvradcnv  26364  abelthlem7  26382  abelthlem8  26383  tanrpcl  26447  tanregt0  26482  efiarg  26550  argregt0  26553  argrege0  26554  argimgt0  26555  tanarg  26562  logdivlti  26563  logno1  26579  logcnlem4  26588  divcxp  26630  cxple2  26640  cxpcn3lem  26691  cxpcn3  26692  cxpaddlelem  26695  cxpaddle  26696  logbrec  26726  asinlem3  26815  rlimcnp  26909  rlimcnp2  26910  rlimcxp  26918  cxp2limlem  26920  cxp2lim  26921  cxploglim2  26923  jensenlem2  26932  amgmlem  26934  logdiflbnd  26939  lgamgulmlem2  26974  lgamucov  26982  basellem3  27027  basellem8  27032  isppw  27058  chpeq0  27153  chteq0  27154  bposlem9  27237  chebbnd1lem2  27415  chebbnd1  27417  chtppilimlem1  27418  chebbnd2  27422  chto1lb  27423  chpchtlim  27424  chpo1ubb  27426  rplogsumlem1  27429  rplogsumlem2  27430  dchrvmasumlem1  27440  dchrvmasum2lem  27441  dchrisum0lema  27459  dchrisum0lem1b  27460  dchrisum0lem1  27461  dchrisum0lem2a  27462  dchrisum0lem2  27463  dchrisum0lem3  27464  dchrisum0  27465  mulog2sumlem1  27479  vmalogdivsum2  27483  vmalogdivsum  27484  2vmadivsumlem  27485  chpdifbndlem1  27498  selberg3lem1  27502  selberg3lem2  27503  selberg3  27504  selberg4lem1  27505  selberg4  27506  selberg3r  27514  selberg4r  27515  selberg34r  27516  pntrlog2bndlem1  27522  pntrlog2bndlem2  27523  pntrlog2bndlem3  27524  pntrlog2bndlem4  27525  pntrlog2bndlem5  27526  pntrlog2bndlem6  27528  pntpbnd2  27532  pntibndlem2  27536  pntlemr  27547  pntlemo  27552  pnt2  27558  pnt  27559  padicabv  27575  padicabvcxp  27577  ostth2lem3  27580  ostth2lem4  27581  ostth3  27583  smcnlem  30677  pjhthlem1  31371  rpxdivcld  32905  xrmulc1cn  33914  esumdivc  34067  probmeasb  34415  signsply0  34536  divsqrtid  34579  hgt750leme  34643  circum  35655  iprodgam  35723  faclimlem1  35724  faclimlem3  35726  knoppndvlem17  36510  knoppndvlem18  36511  itg2addnclem3  37661  geomcau  37747  cntotbnd  37784  bfplem1  37810  rrncmslem  37820  rrnequiv  37823  relogbzexpd  41957  aks4d1p1p1  42045  dvrelogpow2b  42050  aks4d1p1p4  42053  aks4d1p1p6  42055  aks4d1p1p7  42056  aks4d1p5  42062  aks4d1p6  42063  exp11d  42308  rplog11d  42329  irrapxlem5  42808  pellfund14  42880  rmxyneg  42903  rmxyadd  42904  modabsdifz  42969  binomcxplemnotnn0  44339  oddfl  45270  xralrple3  45364  ioodvbdlimc1lem2  45924  ioodvbdlimc2lem  45926  stoweidlem1  45993  stoweidlem14  46006  stoweidlem60  46052  wallispilem4  46060  wallispilem5  46061  wallispi  46062  wallispi2lem1  46063  stirlinglem1  46066  stirlinglem3  46068  stirlinglem4  46069  stirlinglem5  46070  stirlinglem8  46073  stirlinglem12  46077  stirlinglem15  46080  dirkertrigeqlem1  46090  dirkercncflem1  46095  dirkercncflem4  46098  fourierdlem30  46129  fourierdlem39  46138  fourierdlem47  46145  fourierdlem65  46163  fourierdlem73  46171  fourierdlem87  46185  qndenserrnbllem  46286  sge0rpcpnf  46413  hoiqssbllem2  46615  young2d  49788