let i, k, n be Nat; :: thesis: (n div k) div i = n div (k * i)
now :: thesis: (n div k) div i = n div (k * i)
per cases ( i = 0 or i <> 0 ) ;
suppose A1: i = 0 ; :: thesis: (n div k) div i = n div (k * i)
hence (n div k) div i = 0 by NAT_D:def 1
.= n div (k * i) by A1, NAT_D:def 1 ;
:: thesis: verum
end;
suppose A2: i <> 0 ; :: thesis: (n div k) div i = n div (k * i)
now :: thesis: (n div k) div i = n div (k * i)
per cases ( k = 0 or k <> 0 ) ;
suppose A3: k = 0 ; :: thesis: (n div k) div i = n div (k * i)
then n div k = 0 by NAT_D:def 1;
hence (n div k) div i = n div (k * i) by A3, Th2; :: thesis: verum
end;
suppose A4: k <> 0 ; :: thesis: (n div k) div i = n div (k * i)
consider t2 being Nat such that
A5: n div k = (i * ((n div k) div i)) + t2 and
A6: t2 < i by A2, NAT_D:def 1;
t2 + 1 <= i by A6, NAT_1:13;
then A7: k * (t2 + 1) <= k * i by XREAL_1:64;
consider t1 being Nat such that
A8: n = (k * (n div k)) + t1 and
A9: t1 < k by A4, NAT_D:def 1;
(k * t2) + t1 < (k * t2) + (k * 1) by A9, XREAL_1:6;
then ((k * t2) + t1) - (k * i) < (k * (t2 + 1)) - (k * (t2 + 1)) by A7, XREAL_1:14;
then A10: (k * t2) + t1 < 0 + (k * i) by XREAL_1:19;
n = ((k * i) * ((n div k) div i)) + ((k * t2) + t1) by A8, A5;
hence (n div k) div i = n div (k * i) by A10, NAT_D:def 1; :: thesis: verum
end;
end;
end;
hence (n div k) div i = n div (k * i) ; :: thesis: verum
end;
end;
end;
hence (n div k) div i = n div (k * i) ; :: thesis: verum