Theorem rpgt0d 12958

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5095  0cc0 11028   < clt 11168  ℝ⁺crp 12911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-rp 12912

This theorem is referenced by:  rpregt0d  12961  ltmulgt11d  12990  ltmulgt12d  12991  gt0divd  12992  ge0divd  12993  lediv12ad  13014  prodge0rd  13020  expgt0  14020  nnesq  14152  bccl2  14248  01sqrexlem7  15173  sqrtgt0d  15338  iseralt  15610  fsumlt  15725  geomulcvg  15801  eirrlem  16131  sqrt2irrlem  16175  prmind2  16614  4sqlem11  16885  4sqlem12  16886  ssblex  24332  nrginvrcn  24596  mulc1cncf  24814  nmoleub2lem2  25032  itg2mulclem  25663  itggt0  25761  dvgt0  25925  ftc1lem5  25963  aaliou3lem2  26267  abelthlem8  26365  tanord  26463  tanregt0  26464  logccv  26588  cxpgt0d  26663  cxpcn3lem  26673  jensenlem2  26914  dmlogdmgm  26950  basellem1  27007  sgmnncl  27073  chpdifbndlem2  27481  pntibndlem1  27516  pntibnd  27520  pntlemc  27522  abvcxp  27542  ostth2lem1  27545  ostth2lem3  27562  ostth2  27564  sgnmulrp2  32794  xrge0iifhom  33903  omssubadd  34267  signsply0  34518  sinccvglem  35644  unblimceq0lem  36479  unbdqndv2lem2  36483  knoppndvlem14  36498  taupilem1  37294  poimirlem29  37628  heicant  37634  itggt0cn  37669  ftc1cnnc  37671  bfplem1  37801  rrncmslem  37811  aks4d1p1  42049  aks6d1c2  42103  irrapxlem4  42798  irrapxlem5  42799  imo72b2lem1  44142  dvdivbd  45905  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  stoweidlem1  45983  stoweidlem7  45989  stoweidlem11  45993  stoweidlem25  46007  stoweidlem26  46008  stoweidlem34  46016  stoweidlem49  46031  stoweidlem52  46034  stoweidlem60  46042  wallispi  46052  stirlinglem6  46061  stirlinglem11  46066  fourierdlem30  46119  qndenserrnbl  46277  ovnsubaddlem1  46552  hoiqssbllem2  46605  pimrecltpos  46690  smfmullem1  46773  smfmullem2  46774  smfmullem3  46775