Theorem rpgt0d 13081

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5114  0cc0 11118   < clt 11261  ℝ⁺crp 13034

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-rp 13035

This theorem is used by:  rpregt0d  13084  ltmulgt11d  13113  ltmulgt12d  13114  gt0divd  13115  ge0divd  13116  lediv12ad  13137  prodge0rd  13143  expgt0  14151  nnesq  14283  bccl2  14379  sgnmulrp2  15171  01sqrexlem7  15325  sqrtgt0d  15490  iseralt  15762  fsumlt  15878  geomulcvg  15956  eirrlem  16285  sqrt2irrlem  16329  prmind2  16768  4sqlem11  17040  4sqlem12  17041  ssblex  24622  nrginvrcn  24886  mulc1cncf  25101  nmoleub2lem2  25312  itg2mulclem  25942  itggt0  26040  dvgt0  26200  ftc1lem5  26236  aaliou3lem2  26543  abelthlem8  26639  tanord  26740  tanregt0  26741  logccv  26865  cxpgt0d  26940  cxpcn3lem  26949  jensenlem2  27189  dmlogdmgm  27225  basellem1  27282  sgmnncl  27348  chpdifbndlem2  27755  pntibndlem1  27790  pntibnd  27794  pntlemc  27796  abvcxp  27816  ostth2lem1  27819  ostth2lem3  27836  ostth2  27838  xrge0iifhom  34358  omssubadd  34722  signsply0  34970  sinccvglem  36185  unblimceq0lem  37136  unbdqndv2lem2  37140  knoppndvlem14  37155  taupilem1  38006  poimirlem29  38341  heicant  38347  itggt0cn  38382  ftc1cnnc  38384  bfplem1  38514  rrncmslem  38524  aks4d1p1  42884  aks6d1c2  42938  irrapxlem4  43593  irrapxlem5  43594  imo72b2lem1  44936  dvdivbd  46678  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  stoweidlem1  46756  stoweidlem7  46762  stoweidlem11  46766  stoweidlem25  46780  stoweidlem26  46781  stoweidlem34  46789  stoweidlem49  46804  stoweidlem52  46807  stoweidlem60  46815  wallispi  46825  stirlinglem6  46834  stirlinglem11  46839  fourierdlem30  46892  qndenserrnbl  47050  ovnsubaddlem1  47325  hoiqssbllem2  47378  pimrecltpos  47463  smfmullem1  47546  smfmullem2  47547  smfmullem3  47548