let n be Nat; :: thesis: ( n > 0 implies for a, b being Element of Segm n
for k being Nat 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 Nat 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 Nat 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 12;
let k be Nat; :: thesis: ( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . (a,b) = (a * b) - (k * n) )

A2: now :: thesis: ( k * n <= a * b & a * b < (k + 1) * n implies (multint n) . (a,b) = (a * b) - (k * n) )

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

now :: thesis: (multint n) . (a,b) = (a * b) - (k * n)

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

proof

now :: thesis: ( ( t <= k & t = k ) or ( t > k & t = k ) )

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

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

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

now :: thesis: ( ( t = k & t = k ) or ( t <> k & t = k ) )

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

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

hence t = k ; :: thesis: verum

end;

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

r >= 1

proof

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

proof

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

end;

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

end;

then r * n >= 1 * n by NAT_1:4;
then A12: (r * n) + q >= (1 * n) + q by XREAL_1:6;
(1 * n) + q >= n by NAT_1:11;
hence t = k by A1, A6, A9, A12, 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:7;
then A13: n * t >= n * (k + 1) by NAT_1:4;
(n * t) + c >= n * t by NAT_1:11;
hence t = k by A4, A6, A13, 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, A5, A6, Def10; :: thesis: verum

end;

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

end;

now :: thesis: ( (multint n) . (a,b) = (a * b) - (k * n) implies ( k * n <= a * b & a * b < (k + 1) * n ) )

assume (multint n) . (a,b) = (a * b) - (k * n) ; :: thesis: ( k * n <= a * b & a * b < (k + 1) * n )
then (a * b) mod n = (a * b) - (k * n) by A1, Def10;
then A14: ( ((a * b) - (k * n)) + (k * n) >= 0 + (k * n) & ex t being Nat st
( a * b = (n * t) + ((a * b) - (n * k)) & (a * b) - (n * k) < n ) ) by A1, NAT_D:def 2, XREAL_1:6;
(k + 1) * n = (k * n) + n ;
hence ( k * n <= a * b & a * b < (k + 1) * n ) by A14, XREAL_1:6; :: 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