Theorem rpgt0d 13102

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5166  0cc0 11184   < clt 11324  ℝ⁺crp 13057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-rp 13058

This theorem is referenced by:  rpregt0d  13105  ltmulgt11d  13134  ltmulgt12d  13135  gt0divd  13136  ge0divd  13137  lediv12ad  13158  prodge0rd  13164  expgt0  14146  nnesq  14276  bccl2  14372  01sqrexlem7  15297  sqrtgt0d  15461  iseralt  15733  fsumlt  15848  geomulcvg  15924  eirrlem  16252  sqrt2irrlem  16296  prmind2  16732  4sqlem11  17002  4sqlem12  17003  ssblex  24459  nrginvrcn  24734  mulc1cncf  24950  nmoleub2lem2  25168  itg2mulclem  25801  itggt0  25899  dvgt0  26063  ftc1lem5  26101  aaliou3lem2  26403  abelthlem8  26501  tanord  26598  tanregt0  26599  logccv  26723  cxpgt0d  26798  cxpcn3lem  26808  jensenlem2  27049  dmlogdmgm  27085  basellem1  27142  sgmnncl  27208  chpdifbndlem2  27616  pntibndlem1  27651  pntibnd  27655  pntlemc  27657  abvcxp  27677  ostth2lem1  27680  ostth2lem3  27697  ostth2  27699  xrge0iifhom  33883  omssubadd  34265  sgnmulrp2  34508  signsply0  34528  sinccvglem  35640  unblimceq0lem  36472  unbdqndv2lem2  36476  knoppndvlem14  36491  taupilem1  37287  poimirlem29  37609  heicant  37615  itggt0cn  37650  ftc1cnnc  37652  bfplem1  37782  rrncmslem  37792  aks4d1p1  42033  aks6d1c2  42087  irrapxlem4  42781  irrapxlem5  42782  imo72b2lem1  44131  dvdivbd  45844  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem1  45922  stoweidlem7  45928  stoweidlem11  45932  stoweidlem25  45946  stoweidlem26  45947  stoweidlem34  45955  stoweidlem49  45970  stoweidlem52  45973  stoweidlem60  45981  wallispi  45991  stirlinglem6  46000  stirlinglem11  46005  fourierdlem30  46058  qndenserrnbl  46216  ovnsubaddlem1  46491  hoiqssbllem2  46544  pimrecltpos  46629  smfmullem1  46712  smfmullem2  46713  smfmullem3  46714