This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem repos

Description: Two ways of saying that a real number is positive. (Contributed by NM, 7-May-2007)

Ref Expression
Assertion repos ⊢ A ∈ 0 +∞ ↔ A ∈ ℝ ∧ 0 < A

Proof

Step Hyp Ref Expression
1 breq2 ⊢ x = A → 0 < x ↔ 0 < A
2 ioopos ⊢ 0 +∞ = x ∈ ℝ | 0 < x
3 1 2 elrab2 ⊢ A ∈ 0 +∞ ↔ A ∈ ℝ ∧ 0 < A