Theorem rpgt0d 12952

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5098  0cc0 11026   < clt 11166  ℝ⁺crp 12905

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-rp 12906

This theorem is referenced by:  rpregt0d  12955  ltmulgt11d  12984  ltmulgt12d  12985  gt0divd  12986  ge0divd  12987  lediv12ad  13008  prodge0rd  13014  expgt0  14018  nnesq  14150  bccl2  14246  01sqrexlem7  15171  sqrtgt0d  15336  iseralt  15608  fsumlt  15723  geomulcvg  15799  eirrlem  16129  sqrt2irrlem  16173  prmind2  16612  4sqlem11  16883  4sqlem12  16884  ssblex  24372  nrginvrcn  24636  mulc1cncf  24854  nmoleub2lem2  25072  itg2mulclem  25703  itggt0  25801  dvgt0  25965  ftc1lem5  26003  aaliou3lem2  26307  abelthlem8  26405  tanord  26503  tanregt0  26504  logccv  26628  cxpgt0d  26703  cxpcn3lem  26713  jensenlem2  26954  dmlogdmgm  26990  basellem1  27047  sgmnncl  27113  chpdifbndlem2  27521  pntibndlem1  27556  pntibnd  27560  pntlemc  27562  abvcxp  27582  ostth2lem1  27585  ostth2lem3  27602  ostth2  27604  sgnmulrp2  32917  xrge0iifhom  34094  omssubadd  34457  signsply0  34708  sinccvglem  35866  unblimceq0lem  36706  unbdqndv2lem2  36710  knoppndvlem14  36725  taupilem1  37522  poimirlem29  37846  heicant  37852  itggt0cn  37887  ftc1cnnc  37889  bfplem1  38019  rrncmslem  38029  aks4d1p1  42326  aks6d1c2  42380  irrapxlem4  43063  irrapxlem5  43064  imo72b2lem1  44406  dvdivbd  46163  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  stoweidlem1  46241  stoweidlem7  46247  stoweidlem11  46251  stoweidlem25  46265  stoweidlem26  46266  stoweidlem34  46274  stoweidlem49  46289  stoweidlem52  46292  stoweidlem60  46300  wallispi  46310  stirlinglem6  46319  stirlinglem11  46324  fourierdlem30  46377  qndenserrnbl  46535  ovnsubaddlem1  46810  hoiqssbllem2  46863  pimrecltpos  46948  smfmullem1  47031  smfmullem2  47032  smfmullem3  47033