Theorem rpgt0d 13148

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  0cc0 11181   < clt 11324  ℝ⁺crp 13101

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-rp 13102

This theorem is used by:  rpregt0d  13151  ltmulgt11d  13180  ltmulgt12d  13181  gt0divd  13182  ge0divd  13183  lediv12ad  13204  prodge0rd  13210  expgt0  14218  nnesq  14351  bccl2  14447  sgnmulrp2  15241  01sqrexlem7  15395  sqrtgt0d  15560  iseralt  15832  fsumlt  15947  geomulcvg  16025  eirrlem  16352  sqrt2irrlem  16396  prmind2  16840  4sqlem11  17113  4sqlem12  17114  ssblex  24727  nrginvrcn  24991  mulc1cncf  25206  nmoleub2lem2  25417  itg2mulclem  26047  itggt0  26144  dvgt0  26304  ftc1lem5  26340  aaliou3lem2  26652  abelthlem8  26748  tanord  26848  tanregt0  26849  logccv  26973  cxpgt0d  27048  cxpcn3lem  27057  jensenlem2  27297  dmlogdmgm  27333  basellem1  27390  sgmnncl  27456  chpdifbndlem2  27863  pntibndlem1  27898  pntibnd  27902  pntlemc  27904  abvcxp  27924  ostth2lem1  27927  ostth2lem3  27944  ostth2  27946  xrge0iifhom  34551  omssubadd  34915  signsply0  35163  sinccvglem  36406  unblimceq0lem  37342  unbdqndv2lem2  37346  knoppndvlem14  37361  taupilem1  38210  poimirlem29  38535  heicant  38541  itggt0cn  38576  ftc1cnnc  38578  bfplem1  38724  rrncmslem  38734  aks4d1p1  43094  aks6d1c2  43148  irrapxlem4  43785  irrapxlem5  43786  imo72b2lem1  45128  dvdivbd  46877  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  stoweidlem1  46955  stoweidlem7  46961  stoweidlem11  46965  stoweidlem25  46979  stoweidlem26  46980  stoweidlem34  46988  stoweidlem49  47003  stoweidlem52  47006  stoweidlem60  47014  wallispi  47024  stirlinglem6  47033  stirlinglem11  47038  fourierdlem30  47091  qndenserrnbl  47249  ovnsubaddlem1  47524  hoiqssbllem2  47577  pimrecltpos  47662  smfmullem1  47745  smfmullem2  47746  smfmullem3  47747