Theorem rpgt0d 9939

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

Syntax hints:   → wi 4   ∈ wcel 2201   class class class wbr 4089  0cc0 8037   < clt 8219  ℝ⁺crp 9893

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-rab 2518  df-v 2803  df-un 3203  df-sn 3676  df-pr 3677  df-op 3679  df-br 4090  df-rp 9894

This theorem is referenced by:  rpregt0d  9943  ltmulgt11d  9972  ltmulgt12d  9973  gt0divd  9974  ge0divd  9975  lediv12ad  9996  expgt0  10840  nnesq  10927  bccl2  11036  resqrexlemp1rp  11589  resqrexlemover  11593  resqrexlemnm  11601  resqrexlemgt0  11603  resqrexlemglsq  11605  sqrtgt0d  11742  reccn2ap  11896  fsumlt  12048  eirraplem  12361  dvdsmodexp  12379  bitsmod  12540  prmind2  12715  sqrt2irrlem  12756  modprmn0modprm0  12852  4sqlem11  12997  4sqlem12  12998  modxai  13012  ssblex  15184  mulc1cncf  15342  cncfmptc  15349  mulcncflem  15360  cnplimclemle  15421  pilem3  15536  sgmnncl  15741  iooref1o  16705  trilpolemeq1  16711  nconstwlpolemgt0  16736  taupi  16745