Theorem rpgt0d 10035

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

Syntax hints:   → wi 4   ∈ wcel 2205   class class class wbr 4111  0cc0 8129   < clt 8310  ℝ⁺crp 9989

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rab 2531  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-br 4112  df-rp 9990

This theorem is referenced by:  rpregt0d  10039  ltmulgt11d  10068  ltmulgt12d  10069  gt0divd  10070  ge0divd  10071  lediv12ad  10092  expgt0  10938  nnesq  11025  bccl2  11134  resqrexlemp1rp  11695  resqrexlemover  11699  resqrexlemnm  11707  resqrexlemgt0  11709  resqrexlemglsq  11711  sqrtgt0d  11848  reccn2ap  12002  fsumlt  12154  eirraplem  12467  dvdsmodexp  12485  bitsmod  12646  prmind2  12821  sqrt2irrlem  12862  modprmn0modprm0  12958  4sqlem11  13103  4sqlem12  13104  modxai  13118  ssblex  15313  mulc1cncf  15471  cncfmptc  15478  mulcncflem  15489  cnplimclemle  15550  pilem3  15665  sgmnncl  15873  iooref1o  16835  trilpolemeq1  16841  nconstwlpolemgt0  16867  taupi  16876