Theorem rpgt0d 12989

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5085  0cc0 11038   < clt 11179  ℝ⁺crp 12942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-rp 12943

This theorem is referenced by:  rpregt0d  12992  ltmulgt11d  13021  ltmulgt12d  13022  gt0divd  13023  ge0divd  13024  lediv12ad  13045  prodge0rd  13051  expgt0  14057  nnesq  14189  bccl2  14285  01sqrexlem7  15210  sqrtgt0d  15375  iseralt  15647  fsumlt  15763  geomulcvg  15841  eirrlem  16171  sqrt2irrlem  16215  prmind2  16654  4sqlem11  16926  4sqlem12  16927  ssblex  24393  nrginvrcn  24657  mulc1cncf  24872  nmoleub2lem2  25083  itg2mulclem  25713  itggt0  25811  dvgt0  25971  ftc1lem5  26007  aaliou3lem2  26309  abelthlem8  26404  tanord  26502  tanregt0  26503  logccv  26627  cxpgt0d  26702  cxpcn3lem  26711  jensenlem2  26951  dmlogdmgm  26987  basellem1  27044  sgmnncl  27110  chpdifbndlem2  27517  pntibndlem1  27552  pntibnd  27556  pntlemc  27558  abvcxp  27578  ostth2lem1  27581  ostth2lem3  27598  ostth2  27600  sgnmulrp2  32909  xrge0iifhom  34081  omssubadd  34444  signsply0  34695  sinccvglem  35854  unblimceq0lem  36766  unbdqndv2lem2  36770  knoppndvlem14  36785  taupilem1  37635  poimirlem29  37970  heicant  37976  itggt0cn  38011  ftc1cnnc  38013  bfplem1  38143  rrncmslem  38153  aks4d1p1  42515  aks6d1c2  42569  irrapxlem4  43253  irrapxlem5  43254  imo72b2lem1  44596  dvdivbd  46351  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem1  46429  stoweidlem7  46435  stoweidlem11  46439  stoweidlem25  46453  stoweidlem26  46454  stoweidlem34  46462  stoweidlem49  46477  stoweidlem52  46480  stoweidlem60  46488  wallispi  46498  stirlinglem6  46507  stirlinglem11  46512  fourierdlem30  46565  qndenserrnbl  46723  ovnsubaddlem1  46998  hoiqssbllem2  47051  pimrecltpos  47136  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221