MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-np Unicode version

Definition df-np 9380
Description: Define the set of positive reals. A "Dedekind cut" is a partition of the positive rational numbers into two classes such that all the numbers of one class are less than all the numbers of the other. A positive real is defined as the lower class of a Dedekind cut. Definition 9-3.1 of [Gleason] p. 121. (Note: This is a "temporary" definition used in the construction of complex numbers df-c 9519, and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.)
Assertion
Ref Expression
df-np
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-np
StepHypRef Expression
1 cnp 9258 . 2
2 c0 3784 . . . . . 6
3 vx . . . . . . 7
43cv 1394 . . . . . 6
52, 4wpss 3476 . . . . 5
6 cnq 9251 . . . . . 6
74, 6wpss 3476 . . . . 5
85, 7wa 369 . . . 4
9 vz . . . . . . . . . 10
109cv 1394 . . . . . . . . 9
11 vy . . . . . . . . . 10
1211cv 1394 . . . . . . . . 9
13 cltq 9257 . . . . . . . . 9
1410, 12, 13wbr 4452 . . . . . . . 8
159, 3wel 1819 . . . . . . . 8
1614, 15wi 4 . . . . . . 7
1716, 9wal 1393 . . . . . 6
1812, 10, 13wbr 4452 . . . . . . 7
1918, 9, 4wrex 2808 . . . . . 6
2017, 19wa 369 . . . . 5
2120, 11, 4wral 2807 . . . 4
228, 21wa 369 . . 3
2322, 3cab 2442 . 2
241, 23wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  npex  9385  elnp  9386  elnpi  9387
  Copyright terms: Public domain W3C validator