Theorem rpgt0d 13078

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5148  0cc0 11153   < clt 11293  ℝ⁺crp 13032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-rp 13033

This theorem is referenced by:  rpregt0d  13081  ltmulgt11d  13110  ltmulgt12d  13111  gt0divd  13112  ge0divd  13113  lediv12ad  13134  prodge0rd  13140  expgt0  14133  nnesq  14263  bccl2  14359  01sqrexlem7  15284  sqrtgt0d  15448  iseralt  15718  fsumlt  15833  geomulcvg  15909  eirrlem  16237  sqrt2irrlem  16281  prmind2  16719  4sqlem11  16989  4sqlem12  16990  ssblex  24454  nrginvrcn  24729  mulc1cncf  24945  nmoleub2lem2  25163  itg2mulclem  25796  itggt0  25894  dvgt0  26058  ftc1lem5  26096  aaliou3lem2  26400  abelthlem8  26498  tanord  26595  tanregt0  26596  logccv  26720  cxpgt0d  26795  cxpcn3lem  26805  jensenlem2  27046  dmlogdmgm  27082  basellem1  27139  sgmnncl  27205  chpdifbndlem2  27613  pntibndlem1  27648  pntibnd  27652  pntlemc  27654  abvcxp  27674  ostth2lem1  27677  ostth2lem3  27694  ostth2  27696  xrge0iifhom  33898  omssubadd  34282  sgnmulrp2  34525  signsply0  34545  sinccvglem  35657  unblimceq0lem  36489  unbdqndv2lem2  36493  knoppndvlem14  36508  taupilem1  37304  poimirlem29  37636  heicant  37642  itggt0cn  37677  ftc1cnnc  37679  bfplem1  37809  rrncmslem  37819  aks4d1p1  42058  aks6d1c2  42112  irrapxlem4  42813  irrapxlem5  42814  imo72b2lem1  44159  dvdivbd  45879  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  stoweidlem1  45957  stoweidlem7  45963  stoweidlem11  45967  stoweidlem25  45981  stoweidlem26  45982  stoweidlem34  45990  stoweidlem49  46005  stoweidlem52  46008  stoweidlem60  46016  wallispi  46026  stirlinglem6  46035  stirlinglem11  46040  fourierdlem30  46093  qndenserrnbl  46251  ovnsubaddlem1  46526  hoiqssbllem2  46579  pimrecltpos  46664  smfmullem1  46747  smfmullem2  46748  smfmullem3  46749