Theorem divmod1 ≪ | index | src | ≫ 

theorem divmod1 (a b c: nat): $ a // b % c = a % (b * c) // b $;
StepHypRefExpression
1 mod01 
0 % c = 0
2 div0 
a // 0 = 0
3 diveq2 
b = 0 -> a // b = a // 0
4 2, 3 syl6eq 
b = 0 -> a // b = 0
5 4 modeq1d 
b = 0 -> a // b % c = 0 % c
6 1, 5 syl6eq 
b = 0 -> a // b % c = 0
7 div0 
a % (b * c) // 0 = 0
8 diveq2 
b = 0 -> a % (b * c) // b = a % (b * c) // 0
9 7, 8 syl6eq 
b = 0 -> a % (b * c) // b = 0
10 6, 9 eqtr4d 
b = 0 -> a // b % c = a % (b * c) // b
11 mod0 
a // b % 0 = a // b
12 modeq2 
c = 0 -> a // b % c = a // b % 0
13 11, 12 syl6eq 
c = 0 -> a // b % c = a // b
14 mod0 
a % 0 = a
15 mul02 
b * 0 = 0
16 muleq2 
c = 0 -> b * c = b * 0
17 15, 16 syl6eq 
c = 0 -> b * c = 0
18 17 modeq2d 
c = 0 -> a % (b * c) = a % 0
19 14, 18 syl6eq 
c = 0 -> a % (b * c) = a
20 19 diveq1d 
c = 0 -> a % (b * c) // b = a // b
21 13, 20 eqtr4d 
c = 0 -> a // b % c = a % (b * c) // b
22 21 anwr 
~b = 0 /\ c = 0 -> a // b % c = a % (b * c) // b
23 divltmul1 
b != 0 -> (a % (b * c) // b < c <-> a % (b * c) < b * c)
24 23 conv ne 
~b = 0 -> (a % (b * c) // b < c <-> a % (b * c) < b * c)
25 24 anwl 
~b = 0 /\ ~c = 0 -> (a % (b * c) // b < c <-> a % (b * c) < b * c)
26 mulne0 
b * c != 0 <-> b != 0 /\ c != 0
27 26 conv ne 
b * c != 0 <-> ~b = 0 /\ ~c = 0
28 modlt 
b * c != 0 -> a % (b * c) < b * c
29 27, 28 sylbir 
~b = 0 /\ ~c = 0 -> a % (b * c) < b * c
30 25, 29 mpbird 
~b = 0 /\ ~c = 0 -> a % (b * c) // b < c
31 modlt 
b != 0 -> a % (b * c) % b < b
32 31 conv ne 
~b = 0 -> a % (b * c) % b < b
33 32 anwl 
~b = 0 /\ ~c = 0 -> a % (b * c) % b < b
34 eqtr 
b * (c * (a // (b * c)) + a % (b * c) // b) + a % (b * c) % b = b * (c * (a // (b * c))) + b * (a % (b * c) // b) + a % (b * c) % b ->
  b * (c * (a // (b * c))) + b * (a % (b * c) // b) + a % (b * c) % b = a ->
  b * (c * (a // (b * c)) + a % (b * c) // b) + a % (b * c) % b = a
35 addeq1 
b * (c * (a // (b * c)) + a % (b * c) // b) = b * (c * (a // (b * c))) + b * (a % (b * c) // b) ->
  b * (c * (a // (b * c)) + a % (b * c) // b) + a % (b * c) % b = b * (c * (a // (b * c))) + b * (a % (b * c) // b) + a % (b * c) % b
36 muladd 
b * (c * (a // (b * c)) + a % (b * c) // b) = b * (c * (a // (b * c))) + b * (a % (b * c) // b)
37 35, 36 ax_mp 
b * (c * (a // (b * c)) + a % (b * c) // b) + a % (b * c) % b = b * (c * (a // (b * c))) + b * (a % (b * c) // b) + a % (b * c) % b
38 34, 37 ax_mp 
b * (c * (a // (b * c))) + b * (a % (b * c) // b) + a % (b * c) % b = a -> b * (c * (a // (b * c)) + a % (b * c) // b) + a % (b * c) % b = a
39 eqtr 
b * (c * (a // (b * c))) + b * (a % (b * c) // b) + a % (b * c) % b = b * (c * (a // (b * c))) + (b * (a % (b * c) // b) + a % (b * c) % b) ->
  b * (c * (a // (b * c))) + (b * (a % (b * c) // b) + a % (b * c) % b) = a ->
  b * (c * (a // (b * c))) + b * (a % (b * c) // b) + a % (b * c) % b = a
40 addass 
b * (c * (a // (b * c))) + b * (a % (b * c) // b) + a % (b * c) % b = b * (c * (a // (b * c))) + (b * (a % (b * c) // b) + a % (b * c) % b)
41 39, 40 ax_mp 
b * (c * (a // (b * c))) + (b * (a % (b * c) // b) + a % (b * c) % b) = a -> b * (c * (a // (b * c))) + b * (a % (b * c) // b) + a % (b * c) % b = a
42 eqtr 
b * (c * (a // (b * c))) + (b * (a % (b * c) // b) + a % (b * c) % b) = b * (c * (a // (b * c))) + a % (b * c) ->
  b * (c * (a // (b * c))) + a % (b * c) = a ->
  b * (c * (a // (b * c))) + (b * (a % (b * c) // b) + a % (b * c) % b) = a
43 addeq2 
b * (a % (b * c) // b) + a % (b * c) % b = a % (b * c) ->
  b * (c * (a // (b * c))) + (b * (a % (b * c) // b) + a % (b * c) % b) = b * (c * (a // (b * c))) + a % (b * c)
44 divmod 
b * (a % (b * c) // b) + a % (b * c) % b = a % (b * c)
45 43, 44 ax_mp 
b * (c * (a // (b * c))) + (b * (a % (b * c) // b) + a % (b * c) % b) = b * (c * (a // (b * c))) + a % (b * c)
46 42, 45 ax_mp 
b * (c * (a // (b * c))) + a % (b * c) = a -> b * (c * (a // (b * c))) + (b * (a % (b * c) // b) + a % (b * c) % b) = a
47 eqtr3 
b * c * (a // (b * c)) + a % (b * c) = b * (c * (a // (b * c))) + a % (b * c) ->
  b * c * (a // (b * c)) + a % (b * c) = a ->
  b * (c * (a // (b * c))) + a % (b * c) = a
48 addeq1 
b * c * (a // (b * c)) = b * (c * (a // (b * c))) -> b * c * (a // (b * c)) + a % (b * c) = b * (c * (a // (b * c))) + a % (b * c)
49 mulass 
b * c * (a // (b * c)) = b * (c * (a // (b * c)))
50 48, 49 ax_mp 
b * c * (a // (b * c)) + a % (b * c) = b * (c * (a // (b * c))) + a % (b * c)
51 47, 50 ax_mp 
b * c * (a // (b * c)) + a % (b * c) = a -> b * (c * (a // (b * c))) + a % (b * c) = a
52 divmod 
b * c * (a // (b * c)) + a % (b * c) = a
53 51, 52 ax_mp 
b * (c * (a // (b * c))) + a % (b * c) = a
54 46, 53 ax_mp 
b * (c * (a // (b * c))) + (b * (a % (b * c) // b) + a % (b * c) % b) = a
55 41, 54 ax_mp 
b * (c * (a // (b * c))) + b * (a % (b * c) // b) + a % (b * c) % b = a
56 38, 55 ax_mp 
b * (c * (a // (b * c)) + a % (b * c) // b) + a % (b * c) % b = a
57 56 a1i 
~b = 0 /\ ~c = 0 -> b * (c * (a // (b * c)) + a % (b * c) // b) + a % (b * c) % b = a
58 33, 57 eqdivmod 
~b = 0 /\ ~c = 0 -> a // b = c * (a // (b * c)) + a % (b * c) // b /\ a % b = a % (b * c) % b
59 58 anld 
~b = 0 /\ ~c = 0 -> a // b = c * (a // (b * c)) + a % (b * c) // b
60 59 eqcomd 
~b = 0 /\ ~c = 0 -> c * (a // (b * c)) + a % (b * c) // b = a // b
61 30, 60 eqdivmod 
~b = 0 /\ ~c = 0 -> a // b // c = a // (b * c) /\ a // b % c = a % (b * c) // b
62 61 anrd 
~b = 0 /\ ~c = 0 -> a // b % c = a % (b * c) // b
63 22, 62 casesda 
~b = 0 -> a // b % c = a % (b * c) // b
64 10, 63 cases 
a // b % c = a % (b * c) // b

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)