Theorem rpgt0d 12980

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  0cc0 11029   < clt 11170  ℝ⁺crp 12933

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-rp 12934

This theorem is referenced by:  rpregt0d  12983  ltmulgt11d  13012  ltmulgt12d  13013  gt0divd  13014  ge0divd  13015  lediv12ad  13036  prodge0rd  13042  expgt0  14048  nnesq  14180  bccl2  14276  01sqrexlem7  15201  sqrtgt0d  15366  iseralt  15638  fsumlt  15754  geomulcvg  15832  eirrlem  16162  sqrt2irrlem  16206  prmind2  16645  4sqlem11  16917  4sqlem12  16918  ssblex  24403  nrginvrcn  24667  mulc1cncf  24882  nmoleub2lem2  25093  itg2mulclem  25723  itggt0  25821  dvgt0  25981  ftc1lem5  26017  aaliou3lem2  26320  abelthlem8  26417  tanord  26515  tanregt0  26516  logccv  26640  cxpgt0d  26715  cxpcn3lem  26724  jensenlem2  26965  dmlogdmgm  27001  basellem1  27058  sgmnncl  27124  chpdifbndlem2  27531  pntibndlem1  27566  pntibnd  27570  pntlemc  27572  abvcxp  27592  ostth2lem1  27595  ostth2lem3  27612  ostth2  27614  sgnmulrp2  32924  xrge0iifhom  34097  omssubadd  34460  signsply0  34711  sinccvglem  35870  unblimceq0lem  36782  unbdqndv2lem2  36786  knoppndvlem14  36801  taupilem1  37651  poimirlem29  37984  heicant  37990  itggt0cn  38025  ftc1cnnc  38027  bfplem1  38157  rrncmslem  38167  aks4d1p1  42529  aks6d1c2  42583  irrapxlem4  43271  irrapxlem5  43272  imo72b2lem1  44614  dvdivbd  46369  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  stoweidlem1  46447  stoweidlem7  46453  stoweidlem11  46457  stoweidlem25  46471  stoweidlem26  46472  stoweidlem34  46480  stoweidlem49  46495  stoweidlem52  46498  stoweidlem60  46506  wallispi  46516  stirlinglem6  46525  stirlinglem11  46530  fourierdlem30  46583  qndenserrnbl  46741  ovnsubaddlem1  47016  hoiqssbllem2  47069  pimrecltpos  47154  smfmullem1  47237  smfmullem2  47238  smfmullem3  47239