Theorem divmoddilem ≪ | index | src | ≫ 

theorem divmoddilem (a b c: nat):
  $ a != 0 -> a * b // (a * c) = b // c /\ a * b % (a * c) = a * (b % c) $;
StepHypRefExpression
1 div0 
a * b // 0 = 0
2 mul0 
a * 0 = 0
3 muleq2 
c = 0 -> a * c = a * 0
4 2, 3 syl6eq 
c = 0 -> a * c = 0
5 4 diveq2d 
c = 0 -> a * b // (a * c) = a * b // 0
6 1, 5 syl6eq 
c = 0 -> a * b // (a * c) = 0
7 div0 
b // 0 = 0
8 diveq2 
c = 0 -> b // c = b // 0
9 7, 8 syl6eq 
c = 0 -> b // c = 0
10 6, 9 eqtr4d 
c = 0 -> a * b // (a * c) = b // c
11 mod0 
a * b % 0 = a * b
12 4 modeq2d 
c = 0 -> a * b % (a * c) = a * b % 0
13 11, 12 syl6eq 
c = 0 -> a * b % (a * c) = a * b
14 mod0 
b % 0 = b
15 modeq2 
c = 0 -> b % c = b % 0
16 14, 15 syl6eq 
c = 0 -> b % c = b
17 16 muleq2d 
c = 0 -> a * (b % c) = a * b
18 13, 17 eqtr4d 
c = 0 -> a * b % (a * c) = a * (b % c)
19 10, 18 iand 
c = 0 -> a * b // (a * c) = b // c /\ a * b % (a * c) = a * (b % c)
20 19 anwr 
a != 0 /\ c = 0 -> a * b // (a * c) = b // c /\ a * b % (a * c) = a * (b % c)
21 ltmul2 
0 < a -> (b % c < c <-> a * (b % c) < a * c)
22 lt01 
0 < a <-> a != 0
23 anl 
a != 0 /\ ~c = 0 -> a != 0
24 22, 23 sylibr 
a != 0 /\ ~c = 0 -> 0 < a
25 21, 24 syl 
a != 0 /\ ~c = 0 -> (b % c < c <-> a * (b % c) < a * c)
26 modlt 
c != 0 -> b % c < c
27 26 conv ne 
~c = 0 -> b % c < c
28 27 anwr 
a != 0 /\ ~c = 0 -> b % c < c
29 25, 28 mpbid 
a != 0 /\ ~c = 0 -> a * (b % c) < a * c
30 eqtr 
a * c * (b // c) + a * (b % c) = a * (c * (b // c)) + a * (b % c) -> a * (c * (b // c)) + a * (b % c) = a * b -> a * c * (b // c) + a * (b % c) = a * b
31 addeq1 
a * c * (b // c) = a * (c * (b // c)) -> a * c * (b // c) + a * (b % c) = a * (c * (b // c)) + a * (b % c)
32 mulass 
a * c * (b // c) = a * (c * (b // c))
33 31, 32 ax_mp 
a * c * (b // c) + a * (b % c) = a * (c * (b // c)) + a * (b % c)
34 30, 33 ax_mp 
a * (c * (b // c)) + a * (b % c) = a * b -> a * c * (b // c) + a * (b % c) = a * b
35 eqtr3 
a * (c * (b // c) + b % c) = a * (c * (b // c)) + a * (b % c) -> a * (c * (b // c) + b % c) = a * b -> a * (c * (b // c)) + a * (b % c) = a * b
36 muladd 
a * (c * (b // c) + b % c) = a * (c * (b // c)) + a * (b % c)
37 35, 36 ax_mp 
a * (c * (b // c) + b % c) = a * b -> a * (c * (b // c)) + a * (b % c) = a * b
38 muleq2 
c * (b // c) + b % c = b -> a * (c * (b // c) + b % c) = a * b
39 divmod 
c * (b // c) + b % c = b
40 38, 39 ax_mp 
a * (c * (b // c) + b % c) = a * b
41 37, 40 ax_mp 
a * (c * (b // c)) + a * (b % c) = a * b
42 34, 41 ax_mp 
a * c * (b // c) + a * (b % c) = a * b
43 42 a1i 
a != 0 /\ ~c = 0 -> a * c * (b // c) + a * (b % c) = a * b
44 29, 43 eqdivmod 
a != 0 /\ ~c = 0 -> a * b // (a * c) = b // c /\ a * b % (a * c) = a * (b % c)
45 20, 44 casesda 
a != 0 -> a * b // (a * c) = b // c /\ a * b % (a * c) = a * (b % c)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)