Theorem rpgt0d 9828

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

Syntax hints:   → wi 4   ∈ wcel 2177   class class class wbr 4047  0cc0 7932   < clt 8114  ℝ⁺crp 9782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-v 2775  df-un 3171  df-sn 3640  df-pr 3641  df-op 3643  df-br 4048  df-rp 9783

This theorem is referenced by:  rpregt0d  9832  ltmulgt11d  9861  ltmulgt12d  9862  gt0divd  9863  ge0divd  9864  lediv12ad  9885  expgt0  10724  nnesq  10811  bccl2  10920  resqrexlemp1rp  11361  resqrexlemover  11365  resqrexlemnm  11373  resqrexlemgt0  11375  resqrexlemglsq  11377  sqrtgt0d  11514  reccn2ap  11668  fsumlt  11819  eirraplem  12132  dvdsmodexp  12150  bitsmod  12311  prmind2  12486  sqrt2irrlem  12527  modprmn0modprm0  12623  4sqlem11  12768  4sqlem12  12769  modxai  12783  ssblex  14947  mulc1cncf  15105  cncfmptc  15112  mulcncflem  15123  cnplimclemle  15184  pilem3  15299  sgmnncl  15504  iooref1o  16047  trilpolemeq1  16053  nconstwlpolemgt0  16077  taupi  16086