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) )

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;

end;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)

hence
(multint n) . (a,b) = (a * b) - (k * n)
; :: thesis: verumconsider q being Nat such that

A7: a * b = (k * n) + q by A3, NAT_1:10;

t = k

end;A7: a * b = (k * n) + q by A3, NAT_1:10;

t = k

proof

end;

hence
(multint n) . (a,b) = (a * b) - (k * n)
by A1, A5, A6, Def10; :: thesis: verumnow :: thesis: ( ( t <= k & t = k ) or ( t > k & t = k ) )end;

hence
t = k
; :: thesis: verumper cases
( t <= k or t > k )
;

end;

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;

end;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 ) )end;

hence
t = k
; :: thesis: verumper cases
( t = k or t <> k )
;

end;

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

r >= 1

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;proof

then
r * n >= 1 * n
by NAT_1:4;
assume A11:
r < 1
; :: thesis: contradiction

r = 0

end;r = 0

proof

hence
contradiction
by A8, A10; :: thesis: verum
assume
r <> 0
; :: thesis: contradiction

then 1 + 0 <= r by INT_1:7;

hence contradiction by A11; :: thesis: verum

end;then 1 + 0 <= r by INT_1:7;

hence contradiction by A11; :: thesis: verum

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

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

hence
( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . (a,b) = (a * b) - (k * n) )
by A2; :: thesis: verumassume
(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;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