Theorem rpgt0d 13037

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

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5099  0cc0 11070   < clt 11213  ℝ⁺crp 12990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-rp 12991

This theorem is referenced by:  rpregt0d  13040  ltmulgt11d  13069  ltmulgt12d  13070  gt0divd  13071  ge0divd  13072  lediv12ad  13093  prodge0rd  13099  expgt0  14105  nnesq  14237  bccl2  14333  01sqrexlem7  15258  sqrtgt0d  15423  iseralt  15695  fsumlt  15811  geomulcvg  15889  eirrlem  16219  sqrt2irrlem  16263  prmind2  16702  4sqlem11  16974  4sqlem12  16975  ssblex  24468  nrginvrcn  24732  mulc1cncf  24947  nmoleub2lem2  25158  itg2mulclem  25788  itggt0  25886  dvgt0  26046  ftc1lem5  26082  aaliou3lem2  26384  abelthlem8  26479  tanord  26580  tanregt0  26581  logccv  26705  cxpgt0d  26780  cxpcn3lem  26789  jensenlem2  27029  dmlogdmgm  27065  basellem1  27122  sgmnncl  27188  chpdifbndlem2  27595  pntibndlem1  27630  pntibnd  27634  pntlemc  27636  abvcxp  27656  ostth2lem1  27659  ostth2lem3  27676  ostth2  27678  sgnmulrp2  32988  xrge0iifhom  34195  omssubadd  34558  signsply0  34809  sinccvglem  35986  unblimceq0lem  36908  unbdqndv2lem2  36912  knoppndvlem14  36927  taupilem1  37777  poimirlem29  38112  heicant  38118  itggt0cn  38153  ftc1cnnc  38155  bfplem1  38285  rrncmslem  38295  aks4d1p1  42657  aks6d1c2  42711  irrapxlem4  43366  irrapxlem5  43367  imo72b2lem1  44709  dvdivbd  46461  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  stoweidlem1  46539  stoweidlem7  46545  stoweidlem11  46549  stoweidlem25  46563  stoweidlem26  46564  stoweidlem34  46572  stoweidlem49  46587  stoweidlem52  46590  stoweidlem60  46598  wallispi  46608  stirlinglem6  46617  stirlinglem11  46622  fourierdlem30  46675  qndenserrnbl  46833  ovnsubaddlem1  47108  hoiqssbllem2  47161  pimrecltpos  47246  smfmullem1  47329  smfmullem2  47330  smfmullem3  47331