Theorem rpgt0d 13046

Description: A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	⊢ (𝜑 → 𝐴 ∈ ℝ+)

Assertion

Ref	Expression
rpgt0d	⊢ (𝜑 → 0 < 𝐴)

Proof of Theorem rpgt0d

Step	Hyp	Ref	Expression
1		rpred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2		rpgt0 13013	. 2 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5116  0cc0 11121   < clt 11261  ℝ⁺crp 13000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-br 5117  df-rp 13001

This theorem is referenced by:  rpregt0d  13049  ltmulgt11d  13078  ltmulgt12d  13079  gt0divd  13080  ge0divd  13081  lediv12ad  13102  prodge0rd  13108  expgt0  14102  nnesq  14233  bccl2  14329  01sqrexlem7  15254  sqrtgt0d  15418  iseralt  15688  fsumlt  15803  geomulcvg  15879  eirrlem  16207  sqrt2irrlem  16251  prmind2  16689  4sqlem11  16960  4sqlem12  16961  ssblex  24352  nrginvrcn  24616  mulc1cncf  24834  nmoleub2lem2  25052  itg2mulclem  25684  itggt0  25782  dvgt0  25946  ftc1lem5  25984  aaliou3lem2  26288  abelthlem8  26386  tanord  26483  tanregt0  26484  logccv  26608  cxpgt0d  26683  cxpcn3lem  26693  jensenlem2  26934  dmlogdmgm  26970  basellem1  27027  sgmnncl  27093  chpdifbndlem2  27501  pntibndlem1  27536  pntibnd  27540  pntlemc  27542  abvcxp  27562  ostth2lem1  27565  ostth2lem3  27582  ostth2  27584  xrge0iifhom  33876  omssubadd  34240  sgnmulrp2  34484  signsply0  34504  sinccvglem  35615  unblimceq0lem  36445  unbdqndv2lem2  36449  knoppndvlem14  36464  taupilem1  37260  poimirlem29  37594  heicant  37600  itggt0cn  37635  ftc1cnnc  37637  bfplem1  37767  rrncmslem  37777  aks4d1p1  42011  aks6d1c2  42065  irrapxlem4  42773  irrapxlem5  42774  imo72b2lem1  44118  dvdivbd  45882  ioodvbdlimc1lem2  45891  ioodvbdlimc2lem  45893  stoweidlem1  45960  stoweidlem7  45966  stoweidlem11  45970  stoweidlem25  45984  stoweidlem26  45985  stoweidlem34  45993  stoweidlem49  46008  stoweidlem52  46011  stoweidlem60  46019  wallispi  46029  stirlinglem6  46038  stirlinglem11  46043  fourierdlem30  46096  qndenserrnbl  46254  ovnsubaddlem1  46529  hoiqssbllem2  46582  pimrecltpos  46667  smfmullem1  46750  smfmullem2  46751  smfmullem3  46752