Theorem rpgt0d 13170

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  0cc0 11203   < clt 11346  ℝ⁺crp 13123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-rp 13124

This theorem is used by:  rpregt0d  13173  ltmulgt11d  13202  ltmulgt12d  13203  gt0divd  13204  ge0divd  13205  lediv12ad  13226  prodge0rd  13232  expgt0  14241  nnesq  14374  bccl2  14470  sgnmulrp2  15266  01sqrexlem7  15420  sqrtgt0d  15585  iseralt  15857  fsumlt  15972  geomulcvg  16050  eirrlem  16377  sqrt2irrlem  16421  prmind2  16865  4sqlem11  17138  4sqlem12  17139  ssblex  24752  nrginvrcn  25016  mulc1cncf  25231  nmoleub2lem2  25442  itg2mulclem  26072  itggt0  26169  dvgt0  26329  ftc1lem5  26365  aaliou3lem2  26675  abelthlem8  26771  tanord  26871  tanregt0  26872  logccv  26996  cxpgt0d  27071  cxpcn3lem  27080  jensenlem2  27320  dmlogdmgm  27356  basellem1  27413  sgmnncl  27479  chpdifbndlem2  27886  pntibndlem1  27921  pntibnd  27925  pntlemc  27927  abvcxp  27947  ostth2lem1  27950  ostth2lem3  27967  ostth2  27969  xrge0iifhom  34615  omssubadd  34978  signsply0  35226  sinccvglem  36523  unblimceq0lem  37464  unbdqndv2lem2  37468  knoppndvlem14  37483  taupilem1  38335  poimirlem29  38660  heicant  38666  itggt0cn  38701  ftc1cnnc  38703  bfplem1  38849  rrncmslem  38859  aks4d1p1  43219  aks6d1c2  43273  irrapxlem4  43925  irrapxlem5  43926  imo72b2lem1  45262  dvdivbd  47026  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  stoweidlem1  47104  stoweidlem7  47110  stoweidlem11  47114  stoweidlem25  47128  stoweidlem26  47129  stoweidlem34  47137  stoweidlem49  47152  stoweidlem52  47155  stoweidlem60  47163  wallispi  47173  stirlinglem6  47182  stirlinglem11  47187  fourierdlem30  47240  qndenserrnbl  47398  ovnsubaddlem1  47673  hoiqssbllem2  47726  pimrecltpos  47811  smfmullem1  47894  smfmullem2  47895  smfmullem3  47896