Theorem rpgt0d 12939

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5093  0cc0 11013   < clt 11153  ℝ⁺crp 12892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-rp 12893

This theorem is referenced by:  rpregt0d  12942  ltmulgt11d  12971  ltmulgt12d  12972  gt0divd  12973  ge0divd  12974  lediv12ad  12995  prodge0rd  13001  expgt0  14004  nnesq  14136  bccl2  14232  01sqrexlem7  15157  sqrtgt0d  15322  iseralt  15594  fsumlt  15709  geomulcvg  15785  eirrlem  16115  sqrt2irrlem  16159  prmind2  16598  4sqlem11  16869  4sqlem12  16870  ssblex  24344  nrginvrcn  24608  mulc1cncf  24826  nmoleub2lem2  25044  itg2mulclem  25675  itggt0  25773  dvgt0  25937  ftc1lem5  25975  aaliou3lem2  26279  abelthlem8  26377  tanord  26475  tanregt0  26476  logccv  26600  cxpgt0d  26675  cxpcn3lem  26685  jensenlem2  26926  dmlogdmgm  26962  basellem1  27019  sgmnncl  27085  chpdifbndlem2  27493  pntibndlem1  27528  pntibnd  27532  pntlemc  27534  abvcxp  27554  ostth2lem1  27557  ostth2lem3  27574  ostth2  27576  sgnmulrp2  32824  xrge0iifhom  33971  omssubadd  34334  signsply0  34585  sinccvglem  35737  unblimceq0lem  36571  unbdqndv2lem2  36575  knoppndvlem14  36590  taupilem1  37386  poimirlem29  37709  heicant  37715  itggt0cn  37750  ftc1cnnc  37752  bfplem1  37882  rrncmslem  37892  aks4d1p1  42189  aks6d1c2  42243  irrapxlem4  42942  irrapxlem5  42943  imo72b2lem1  44286  dvdivbd  46045  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  stoweidlem1  46123  stoweidlem7  46129  stoweidlem11  46133  stoweidlem25  46147  stoweidlem26  46148  stoweidlem34  46156  stoweidlem49  46171  stoweidlem52  46174  stoweidlem60  46182  wallispi  46192  stirlinglem6  46201  stirlinglem11  46206  fourierdlem30  46259  qndenserrnbl  46417  ovnsubaddlem1  46692  hoiqssbllem2  46745  pimrecltpos  46830  smfmullem1  46913  smfmullem2  46914  smfmullem3  46915