let n be natural number ; :: thesis: ( n > 0 implies for a, b being Element of Segm n
for k being natural number holds
( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . a,b = (a * b) - (k * n) ) )
assume A1: n > 0 ; :: thesis: for a, b being Element of Segm n
for k being natural number holds
( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . a,b = (a * b) - (k * n) )
let a, b be Element of Segm n; :: thesis: for k being natural number holds
( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . a,b = (a * b) - (k * n) )
reconsider a = a, b = b as Element of NAT by ORDINAL1:def 13;
let k be natural number ; :: thesis: ( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . a,b = (a * b) - (k * n) )

A2: now

assume (multint n) . a,b = (a * b) - (k * n) ; :: thesis: ( k * n <= a * b & a * b < (k + 1) * n )
then A3: (a * b) mod n = (a * b) - (k * n) by A1, Def11;
then A4: ((a * b) - (k * n)) + (k * n) >= 0 + (k * n) by XREAL_1:8;
consider t being Nat such that
A5: ( a * b = (n * t) + ((a * b) - (n * k)) & (a * b) - (n * k) < n ) by A1, A3, NAT_D:def 2;
(k + 1) * n = (k * n) + n ;
hence ( k * n <= a * b & a * b < (k + 1) * n ) by A4, A5, XREAL_1:8; :: thesis: verum

end;

now

assume A6: ( k * n <= a * b & a * b < (k + 1) * n ) ; :: thesis: (multint n) . a,b = (a * b) - (k * n)
consider c being Element of NAT such that
A7: c = (a * b) mod n ;
consider t being Nat such that
A8: ( ( a * b = (n * t) + c & c < n ) or ( c = 0 & n = 0 ) ) by A7, NAT_D:def 2;

now

now

consider q being Nat such that
A9: a * b = (k * n) + q by A6, NAT_1:10;
t = k

proof

now

per cases ( t <= k or t > k ) ;

case t <= k ; :: thesis: t = k

then consider r being Nat such that
A10: t + r = k by NAT_1:10;
A11: (n * t) + c = (t * n) + ((r * n) + q) by A1, A8, A9, A10;

now

per cases ( t = k or t <> k ) ;

case t = k ; :: thesis: t = k

hence t = k ; :: thesis: verum

end;

case A12: t <> k ; :: thesis: t = k

r >= 1

proof

assume A13: r < 1 ; :: thesis: contradiction
r = 0

proof

assume r <> 0 ; :: thesis: contradiction
then r > 0 ;
then 1 + 0 <= r by INT_1:20;
hence contradiction by A13; :: thesis: verum

end;

hence contradiction by A10, A12; :: thesis: verum

end;

then r * n >= 1 * n by NAT_1:4;
then A14: (r * n) + q >= (1 * n) + q by XREAL_1:8;
(1 * n) + q >= n by NAT_1:11;
hence t = k by A1, A8, A11, A14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence t = k ; :: thesis: verum

end;

case t > k ; :: thesis: t = k

then t >= k + 1 by INT_1:20;
then A15: n * t >= n * (k + 1) by NAT_1:4;
(n * t) + c >= n * t by NAT_1:11;
hence t = k by A6, A8, A15, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence t = k ; :: thesis: verum

end;

hence (multint n) . a,b = (a * b) - (k * n) by A1, A7, A8, Def11; :: thesis: verum

end;

hence (multint n) . a,b = (a * b) - (k * n) ; :: thesis: verum

end;

hence (multint n) . a,b = (a * b) - (k * n) ; :: thesis: verum

end;

hence ( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . a,b = (a * b) - (k * n) ) by A2; :: thesis: verum