Theorem rpgt0d 12998

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5107  0cc0 11068   < clt 11208  ℝ⁺crp 12951

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-rp 12952

This theorem is referenced by:  rpregt0d  13001  ltmulgt11d  13030  ltmulgt12d  13031  gt0divd  13032  ge0divd  13033  lediv12ad  13054  prodge0rd  13060  expgt0  14060  nnesq  14192  bccl2  14288  01sqrexlem7  15214  sqrtgt0d  15379  iseralt  15651  fsumlt  15766  geomulcvg  15842  eirrlem  16172  sqrt2irrlem  16216  prmind2  16655  4sqlem11  16926  4sqlem12  16927  ssblex  24316  nrginvrcn  24580  mulc1cncf  24798  nmoleub2lem2  25016  itg2mulclem  25647  itggt0  25745  dvgt0  25909  ftc1lem5  25947  aaliou3lem2  26251  abelthlem8  26349  tanord  26447  tanregt0  26448  logccv  26572  cxpgt0d  26647  cxpcn3lem  26657  jensenlem2  26898  dmlogdmgm  26934  basellem1  26991  sgmnncl  27057  chpdifbndlem2  27465  pntibndlem1  27500  pntibnd  27504  pntlemc  27506  abvcxp  27526  ostth2lem1  27529  ostth2lem3  27546  ostth2  27548  sgnmulrp2  32761  xrge0iifhom  33927  omssubadd  34291  signsply0  34542  sinccvglem  35659  unblimceq0lem  36494  unbdqndv2lem2  36498  knoppndvlem14  36513  taupilem1  37309  poimirlem29  37643  heicant  37649  itggt0cn  37684  ftc1cnnc  37686  bfplem1  37816  rrncmslem  37826  aks4d1p1  42064  aks6d1c2  42118  irrapxlem4  42813  irrapxlem5  42814  imo72b2lem1  44158  dvdivbd  45921  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem1  45999  stoweidlem7  46005  stoweidlem11  46009  stoweidlem25  46023  stoweidlem26  46024  stoweidlem34  46032  stoweidlem49  46047  stoweidlem52  46050  stoweidlem60  46058  wallispi  46068  stirlinglem6  46077  stirlinglem11  46082  fourierdlem30  46135  qndenserrnbl  46293  ovnsubaddlem1  46568  hoiqssbllem2  46621  pimrecltpos  46706  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791