Theorem rpgt0d 13080

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5143  0cc0 11155   < clt 11295  ℝ⁺crp 13034

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-rp 13035

This theorem is referenced by:  rpregt0d  13083  ltmulgt11d  13112  ltmulgt12d  13113  gt0divd  13114  ge0divd  13115  lediv12ad  13136  prodge0rd  13142  expgt0  14136  nnesq  14266  bccl2  14362  01sqrexlem7  15287  sqrtgt0d  15451  iseralt  15721  fsumlt  15836  geomulcvg  15912  eirrlem  16240  sqrt2irrlem  16284  prmind2  16722  4sqlem11  16993  4sqlem12  16994  ssblex  24438  nrginvrcn  24713  mulc1cncf  24931  nmoleub2lem2  25149  itg2mulclem  25781  itggt0  25879  dvgt0  26043  ftc1lem5  26081  aaliou3lem2  26385  abelthlem8  26483  tanord  26580  tanregt0  26581  logccv  26705  cxpgt0d  26780  cxpcn3lem  26790  jensenlem2  27031  dmlogdmgm  27067  basellem1  27124  sgmnncl  27190  chpdifbndlem2  27598  pntibndlem1  27633  pntibnd  27637  pntlemc  27639  abvcxp  27659  ostth2lem1  27662  ostth2lem3  27679  ostth2  27681  xrge0iifhom  33936  omssubadd  34302  sgnmulrp2  34546  signsply0  34566  sinccvglem  35677  unblimceq0lem  36507  unbdqndv2lem2  36511  knoppndvlem14  36526  taupilem1  37322  poimirlem29  37656  heicant  37662  itggt0cn  37697  ftc1cnnc  37699  bfplem1  37829  rrncmslem  37839  aks4d1p1  42077  aks6d1c2  42131  irrapxlem4  42836  irrapxlem5  42837  imo72b2lem1  44182  dvdivbd  45938  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem1  46016  stoweidlem7  46022  stoweidlem11  46026  stoweidlem25  46040  stoweidlem26  46041  stoweidlem34  46049  stoweidlem49  46064  stoweidlem52  46067  stoweidlem60  46075  wallispi  46085  stirlinglem6  46094  stirlinglem11  46099  fourierdlem30  46152  qndenserrnbl  46310  ovnsubaddlem1  46585  hoiqssbllem2  46638  pimrecltpos  46723  smfmullem1  46806  smfmullem2  46807  smfmullem3  46808