Theorem rpgt0d 12757

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5078  0cc0 10855   < clt 10993  ℝ⁺crp 12712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-rp 12713

This theorem is referenced by:  rpregt0d  12760  ltmulgt11d  12789  ltmulgt12d  12790  gt0divd  12791  ge0divd  12792  lediv12ad  12813  prodge0rd  12819  expgt0  13797  nnesq  13923  bccl2  14018  sqrlem7  14941  sqrtgt0d  15105  iseralt  15377  fsumlt  15493  geomulcvg  15569  eirrlem  15894  sqrt2irrlem  15938  prmind2  16371  4sqlem11  16637  4sqlem12  16638  ssblex  23562  nrginvrcn  23837  mulc1cncf  24049  nmoleub2lem2  24260  itg2mulclem  24892  itggt0  24989  dvgt0  25149  ftc1lem5  25185  aaliou3lem2  25484  abelthlem8  25579  tanord  25675  tanregt0  25676  logccv  25799  cxpcn3lem  25881  jensenlem2  26118  dmlogdmgm  26154  basellem1  26211  sgmnncl  26277  chpdifbndlem2  26683  pntibndlem1  26718  pntibnd  26722  pntlemc  26724  abvcxp  26744  ostth2lem1  26747  ostth2lem3  26764  ostth2  26766  xrge0iifhom  31866  omssubadd  32246  sgnmulrp2  32489  signsply0  32509  sinccvglem  33609  unblimceq0lem  34665  unbdqndv2lem2  34669  knoppndvlem14  34684  taupilem1  35471  poimirlem29  35785  heicant  35791  itggt0cn  35826  ftc1cnnc  35828  bfplem1  35959  rrncmslem  35969  aks4d1p1  40064  cxpgt0d  40324  irrapxlem4  40627  irrapxlem5  40628  imo72b2lem1  41733  dvdivbd  43418  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  stoweidlem1  43496  stoweidlem7  43502  stoweidlem11  43506  stoweidlem25  43520  stoweidlem26  43521  stoweidlem34  43529  stoweidlem49  43544  stoweidlem52  43547  stoweidlem60  43555  wallispi  43565  stirlinglem6  43574  stirlinglem11  43579  fourierdlem30  43632  qndenserrnbl  43790  ovnsubaddlem1  44062  hoiqssbllem2  44115  pimrecltpos  44197  smfmullem1  44276  smfmullem2  44277  smfmullem3  44278