Theorem rpgt0d 12964

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  0cc0 11038   < clt 11178  ℝ⁺crp 12917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-rp 12918

This theorem is referenced by:  rpregt0d  12967  ltmulgt11d  12996  ltmulgt12d  12997  gt0divd  12998  ge0divd  12999  lediv12ad  13020  prodge0rd  13026  expgt0  14030  nnesq  14162  bccl2  14258  01sqrexlem7  15183  sqrtgt0d  15348  iseralt  15620  fsumlt  15735  geomulcvg  15811  eirrlem  16141  sqrt2irrlem  16185  prmind2  16624  4sqlem11  16895  4sqlem12  16896  ssblex  24384  nrginvrcn  24648  mulc1cncf  24866  nmoleub2lem2  25084  itg2mulclem  25715  itggt0  25813  dvgt0  25977  ftc1lem5  26015  aaliou3lem2  26319  abelthlem8  26417  tanord  26515  tanregt0  26516  logccv  26640  cxpgt0d  26715  cxpcn3lem  26725  jensenlem2  26966  dmlogdmgm  27002  basellem1  27059  sgmnncl  27125  chpdifbndlem2  27533  pntibndlem1  27568  pntibnd  27572  pntlemc  27574  abvcxp  27594  ostth2lem1  27597  ostth2lem3  27614  ostth2  27616  sgnmulrp2  32927  xrge0iifhom  34114  omssubadd  34477  signsply0  34728  sinccvglem  35885  unblimceq0lem  36725  unbdqndv2lem2  36729  knoppndvlem14  36744  taupilem1  37570  poimirlem29  37894  heicant  37900  itggt0cn  37935  ftc1cnnc  37937  bfplem1  38067  rrncmslem  38077  aks4d1p1  42440  aks6d1c2  42494  irrapxlem4  43176  irrapxlem5  43177  imo72b2lem1  44519  dvdivbd  46275  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  stoweidlem1  46353  stoweidlem7  46359  stoweidlem11  46363  stoweidlem25  46377  stoweidlem26  46378  stoweidlem34  46386  stoweidlem49  46401  stoweidlem52  46404  stoweidlem60  46412  wallispi  46422  stirlinglem6  46431  stirlinglem11  46436  fourierdlem30  46489  qndenserrnbl  46647  ovnsubaddlem1  46922  hoiqssbllem2  46975  pimrecltpos  47060  smfmullem1  47143  smfmullem2  47144  smfmullem3  47145