Theorem rpgt0d 13093

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5107  0cc0 11128   < clt 11271  ℝ⁺crp 13046

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-rp 13047

This theorem is used by:  rpregt0d  13096  ltmulgt11d  13125  ltmulgt12d  13126  gt0divd  13127  ge0divd  13128  lediv12ad  13149  prodge0rd  13155  expgt0  14163  nnesq  14295  bccl2  14391  sgnmulrp2  15185  01sqrexlem7  15339  sqrtgt0d  15504  iseralt  15776  fsumlt  15891  geomulcvg  15969  eirrlem  16298  sqrt2irrlem  16342  prmind2  16781  4sqlem11  17053  4sqlem12  17054  ssblex  24660  nrginvrcn  24924  mulc1cncf  25139  nmoleub2lem2  25350  itg2mulclem  25980  itggt0  26078  dvgt0  26238  ftc1lem5  26274  aaliou3lem2  26586  abelthlem8  26682  tanord  26783  tanregt0  26784  logccv  26908  cxpgt0d  26983  cxpcn3lem  26992  jensenlem2  27232  dmlogdmgm  27268  basellem1  27325  sgmnncl  27391  chpdifbndlem2  27798  pntibndlem1  27833  pntibnd  27837  pntlemc  27839  abvcxp  27859  ostth2lem1  27862  ostth2lem3  27879  ostth2  27881  xrge0iifhom  34455  omssubadd  34819  signsply0  35067  sinccvglem  36259  unblimceq0lem  37211  unbdqndv2lem2  37215  knoppndvlem14  37230  taupilem1  38081  poimirlem29  38406  heicant  38412  itggt0cn  38447  ftc1cnnc  38449  bfplem1  38580  rrncmslem  38590  aks4d1p1  42950  aks6d1c2  43004  irrapxlem4  43674  irrapxlem5  43675  imo72b2lem1  45017  dvdivbd  46759  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  stoweidlem1  46837  stoweidlem7  46843  stoweidlem11  46847  stoweidlem25  46861  stoweidlem26  46862  stoweidlem34  46870  stoweidlem49  46885  stoweidlem52  46888  stoweidlem60  46896  wallispi  46906  stirlinglem6  46915  stirlinglem11  46920  fourierdlem30  46973  qndenserrnbl  47131  ovnsubaddlem1  47406  hoiqssbllem2  47459  pimrecltpos  47544  smfmullem1  47627  smfmullem2  47628  smfmullem3  47629