Description: Express the division algorithm as stated in divalg in terms of || . (Contributed by Paul Chapman, 31-Mar-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | divalgb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an | |
|
2 | 1 | rexbii | |
3 | r19.42v | |
|
4 | 2 3 | bitri | |
5 | zsubcl | |
|
6 | divides | |
|
7 | 5 6 | sylan2 | |
8 | 7 | 3impb | |
9 | 8 | 3com12 | |
10 | zcn | |
|
11 | zcn | |
|
12 | zmulcl | |
|
13 | 12 | zcnd | |
14 | subadd | |
|
15 | 10 11 13 14 | syl3an | |
16 | addcom | |
|
17 | 11 13 16 | syl2an | |
18 | 17 | 3adant1 | |
19 | 18 | eqeq1d | |
20 | 15 19 | bitrd | |
21 | eqcom | |
|
22 | eqcom | |
|
23 | 20 21 22 | 3bitr3g | |
24 | 23 | 3expia | |
25 | 24 | expcomd | |
26 | 25 | 3impia | |
27 | 26 | imp | |
28 | 27 | rexbidva | |
29 | 28 | 3com23 | |
30 | 9 29 | bitrd | |
31 | 30 | anbi2d | |
32 | 4 31 | bitr4id | |
33 | anass | |
|
34 | 32 33 | bitrdi | |
35 | 34 | 3expa | |
36 | 35 | reubidva | |
37 | elnn0z | |
|
38 | 37 | anbi1i | |
39 | anass | |
|
40 | 38 39 | bitri | |
41 | 40 | eubii | |
42 | df-reu | |
|
43 | df-reu | |
|
44 | 41 42 43 | 3bitr4ri | |
45 | 36 44 | bitrdi | |
46 | 45 | 3adant3 | |