Theorem divdiv ≪ | index | src | ≫ 

theorem divdiv (a b c: nat): $ a // b // c = a // (b * c) $;
StepHypRefExpression
1 div01 
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 diveq1d 
b = 0 -> a // b // c = 0 // c
6 1, 5 syl6eq 
b = 0 -> a // b // c = 0
7 mul01 
0 * c = 0
8 muleq1 
b = 0 -> b * c = 0 * c
9 7, 8 syl6eq 
b = 0 -> b * c = 0
10 9 diveq2d 
b = 0 -> a // (b * c) = a // 0
11 2, 10 syl6eq 
b = 0 -> a // (b * c) = 0
12 6, 11 eqtr4d 
b = 0 -> a // b // c = a // (b * c)
13 div0 
a // b // 0 = 0
14 diveq2 
c = 0 -> a // b // c = a // b // 0
15 13, 14 syl6eq 
c = 0 -> a // b // c = 0
16 mul02 
b * 0 = 0
17 muleq2 
c = 0 -> b * c = b * 0
18 16, 17 syl6eq 
c = 0 -> b * c = 0
19 18 diveq2d 
c = 0 -> a // (b * c) = a // 0
20 2, 19 syl6eq 
c = 0 -> a // (b * c) = 0
21 15, 20 eqtr4d 
c = 0 -> a // b // c = a // (b * c)
22 21 anwr 
~b = 0 /\ c = 0 -> a // b // c = a // (b * c)
23 mulne0 
b * c != 0 <-> b != 0 /\ c != 0
24 23 conv ne 
b * c != 0 <-> ~b = 0 /\ ~c = 0
25 ledivmul1 
b * c != 0 -> (a // b // c <= a // (b * c) <-> b * c * (a // b // c) <= a)
26 24, 25 sylbir 
~b = 0 /\ ~c = 0 -> (a // b // c <= a // (b * c) <-> b * c * (a // b // c) <= a)
27 leeq1 
b * c * (a // b // c) = b * (c * (a // b // c)) -> (b * c * (a // b // c) <= a <-> b * (c * (a // b // c)) <= a)
28 mulass 
b * c * (a // b // c) = b * (c * (a // b // c))
29 27, 28 ax_mp 
b * c * (a // b // c) <= a <-> b * (c * (a // b // c)) <= a
30 letr 
b * (c * (a // b // c)) <= b * (a // b) -> b * (a // b) <= a -> b * (c * (a // b // c)) <= a
31 lemul2a 
c * (a // b // c) <= a // b -> b * (c * (a // b // c)) <= b * (a // b)
32 muldivle 
c * (a // b // c) <= a // b
33 31, 32 ax_mp 
b * (c * (a // b // c)) <= b * (a // b)
34 30, 33 ax_mp 
b * (a // b) <= a -> b * (c * (a // b // c)) <= a
35 muldivle 
b * (a // b) <= a
36 34, 35 ax_mp 
b * (c * (a // b // c)) <= a
37 29, 36 mpbir 
b * c * (a // b // c) <= a
38 37 a1i 
~b = 0 /\ ~c = 0 -> b * c * (a // b // c) <= a
39 26, 38 mpbird 
~b = 0 /\ ~c = 0 -> a // b // c <= a // (b * c)
40 ledivmul1 
c != 0 -> (a // (b * c) <= a // b // c <-> c * (a // (b * c)) <= a // b)
41 40 conv ne 
~c = 0 -> (a // (b * c) <= a // b // c <-> c * (a // (b * c)) <= a // b)
42 41 anwr 
~b = 0 /\ ~c = 0 -> (a // (b * c) <= a // b // c <-> c * (a // (b * c)) <= a // b)
43 ledivmul1 
b != 0 -> (c * (a // (b * c)) <= a // b <-> b * (c * (a // (b * c))) <= a)
44 43 conv ne 
~b = 0 -> (c * (a // (b * c)) <= a // b <-> b * (c * (a // (b * c))) <= a)
45 44 anwl 
~b = 0 /\ ~c = 0 -> (c * (a // (b * c)) <= a // b <-> b * (c * (a // (b * c))) <= a)
46 leeq1 
b * c * (a // (b * c)) = b * (c * (a // (b * c))) -> (b * c * (a // (b * c)) <= a <-> b * (c * (a // (b * c))) <= a)
47 mulass 
b * c * (a // (b * c)) = b * (c * (a // (b * c)))
48 46, 47 ax_mp 
b * c * (a // (b * c)) <= a <-> b * (c * (a // (b * c))) <= a
49 muldivle 
b * c * (a // (b * c)) <= a
50 48, 49 mpbi 
b * (c * (a // (b * c))) <= a
51 50 a1i 
~b = 0 /\ ~c = 0 -> b * (c * (a // (b * c))) <= a
52 45, 51 mpbird 
~b = 0 /\ ~c = 0 -> c * (a // (b * c)) <= a // b
53 42, 52 mpbird 
~b = 0 /\ ~c = 0 -> a // (b * c) <= a // b // c
54 39, 53 leasymd 
~b = 0 /\ ~c = 0 -> a // b // c = a // (b * c)
55 22, 54 casesda 
~b = 0 -> a // b // c = a // (b * c)
56 12, 55 cases 
a // b // 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)