Theorem rpgt0d 12934

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5091  0cc0 11003   < clt 11143  ℝ⁺crp 12887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-rp 12888

This theorem is referenced by:  rpregt0d  12937  ltmulgt11d  12966  ltmulgt12d  12967  gt0divd  12968  ge0divd  12969  lediv12ad  12990  prodge0rd  12996  expgt0  13999  nnesq  14131  bccl2  14227  01sqrexlem7  15152  sqrtgt0d  15317  iseralt  15589  fsumlt  15704  geomulcvg  15780  eirrlem  16110  sqrt2irrlem  16154  prmind2  16593  4sqlem11  16864  4sqlem12  16865  ssblex  24341  nrginvrcn  24605  mulc1cncf  24823  nmoleub2lem2  25041  itg2mulclem  25672  itggt0  25770  dvgt0  25934  ftc1lem5  25972  aaliou3lem2  26276  abelthlem8  26374  tanord  26472  tanregt0  26473  logccv  26597  cxpgt0d  26672  cxpcn3lem  26682  jensenlem2  26923  dmlogdmgm  26959  basellem1  27016  sgmnncl  27082  chpdifbndlem2  27490  pntibndlem1  27525  pntibnd  27529  pntlemc  27531  abvcxp  27551  ostth2lem1  27554  ostth2lem3  27571  ostth2  27573  sgnmulrp2  32814  xrge0iifhom  33945  omssubadd  34308  signsply0  34559  sinccvglem  35704  unblimceq0lem  36539  unbdqndv2lem2  36543  knoppndvlem14  36558  taupilem1  37354  poimirlem29  37688  heicant  37694  itggt0cn  37729  ftc1cnnc  37731  bfplem1  37861  rrncmslem  37871  aks4d1p1  42108  aks6d1c2  42162  irrapxlem4  42857  irrapxlem5  42858  imo72b2lem1  44201  dvdivbd  45960  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  stoweidlem1  46038  stoweidlem7  46044  stoweidlem11  46048  stoweidlem25  46062  stoweidlem26  46063  stoweidlem34  46071  stoweidlem49  46086  stoweidlem52  46089  stoweidlem60  46097  wallispi  46107  stirlinglem6  46116  stirlinglem11  46121  fourierdlem30  46174  qndenserrnbl  46332  ovnsubaddlem1  46607  hoiqssbllem2  46660  pimrecltpos  46745  smfmullem1  46828  smfmullem2  46829  smfmullem3  46830