Theorem rpgt0d 13064

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5110  0cc0 11101   < clt 11244  ℝ⁺crp 13017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-rp 13018

This theorem is referenced by:  rpregt0d  13067  ltmulgt11d  13096  ltmulgt12d  13097  gt0divd  13098  ge0divd  13099  lediv12ad  13120  prodge0rd  13126  expgt0  14133  nnesq  14265  bccl2  14361  sgnmulrp2  15147  01sqrexlem7  15301  sqrtgt0d  15466  iseralt  15738  fsumlt  15854  geomulcvg  15932  eirrlem  16261  sqrt2irrlem  16305  prmind2  16744  4sqlem11  17016  4sqlem12  17017  ssblex  24566  nrginvrcn  24830  mulc1cncf  25045  nmoleub2lem2  25256  itg2mulclem  25886  itggt0  25984  dvgt0  26144  ftc1lem5  26180  aaliou3lem2  26485  abelthlem8  26580  tanord  26681  tanregt0  26682  logccv  26806  cxpgt0d  26881  cxpcn3lem  26890  jensenlem2  27130  dmlogdmgm  27166  basellem1  27223  sgmnncl  27289  chpdifbndlem2  27696  pntibndlem1  27731  pntibnd  27735  pntlemc  27737  abvcxp  27757  ostth2lem1  27760  ostth2lem3  27777  ostth2  27779  xrge0iifhom  34305  omssubadd  34668  signsply0  34916  sinccvglem  36142  unblimceq0lem  37073  unbdqndv2lem2  37077  knoppndvlem14  37092  taupilem1  37943  poimirlem29  38278  heicant  38284  itggt0cn  38319  ftc1cnnc  38321  bfplem1  38451  rrncmslem  38461  aks4d1p1  42821  aks6d1c2  42875  irrapxlem4  43532  irrapxlem5  43533  imo72b2lem1  44875  dvdivbd  46617  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  stoweidlem1  46695  stoweidlem7  46701  stoweidlem11  46705  stoweidlem25  46719  stoweidlem26  46720  stoweidlem34  46728  stoweidlem49  46743  stoweidlem52  46746  stoweidlem60  46754  wallispi  46764  stirlinglem6  46773  stirlinglem11  46778  fourierdlem30  46831  qndenserrnbl  46989  ovnsubaddlem1  47264  hoiqssbllem2  47317  pimrecltpos  47402  smfmullem1  47485  smfmullem2  47486  smfmullem3  47487