Theorem rpgt0d 12969

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5110  0cc0 11060   < clt 11198  ℝ⁺crp 12924

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-rp 12925

This theorem is referenced by:  rpregt0d  12972  ltmulgt11d  13001  ltmulgt12d  13002  gt0divd  13003  ge0divd  13004  lediv12ad  13025  prodge0rd  13031  expgt0  14011  nnesq  14140  bccl2  14233  01sqrexlem7  15145  sqrtgt0d  15309  iseralt  15581  fsumlt  15696  geomulcvg  15772  eirrlem  16097  sqrt2irrlem  16141  prmind2  16572  4sqlem11  16838  4sqlem12  16839  ssblex  23818  nrginvrcn  24093  mulc1cncf  24305  nmoleub2lem2  24516  itg2mulclem  25148  itggt0  25245  dvgt0  25405  ftc1lem5  25441  aaliou3lem2  25740  abelthlem8  25835  tanord  25931  tanregt0  25932  logccv  26055  cxpcn3lem  26137  jensenlem2  26374  dmlogdmgm  26410  basellem1  26467  sgmnncl  26533  chpdifbndlem2  26939  pntibndlem1  26974  pntibnd  26978  pntlemc  26980  abvcxp  27000  ostth2lem1  27003  ostth2lem3  27020  ostth2  27022  xrge0iifhom  32607  omssubadd  32989  sgnmulrp2  33232  signsply0  33252  sinccvglem  34347  unblimceq0lem  35045  unbdqndv2lem2  35049  knoppndvlem14  35064  taupilem1  35865  poimirlem29  36180  heicant  36186  itggt0cn  36221  ftc1cnnc  36223  bfplem1  36354  rrncmslem  36364  aks4d1p1  40606  cxpgt0d  40888  irrapxlem4  41206  irrapxlem5  41207  imo72b2lem1  42564  dvdivbd  44284  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  stoweidlem1  44362  stoweidlem7  44368  stoweidlem11  44372  stoweidlem25  44386  stoweidlem26  44387  stoweidlem34  44395  stoweidlem49  44410  stoweidlem52  44413  stoweidlem60  44421  wallispi  44431  stirlinglem6  44440  stirlinglem11  44445  fourierdlem30  44498  qndenserrnbl  44656  ovnsubaddlem1  44931  hoiqssbllem2  44984  pimrecltpos  45069  smfmullem1  45152  smfmullem2  45153  smfmullem3  45154