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 
|- RR+ = { x e. RR | 0 < x }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crp 
 |-  RR+
1 vx 
 |-  x
2 cr 
 |-  RR
3 cc0 
 |-  0
4 clt 
 |-  <
5 1 cv 
 |-  x
6 3 5 4 wbr 
 |-  0 < x
7 6 1 2 crab 
 |-  { x e. RR | 0 < x }
8 0 7 wceq 
 |-  RR+ = { x e. RR | 0 < x }