Theorem rpgt0d 12991

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  0cc0 11040   < clt 11181  ℝ⁺crp 12944

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-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-rp 12945

This theorem is referenced by:  rpregt0d  12994  ltmulgt11d  13023  ltmulgt12d  13024  gt0divd  13025  ge0divd  13026  lediv12ad  13047  prodge0rd  13053  expgt0  14059  nnesq  14191  bccl2  14287  01sqrexlem7  15212  sqrtgt0d  15377  iseralt  15649  fsumlt  15765  geomulcvg  15843  eirrlem  16173  sqrt2irrlem  16217  prmind2  16656  4sqlem11  16928  4sqlem12  16929  ssblex  24395  nrginvrcn  24659  mulc1cncf  24874  nmoleub2lem2  25085  itg2mulclem  25715  itggt0  25813  dvgt0  25973  ftc1lem5  26009  aaliou3lem2  26311  abelthlem8  26406  tanord  26504  tanregt0  26505  logccv  26629  cxpgt0d  26704  cxpcn3lem  26713  jensenlem2  26953  dmlogdmgm  26989  basellem1  27046  sgmnncl  27112  chpdifbndlem2  27519  pntibndlem1  27554  pntibnd  27558  pntlemc  27560  abvcxp  27580  ostth2lem1  27583  ostth2lem3  27600  ostth2  27602  sgnmulrp2  32911  xrge0iifhom  34083  omssubadd  34446  signsply0  34697  sinccvglem  35856  unblimceq0lem  36768  unbdqndv2lem2  36772  knoppndvlem14  36787  taupilem1  37637  poimirlem29  37972  heicant  37978  itggt0cn  38013  ftc1cnnc  38015  bfplem1  38145  rrncmslem  38155  aks4d1p1  42517  aks6d1c2  42571  irrapxlem4  43255  irrapxlem5  43256  imo72b2lem1  44598  dvdivbd  46353  ioodvbdlimc1lem2  46362  ioodvbdlimc2lem  46364  stoweidlem1  46431  stoweidlem7  46437  stoweidlem11  46441  stoweidlem25  46455  stoweidlem26  46456  stoweidlem34  46464  stoweidlem49  46479  stoweidlem52  46482  stoweidlem60  46490  wallispi  46500  stirlinglem6  46509  stirlinglem11  46514  fourierdlem30  46567  qndenserrnbl  46725  ovnsubaddlem1  47000  hoiqssbllem2  47053  pimrecltpos  47138  smfmullem1  47221  smfmullem2  47222  smfmullem3  47223