Theorem rpgt0d 13054

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5119  0cc0 11129   < clt 11269  ℝ⁺crp 13008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-rp 13009

This theorem is referenced by:  rpregt0d  13057  ltmulgt11d  13086  ltmulgt12d  13087  gt0divd  13088  ge0divd  13089  lediv12ad  13110  prodge0rd  13116  expgt0  14113  nnesq  14245  bccl2  14341  01sqrexlem7  15267  sqrtgt0d  15431  iseralt  15701  fsumlt  15816  geomulcvg  15892  eirrlem  16222  sqrt2irrlem  16266  prmind2  16704  4sqlem11  16975  4sqlem12  16976  ssblex  24367  nrginvrcn  24631  mulc1cncf  24849  nmoleub2lem2  25067  itg2mulclem  25699  itggt0  25797  dvgt0  25961  ftc1lem5  25999  aaliou3lem2  26303  abelthlem8  26401  tanord  26499  tanregt0  26500  logccv  26624  cxpgt0d  26699  cxpcn3lem  26709  jensenlem2  26950  dmlogdmgm  26986  basellem1  27043  sgmnncl  27109  chpdifbndlem2  27517  pntibndlem1  27552  pntibnd  27556  pntlemc  27558  abvcxp  27578  ostth2lem1  27581  ostth2lem3  27598  ostth2  27600  sgnmulrp2  32815  xrge0iifhom  33968  omssubadd  34332  signsply0  34583  sinccvglem  35694  unblimceq0lem  36524  unbdqndv2lem2  36528  knoppndvlem14  36543  taupilem1  37339  poimirlem29  37673  heicant  37679  itggt0cn  37714  ftc1cnnc  37716  bfplem1  37846  rrncmslem  37856  aks4d1p1  42089  aks6d1c2  42143  irrapxlem4  42848  irrapxlem5  42849  imo72b2lem1  44193  dvdivbd  45952  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  stoweidlem1  46030  stoweidlem7  46036  stoweidlem11  46040  stoweidlem25  46054  stoweidlem26  46055  stoweidlem34  46063  stoweidlem49  46078  stoweidlem52  46081  stoweidlem60  46089  wallispi  46099  stirlinglem6  46108  stirlinglem11  46113  fourierdlem30  46166  qndenserrnbl  46324  ovnsubaddlem1  46599  hoiqssbllem2  46652  pimrecltpos  46737  smfmullem1  46820  smfmullem2  46821  smfmullem3  46822