Theorem rpgt0d 13019

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5149  0cc0 11110   < clt 11248  ℝ⁺crp 12974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-rp 12975

This theorem is referenced by:  rpregt0d  13022  ltmulgt11d  13051  ltmulgt12d  13052  gt0divd  13053  ge0divd  13054  lediv12ad  13075  prodge0rd  13081  expgt0  14061  nnesq  14190  bccl2  14283  01sqrexlem7  15195  sqrtgt0d  15359  iseralt  15631  fsumlt  15746  geomulcvg  15822  eirrlem  16147  sqrt2irrlem  16191  prmind2  16622  4sqlem11  16888  4sqlem12  16889  ssblex  23934  nrginvrcn  24209  mulc1cncf  24421  nmoleub2lem2  24632  itg2mulclem  25264  itggt0  25361  dvgt0  25521  ftc1lem5  25557  aaliou3lem2  25856  abelthlem8  25951  tanord  26047  tanregt0  26048  logccv  26171  cxpgt0d  26246  cxpcn3lem  26255  jensenlem2  26492  dmlogdmgm  26528  basellem1  26585  sgmnncl  26651  chpdifbndlem2  27057  pntibndlem1  27092  pntibnd  27096  pntlemc  27098  abvcxp  27118  ostth2lem1  27121  ostth2lem3  27138  ostth2  27140  xrge0iifhom  32917  omssubadd  33299  sgnmulrp2  33542  signsply0  33562  sinccvglem  34657  unblimceq0lem  35382  unbdqndv2lem2  35386  knoppndvlem14  35401  taupilem1  36202  poimirlem29  36517  heicant  36523  itggt0cn  36558  ftc1cnnc  36560  bfplem1  36690  rrncmslem  36700  aks4d1p1  40941  irrapxlem4  41563  irrapxlem5  41564  imo72b2lem1  42921  dvdivbd  44639  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  stoweidlem1  44717  stoweidlem7  44723  stoweidlem11  44727  stoweidlem25  44741  stoweidlem26  44742  stoweidlem34  44750  stoweidlem49  44765  stoweidlem52  44768  stoweidlem60  44776  wallispi  44786  stirlinglem6  44795  stirlinglem11  44800  fourierdlem30  44853  qndenserrnbl  45011  ovnsubaddlem1  45286  hoiqssbllem2  45339  pimrecltpos  45424  smfmullem1  45507  smfmullem2  45508  smfmullem3  45509