Theorem rpgt0d 11751

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

Syntax hints:   → wi 4   ∈ wcel 1977   class class class wbr 4583  0cc0 9815   < clt 9953  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-rp 11709

This theorem is referenced by:  rpregt0d  11754  ltmulgt11d  11783  ltmulgt12d  11784  gt0divd  11785  ge0divd  11786  lediv12ad  11807  expgt0  12755  nnesq  12850  bccl2  12972  sqrlem7  13837  sqrtgt0d  13999  iseralt  14263  fsumlt  14373  geomulcvg  14446  eirrlem  14771  sqr2irrlem  14816  prmind2  15236  4sqlem11  15497  4sqlem12  15498  ssblex  22043  nrginvrcn  22306  mulc1cncf  22516  nmoleub2lem2  22724  itg2mulclem  23319  itggt0  23414  dvgt0  23571  ftc1lem5  23607  aaliou3lem2  23902  abelthlem8  23997  tanord  24088  tanregt0  24089  logccv  24209  cxpcn3lem  24288  jensenlem2  24514  dmlogdmgm  24550  basellem1  24607  sgmnncl  24673  chpdifbndlem2  25043  pntibndlem1  25078  pntibnd  25082  pntlemc  25084  abvcxp  25104  ostth2lem1  25107  ostth2lem3  25124  ostth2  25126  xrge0iifhom  29311  omssubadd  29689  sgnmulrp2  29932  signsply0  29954  sinccvglem  30820  unblimceq0lem  31667  unbdqndv2lem2  31671  knoppndvlem14  31686  taupilem1  32344  poimirlem29  32608  heicant  32614  itggt0cn  32652  ftc1cnnc  32654  bfplem1  32791  rrncmslem  32801  irrapxlem4  36407  irrapxlem5  36408  imo72b2lem1  37493  dvdivbd  38813  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem1  38894  stoweidlem7  38900  stoweidlem11  38904  stoweidlem25  38918  stoweidlem26  38919  stoweidlem34  38927  stoweidlem49  38942  stoweidlem52  38945  stoweidlem60  38953  wallispi  38963  stirlinglem6  38972  stirlinglem11  38977  fourierdlem30  39030  qndenserrnbl  39191  ovnsubaddlem1  39460  hoiqssbllem2  39513  pimrecltpos  39596  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678