Theorem rpgt0d 12704

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5070  0cc0 10802   < clt 10940  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-rp 12660

This theorem is referenced by:  rpregt0d  12707  ltmulgt11d  12736  ltmulgt12d  12737  gt0divd  12738  ge0divd  12739  lediv12ad  12760  prodge0rd  12766  expgt0  13744  nnesq  13870  bccl2  13965  sqrlem7  14888  sqrtgt0d  15052  iseralt  15324  fsumlt  15440  geomulcvg  15516  eirrlem  15841  sqrt2irrlem  15885  prmind2  16318  4sqlem11  16584  4sqlem12  16585  ssblex  23489  nrginvrcn  23762  mulc1cncf  23974  nmoleub2lem2  24185  itg2mulclem  24816  itggt0  24913  dvgt0  25073  ftc1lem5  25109  aaliou3lem2  25408  abelthlem8  25503  tanord  25599  tanregt0  25600  logccv  25723  cxpcn3lem  25805  jensenlem2  26042  dmlogdmgm  26078  basellem1  26135  sgmnncl  26201  chpdifbndlem2  26607  pntibndlem1  26642  pntibnd  26646  pntlemc  26648  abvcxp  26668  ostth2lem1  26671  ostth2lem3  26688  ostth2  26690  xrge0iifhom  31789  omssubadd  32167  sgnmulrp2  32410  signsply0  32430  sinccvglem  33530  unblimceq0lem  34613  unbdqndv2lem2  34617  knoppndvlem14  34632  taupilem1  35419  poimirlem29  35733  heicant  35739  itggt0cn  35774  ftc1cnnc  35776  bfplem1  35907  rrncmslem  35917  aks4d1p1  40012  cxpgt0d  40265  irrapxlem4  40563  irrapxlem5  40564  imo72b2lem1  41669  dvdivbd  43354  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem1  43432  stoweidlem7  43438  stoweidlem11  43442  stoweidlem25  43456  stoweidlem26  43457  stoweidlem34  43465  stoweidlem49  43480  stoweidlem52  43483  stoweidlem60  43491  wallispi  43501  stirlinglem6  43510  stirlinglem11  43515  fourierdlem30  43568  qndenserrnbl  43726  ovnsubaddlem1  43998  hoiqssbllem2  44051  pimrecltpos  44133  smfmullem1  44212  smfmullem2  44213  smfmullem3  44214