Description: A positive real is a positive real number. (Contributed by NM, 11-Nov-2008) (Revised by Mario Carneiro, 31-Jan-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | rpregt0 | ⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrp | ⊢ ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) | |
2 | 1 | biimpi | ⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) |