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  32948  omssubadd  33330  sgnmulrp2  33573  signsply0  33593  sinccvglem  34688  unblimceq0lem  35430  unbdqndv2lem2  35434  knoppndvlem14  35449  taupilem1  36250  poimirlem29  36565  heicant  36571  itggt0cn  36606  ftc1cnnc  36608  bfplem1  36738  rrncmslem  36748  aks4d1p1  40989  irrapxlem4  41611  irrapxlem5  41612  imo72b2lem1  42969  dvdivbd  44687  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  stoweidlem1  44765  stoweidlem7  44771  stoweidlem11  44775  stoweidlem25  44789  stoweidlem26  44790  stoweidlem34  44798  stoweidlem49  44813  stoweidlem52  44816  stoweidlem60  44824  wallispi  44834  stirlinglem6  44843  stirlinglem11  44848  fourierdlem30  44901  qndenserrnbl  45059  ovnsubaddlem1  45334  hoiqssbllem2  45387  pimrecltpos  45472  smfmullem1  45555  smfmullem2  45556  smfmullem3  45557