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

Metamath Proof Explorer

Theorem elrpii

Description: Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008)

Ref Expression
Hypotheses elrpi.1 ⊢ A ∈ ℝ
elrpi.2 ⊢ 0 < A
Assertion elrpii ⊢ A ∈ ℝ +

Proof

Step Hyp Ref Expression
1 elrpi.1 ⊢ A ∈ ℝ
2 elrpi.2 ⊢ 0 < A
3 elrp ⊢ A ∈ ℝ + ↔ A ∈ ℝ ∧ 0 < A
4 1 2 3 mpbir2an ⊢ A ∈ ℝ +