Theorem rpgt0d 12987

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

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5079  0cc0 11036   < clt 11177  ℝ⁺crp 12940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-rp 12941

This theorem is referenced by:  rpregt0d  12990  ltmulgt11d  13019  ltmulgt12d  13020  gt0divd  13021  ge0divd  13022  lediv12ad  13043  prodge0rd  13049  expgt0  14055  nnesq  14187  bccl2  14283  01sqrexlem7  15208  sqrtgt0d  15373  iseralt  15645  fsumlt  15761  geomulcvg  15839  eirrlem  16169  sqrt2irrlem  16213  prmind2  16652  4sqlem11  16924  4sqlem12  16925  ssblex  24418  nrginvrcn  24682  mulc1cncf  24897  nmoleub2lem2  25108  itg2mulclem  25738  itggt0  25836  dvgt0  25996  ftc1lem5  26032  aaliou3lem2  26334  abelthlem8  26429  tanord  26527  tanregt0  26528  logccv  26652  cxpgt0d  26727  cxpcn3lem  26736  jensenlem2  26976  dmlogdmgm  27012  basellem1  27069  sgmnncl  27135  chpdifbndlem2  27542  pntibndlem1  27577  pntibnd  27581  pntlemc  27583  abvcxp  27603  ostth2lem1  27606  ostth2lem3  27623  ostth2  27625  sgnmulrp2  32935  xrge0iifhom  34128  omssubadd  34491  signsply0  34742  sinccvglem  35907  unblimceq0lem  36819  unbdqndv2lem2  36823  knoppndvlem14  36838  taupilem1  37688  poimirlem29  38023  heicant  38029  itggt0cn  38064  ftc1cnnc  38066  bfplem1  38196  rrncmslem  38206  aks4d1p1  42568  aks6d1c2  42622  irrapxlem4  43277  irrapxlem5  43278  imo72b2lem1  44620  dvdivbd  46373  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  stoweidlem1  46451  stoweidlem7  46457  stoweidlem11  46461  stoweidlem25  46475  stoweidlem26  46476  stoweidlem34  46484  stoweidlem49  46499  stoweidlem52  46502  stoweidlem60  46510  wallispi  46520  stirlinglem6  46529  stirlinglem11  46534  fourierdlem30  46587  qndenserrnbl  46745  ovnsubaddlem1  47020  hoiqssbllem2  47073  pimrecltpos  47158  smfmullem1  47241  smfmullem2  47242  smfmullem3  47243