Theorem rpgt0d 12775

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5074  0cc0 10871   < clt 11009  ℝ⁺crp 12730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-rp 12731

This theorem is referenced by:  rpregt0d  12778  ltmulgt11d  12807  ltmulgt12d  12808  gt0divd  12809  ge0divd  12810  lediv12ad  12831  prodge0rd  12837  expgt0  13816  nnesq  13942  bccl2  14037  sqrlem7  14960  sqrtgt0d  15124  iseralt  15396  fsumlt  15512  geomulcvg  15588  eirrlem  15913  sqrt2irrlem  15957  prmind2  16390  4sqlem11  16656  4sqlem12  16657  ssblex  23581  nrginvrcn  23856  mulc1cncf  24068  nmoleub2lem2  24279  itg2mulclem  24911  itggt0  25008  dvgt0  25168  ftc1lem5  25204  aaliou3lem2  25503  abelthlem8  25598  tanord  25694  tanregt0  25695  logccv  25818  cxpcn3lem  25900  jensenlem2  26137  dmlogdmgm  26173  basellem1  26230  sgmnncl  26296  chpdifbndlem2  26702  pntibndlem1  26737  pntibnd  26741  pntlemc  26743  abvcxp  26763  ostth2lem1  26766  ostth2lem3  26783  ostth2  26785  xrge0iifhom  31887  omssubadd  32267  sgnmulrp2  32510  signsply0  32530  sinccvglem  33630  unblimceq0lem  34686  unbdqndv2lem2  34690  knoppndvlem14  34705  taupilem1  35492  poimirlem29  35806  heicant  35812  itggt0cn  35847  ftc1cnnc  35849  bfplem1  35980  rrncmslem  35990  aks4d1p1  40084  cxpgt0d  40344  irrapxlem4  40647  irrapxlem5  40648  imo72b2lem1  41780  dvdivbd  43464  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  stoweidlem1  43542  stoweidlem7  43548  stoweidlem11  43552  stoweidlem25  43566  stoweidlem26  43567  stoweidlem34  43575  stoweidlem49  43590  stoweidlem52  43593  stoweidlem60  43601  wallispi  43611  stirlinglem6  43620  stirlinglem11  43625  fourierdlem30  43678  qndenserrnbl  43836  ovnsubaddlem1  44108  hoiqssbllem2  44161  pimrecltpos  44245  smfmullem1  44325  smfmullem2  44326  smfmullem3  44327