Theorem rpgt0d 13054

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

Syntax hints:   → wi 4   ∈ wcel 2145   class class class wbr 5105  0cc0 11088   < clt 11231  ℝ⁺crp 13007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-rp 13008

This theorem is referenced by:  rpregt0d  13057  ltmulgt11d  13086  ltmulgt12d  13087  gt0divd  13088  ge0divd  13089  lediv12ad  13110  prodge0rd  13116  expgt0  14122  nnesq  14254  bccl2  14350  sgnmulrp2  15135  01sqrexlem7  15289  sqrtgt0d  15454  iseralt  15726  fsumlt  15842  geomulcvg  15920  eirrlem  16250  sqrt2irrlem  16294  prmind2  16733  4sqlem11  17005  4sqlem12  17006  ssblex  24546  nrginvrcn  24810  mulc1cncf  25025  nmoleub2lem2  25236  itg2mulclem  25866  itggt0  25964  dvgt0  26124  ftc1lem5  26160  aaliou3lem2  26465  abelthlem8  26560  tanord  26661  tanregt0  26662  logccv  26786  cxpgt0d  26861  cxpcn3lem  26870  jensenlem2  27110  dmlogdmgm  27146  basellem1  27203  sgmnncl  27269  chpdifbndlem2  27676  pntibndlem1  27711  pntibnd  27715  pntlemc  27717  abvcxp  27737  ostth2lem1  27740  ostth2lem3  27757  ostth2  27759  xrge0iifhom  34244  omssubadd  34607  signsply0  34855  sinccvglem  36035  unblimceq0lem  36957  unbdqndv2lem2  36961  knoppndvlem14  36976  taupilem1  37825  poimirlem29  38160  heicant  38166  itggt0cn  38201  ftc1cnnc  38203  bfplem1  38333  rrncmslem  38343  aks4d1p1  42705  aks6d1c2  42759  irrapxlem4  43414  irrapxlem5  43415  imo72b2lem1  44757  dvdivbd  46495  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  stoweidlem1  46573  stoweidlem7  46579  stoweidlem11  46583  stoweidlem25  46597  stoweidlem26  46598  stoweidlem34  46606  stoweidlem49  46621  stoweidlem52  46624  stoweidlem60  46632  wallispi  46642  stirlinglem6  46651  stirlinglem11  46656  fourierdlem30  46709  qndenserrnbl  46867  ovnsubaddlem1  47142  hoiqssbllem2  47195  pimrecltpos  47280  smfmullem1  47363  smfmullem2  47364  smfmullem3  47365