Description: The division algorithm (theorem). Dividing an integer N by a nonzero integer D produces a (unique) quotient q and a unique remainder 0 <_ r < ( absD ) . Theorem 1.14 in ApostolNT p. 19. The proof does not use / or |_ or mod . (Contributed by Paul Chapman, 21-Mar-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | divalg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 | |
|
2 | 1 | 3anbi3d | |
3 | 2 | rexbidv | |
4 | 3 | reubidv | |
5 | fveq2 | |
|
6 | 5 | breq2d | |
7 | oveq2 | |
|
8 | 7 | oveq1d | |
9 | 8 | eqeq2d | |
10 | 6 9 | 3anbi23d | |
11 | 10 | rexbidv | |
12 | 11 | reubidv | |
13 | 1z | |
|
14 | 13 | elimel | |
15 | simpl | |
|
16 | eleq1 | |
|
17 | eleq1 | |
|
18 | 15 16 17 13 | elimdhyp | |
19 | simpr | |
|
20 | neeq1 | |
|
21 | neeq1 | |
|
22 | ax-1ne0 | |
|
23 | 19 20 21 22 | elimdhyp | |
24 | eqid | |
|
25 | 14 18 23 24 | divalglem10 | |
26 | 4 12 25 | dedth2h | |
27 | 26 | 3impb | |