Theorem rpgt0d 13016

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

Syntax hints:   → wi 4   ∈ wcel 2098   class class class wbr 5138  0cc0 11106   < clt 11245  ℝ⁺crp 12971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-br 5139  df-rp 12972

This theorem is referenced by:  rpregt0d  13019  ltmulgt11d  13048  ltmulgt12d  13049  gt0divd  13050  ge0divd  13051  lediv12ad  13072  prodge0rd  13078  expgt0  14058  nnesq  14187  bccl2  14280  01sqrexlem7  15192  sqrtgt0d  15356  iseralt  15628  fsumlt  15743  geomulcvg  15819  eirrlem  16144  sqrt2irrlem  16188  prmind2  16619  4sqlem11  16887  4sqlem12  16888  ssblex  24256  nrginvrcn  24531  mulc1cncf  24747  nmoleub2lem2  24965  itg2mulclem  25598  itggt0  25695  dvgt0  25859  ftc1lem5  25897  aaliou3lem2  26197  abelthlem8  26293  tanord  26389  tanregt0  26390  logccv  26513  cxpgt0d  26588  cxpcn3lem  26598  jensenlem2  26836  dmlogdmgm  26872  basellem1  26929  sgmnncl  26995  chpdifbndlem2  27403  pntibndlem1  27438  pntibnd  27442  pntlemc  27444  abvcxp  27464  ostth2lem1  27467  ostth2lem3  27484  ostth2  27486  xrge0iifhom  33406  omssubadd  33788  sgnmulrp2  34031  signsply0  34051  sinccvglem  35146  unblimceq0lem  35872  unbdqndv2lem2  35876  knoppndvlem14  35891  taupilem1  36692  poimirlem29  37007  heicant  37013  itggt0cn  37048  ftc1cnnc  37050  bfplem1  37180  rrncmslem  37190  aks4d1p1  41434  irrapxlem4  42052  irrapxlem5  42053  imo72b2lem1  43410  dvdivbd  45124  ioodvbdlimc1lem2  45133  ioodvbdlimc2lem  45135  stoweidlem1  45202  stoweidlem7  45208  stoweidlem11  45212  stoweidlem25  45226  stoweidlem26  45227  stoweidlem34  45235  stoweidlem49  45250  stoweidlem52  45253  stoweidlem60  45261  wallispi  45271  stirlinglem6  45280  stirlinglem11  45285  fourierdlem30  45338  qndenserrnbl  45496  ovnsubaddlem1  45771  hoiqssbllem2  45824  pimrecltpos  45909  smfmullem1  45992  smfmullem2  45993  smfmullem3  45994