Theorem rpgt0 9905

Description: A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)

Assertion

Ref	Expression
rpgt0	⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Proof of Theorem rpgt0

Step	Hyp	Ref	Expression
1		elrp 9895	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	simprbi 275	1 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2201   class class class wbr 4089  ℝcr 8036  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:  rpge0  9906  rpap0  9910  rpgecl  9922  0nrp  9929  rpgt0d  9939  addlelt  10008  rpsqrtcl  11624  rpmaxcl  11806  rpmincl  11821  xrminrpcl  11857  climconst  11873  sinltxirr  12345  blcntrps  15168  blcntr  15169  bdmet  15255  bdmopn  15257  reeff1o  15526  coseq00topi  15588  coseq0negpitopi  15589