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

Metamath Proof Explorer

Definition df-rp

Description: Define the set of positive reals. Definition of positive numbers in Apostol p. 20. (Contributed by NM, 27-Oct-2007)

Ref Expression
Assertion df-rp ℝ+ = { 𝑥 ∈ ℝ ∣ 0 < 𝑥 }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crp ⊢ ℝ+
1 vx ⊢ 𝑥
2 cr ⊢ ℝ
3 cc0 ⊢ 0
4 clt ⊢ <
5 1 cv ⊢ 𝑥
6 3 5 4 wbr ⊢ 0 < 𝑥
7 6 1 2 crab ⊢ { 𝑥 ∈ ℝ ∣ 0 < 𝑥 }
8 0 7 wceq ⊢ ℝ+ = { 𝑥 ∈ ℝ ∣ 0 < 𝑥 }