:: Modular Integer Arithmetic
:: by Christoph Schwarzweller
::
:: Received May 13, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users


begin

Lm1: for f being integer-yielding FinSequence holds f is FinSequence of INT
proof end;

registration
let f be complex-valued FinSequence;
let n be natural number ;
cluster f | n -> complex-valued ;
coherence
f | n is complex-valued
;
end;

registration
let f be integer-valued FinSequence;
let n be natural number ;
cluster f | n -> integer-valued ;
coherence
f | n is integer-yielding
;
end;

registration
let f be integer-valued FinSequence;
let n be natural number ;
cluster f /^ n -> integer-valued ;
coherence
f /^ n is integer-yielding
proof end;
end;

registration
let i be Integer;
cluster <*i*> -> integer-valued ;
coherence
<*i*> is integer-yielding
proof end;
end;

registration
let f, g be integer-valued FinSequence;
cluster f ^ g -> integer-valued ;
coherence
f ^ g is integer-yielding
proof end;
end;

theorem Th1: :: INT_6:1
for f1, f2 being complex-valued FinSequence holds len (f1 + f2) = min ((len f1),(len f2))
proof end;

theorem Th2: :: INT_6:2
for f1, f2 being complex-valued FinSequence holds len (f1 - f2) = min ((len f1),(len f2))
proof end;

theorem Th3: :: INT_6:3
for f1, f2 being complex-valued FinSequence holds len (f1 (#) f2) = min ((len f1),(len f2))
proof end;

Lm2: for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 + m2) = len m1
proof end;

Lm3: for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 - m2) = len m1
proof end;

Lm4: for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
len (m1 (#) m2) = len m1
proof end;

theorem Th4: :: INT_6:4
for m1, m2 being complex-valued FinSequence st len m1 = len m2 holds
for k being natural number st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k)
proof end;

registration
let F be integer-valued FinSequence;
cluster Sum F -> integer ;
coherence
Sum F is integer
proof end;
cluster Product F -> integer ;
coherence
Product F is integer
proof end;
end;

Lm5: for z being integer-yielding FinSequence holds z is FinSequence of REAL
proof end;

theorem Th5: :: INT_6:5
for f being complex-valued FinSequence
for i being natural number st i + 1 <= len f holds
(f | i) ^ <*(f . (i + 1))*> = f | (i + 1)
proof end;

theorem Th6: :: INT_6:6
for f being complex-valued FinSequence st ex i being natural number st
( i in dom f & f . i = 0 ) holds
Product f = 0
proof end;

theorem Th7: :: INT_6:7
for n, a, b being Integer holds (a - b) mod n = ((a mod n) - (b mod n)) mod n
proof end;

theorem Th8: :: INT_6:8
for i, j, k being Integer st i divides j holds
k * i divides k * j
proof end;

theorem Th9: :: INT_6:9
for m being integer-valued FinSequence
for i being natural number st i in dom m & m . i <> 0 holds
(Product m) / (m . i) is Integer
proof end;

theorem Th10: :: INT_6:10
for m being integer-valued FinSequence
for i being natural number st i in dom m holds
ex z being Integer st z * (m . i) = Product m
proof end;

Lm6: for m being integer-yielding FinSequence
for i, j being natural number st i in dom m & j in dom m & j <> i & m . j <> 0 holds
ex z being Integer st z * (m . i) = (Product m) / (m . j)
proof end;

theorem :: INT_6:11
for m being integer-valued FinSequence
for i, j being natural number st i in dom m & j in dom m & j <> i & m . j <> 0 holds
(Product m) / ((m . i) * (m . j)) is Integer
proof end;

theorem :: INT_6:12
for m being integer-valued FinSequence
for i, j being natural number st i in dom m & j in dom m & j <> i & m . j <> 0 holds
ex z being Integer st z * (m . i) = (Product m) / (m . j) by Lm6;

begin

theorem Th13: :: INT_6:13
for i being Integer holds
( abs i divides i & i divides abs i )
proof end;

theorem Th14: :: INT_6:14
for i, j being Integer holds i gcd j = i gcd (abs j)
proof end;

theorem Th15: :: INT_6:15
for i, j being Integer st i,j are_relative_prime holds
i lcm j = abs (i * j)
proof end;

theorem Th16: :: INT_6:16
for i, j, k being Integer holds (i * j) gcd (i * k) = (abs i) * (j gcd k)
proof end;

theorem Th17: :: INT_6:17
for i, j being Integer holds (i * j) gcd i = abs i
proof end;

theorem Th18: :: INT_6:18
for i, j, k being Integer holds i gcd (j gcd k) = (i gcd j) gcd k
proof end;

theorem Th19: :: INT_6:19
for i, j, k being Integer st i,j are_relative_prime holds
i gcd (j * k) = i gcd k
proof end;

theorem Th20: :: INT_6:20
for i, j being Integer st i,j are_relative_prime holds
i * j divides i lcm j
proof end;

theorem Th21: :: INT_6:21
for x, y, i, j being Integer st i,j are_relative_prime & x,y are_congruent_mod i & x,y are_congruent_mod j holds
x,y are_congruent_mod i * j
proof end;

theorem Th22: :: INT_6:22
for i, j being Integer st i,j are_relative_prime holds
ex s being Integer st s * i,1 are_congruent_mod j
proof end;

begin

notation
let f be integer-valued FinSequence;
antonym multiplicative-trivial f for non-empty ;
end;

definition
let f be integer-valued FinSequence;
redefine attr f is non-empty means :Def1: :: INT_6:def 1
for i being natural number holds
( not i in dom f or not f . i = 0 );
compatibility
( not f is multiplicative-trivial iff for i being natural number holds
( not i in dom f or not f . i = 0 ) )
proof end;
end;

:: deftheorem Def1 defines multiplicative-trivial INT_6:def 1 :
for f being integer-valued FinSequence holds
( not f is multiplicative-trivial iff for i being natural number holds
( not i in dom f or not f . i = 0 ) );

registration
cluster V1() multiplicative-trivial Function-like V29() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued rational-valued integer-valued set ;
existence
ex b1 being integer-valued FinSequence st b1 is multiplicative-trivial
proof end;
cluster V1() non multiplicative-trivial Function-like V29() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued rational-valued integer-valued set ;
existence
not for b1 being integer-valued FinSequence holds b1 is multiplicative-trivial
by Def1;
cluster V1() Function-like non empty V29() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued rational-valued integer-valued positive-yielding set ;
existence
ex b1 being integer-valued FinSequence st
( not b1 is empty & b1 is positive-yielding )
proof end;
end;

theorem :: INT_6:23
for m being multiplicative-trivial integer-valued FinSequence holds Product m = 0
proof end;

definition
let f be integer-valued FinSequence;
attr f is Chinese_Remainder means :Def2: :: INT_6:def 2
for i, j being natural number st i in dom f & j in dom f & i <> j holds
f . i,f . j are_relative_prime ;
end;

:: deftheorem Def2 defines Chinese_Remainder INT_6:def 2 :
for f being integer-valued FinSequence holds
( f is Chinese_Remainder iff for i, j being natural number st i in dom f & j in dom f & i <> j holds
f . i,f . j are_relative_prime );

registration
cluster V1() Function-like non empty V29() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued rational-valued integer-valued positive-yielding Chinese_Remainder set ;
existence
ex b1 being integer-valued FinSequence st
( not b1 is empty & b1 is positive-yielding & b1 is Chinese_Remainder )
proof end;
end;

definition
mode CR_Sequence is non empty integer-valued positive-yielding Chinese_Remainder FinSequence;
end;

registration
cluster V1() Function-like non empty FinSequence-like integer-yielding positive-yielding Chinese_Remainder -> non multiplicative-trivial set ;
coherence
for b1 being CR_Sequence holds not b1 is multiplicative-trivial
proof end;
end;

registration
cluster V1() multiplicative-trivial Function-like FinSequence-like integer-valued -> non empty integer-valued set ;
coherence
for b1 being integer-valued FinSequence st b1 is multiplicative-trivial holds
not b1 is empty
;
end;

theorem Th24: :: INT_6:24
for f being CR_Sequence
for m being natural number st 0 < m & m <= len f holds
f | m is CR_Sequence
proof end;

Lm7: for m being CR_Sequence holds Product m > 0
proof end;

registration
let m be CR_Sequence;
cluster Product m -> natural positive ;
coherence
( Product m is positive & Product m is natural )
proof end;
end;

theorem Th25: :: INT_6:25
for m being CR_Sequence
for i being natural number st i in dom m holds
for mm being Integer st mm = (Product m) / (m . i) holds
mm,m . i are_relative_prime
proof end;

Lm8: for u being integer-yielding FinSequence
for m being CR_Sequence
for z1, z2 being Integer st 0 <= z1 & z1 < Product m & ( for i being natural number st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being natural number st i in dom m holds
z2,u . i are_congruent_mod m . i ) holds
z1 = z2
proof end;

begin

definition
let u be Integer;
let m be integer-valued FinSequence;
func mod (u,m) -> FinSequence means :Def3: :: INT_6:def 3
( len it = len m & ( for i being natural number st i in dom it holds
it . i = u mod (m . i) ) );
existence
ex b1 being FinSequence st
( len b1 = len m & ( for i being natural number st i in dom b1 holds
b1 . i = u mod (m . i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence st len b1 = len m & ( for i being natural number st i in dom b1 holds
b1 . i = u mod (m . i) ) & len b2 = len m & ( for i being natural number st i in dom b2 holds
b2 . i = u mod (m . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines mod INT_6:def 3 :
for u being Integer
for m being integer-valued FinSequence
for b3 being FinSequence holds
( b3 = mod (u,m) iff ( len b3 = len m & ( for i being natural number st i in dom b3 holds
b3 . i = u mod (m . i) ) ) );

registration
let u be Integer;
let m be integer-valued FinSequence;
cluster mod (u,m) -> integer-valued ;
coherence
mod (u,m) is integer-yielding
proof end;
end;

definition
let m be CR_Sequence;
mode CR_coefficients of m -> FinSequence means :Def4: :: INT_6:def 4
( len it = len m & ( for i being natural number st i in dom it holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & it . i = s * ((Product m) / (m . i)) ) ) );
existence
ex b1 being FinSequence st
( len b1 = len m & ( for i being natural number st i in dom b1 holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & b1 . i = s * ((Product m) / (m . i)) ) ) )
proof end;
end;

:: deftheorem Def4 defines CR_coefficients INT_6:def 4 :
for m being CR_Sequence
for b2 being FinSequence holds
( b2 is CR_coefficients of m iff ( len b2 = len m & ( for i being natural number st i in dom b2 holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & b2 . i = s * ((Product m) / (m . i)) ) ) ) );

registration
let m be CR_Sequence;
cluster -> integer-valued CR_coefficients of m;
coherence
for b1 being CR_coefficients of m holds b1 is integer-yielding
proof end;
end;

theorem Th26: :: INT_6:26
for m being CR_Sequence
for c being CR_coefficients of m
for i being natural number st i in dom c holds
c . i,1 are_congruent_mod m . i
proof end;

theorem Th27: :: INT_6:27
for m being CR_Sequence
for c being CR_coefficients of m
for i, j being natural number st i in dom c & j in dom c & i <> j holds
c . i, 0 are_congruent_mod m . j
proof end;

theorem :: INT_6:28
for m being CR_Sequence
for c1, c2 being CR_coefficients of m
for i being natural number st i in dom c1 holds
c1 . i,c2 . i are_congruent_mod m . i
proof end;

theorem Th29: :: INT_6:29
for u being integer-valued FinSequence
for m being CR_Sequence st len m = len u holds
for c being CR_coefficients of m
for i being natural number st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i
proof end;

theorem Th30: :: INT_6:30
for u being integer-valued FinSequence
for m being CR_Sequence st len m = len u holds
for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
proof end;

definition
let u be integer-valued FinSequence;
let m be CR_Sequence;
assume A1: len m = len u ;
func to_int (u,m) -> Integer means :Def5: :: INT_6:def 5
for c being CR_coefficients of m holds it = (Sum (u (#) c)) mod (Product m);
existence
ex b1 being Integer st
for c being CR_coefficients of m holds b1 = (Sum (u (#) c)) mod (Product m)
proof end;
uniqueness
for b1, b2 being Integer st ( for c being CR_coefficients of m holds b1 = (Sum (u (#) c)) mod (Product m) ) & ( for c being CR_coefficients of m holds b2 = (Sum (u (#) c)) mod (Product m) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines to_int INT_6:def 5 :
for u being integer-valued FinSequence
for m being CR_Sequence st len m = len u holds
for b3 being Integer holds
( b3 = to_int (u,m) iff for c being CR_coefficients of m holds b3 = (Sum (u (#) c)) mod (Product m) );

theorem Th31: :: INT_6:31
for u being integer-valued FinSequence
for m being CR_Sequence st len m = len u holds
( 0 <= to_int (u,m) & to_int (u,m) < Product m )
proof end;

theorem Th32: :: INT_6:32
for u being Integer
for m being CR_Sequence
for i being natural number st i in dom m holds
u,(mod (u,m)) . i are_congruent_mod m . i
proof end;

theorem Th33: :: INT_6:33
for u, v being Integer
for m being CR_Sequence
for i being natural number st i in dom m holds
((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i
proof end;

Lm9: for u, v being Integer
for m being CR_Sequence
for i being natural number st i in dom m holds
((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i
proof end;

theorem Th34: :: INT_6:34
for u, v being Integer
for m being CR_Sequence
for i being natural number st i in dom m holds
((mod (u,m)) (#) (mod (v,m))) . i,u * v are_congruent_mod m . i
proof end;

theorem Th35: :: INT_6:35
for u, v being Integer
for m being CR_Sequence
for i being natural number st i in dom m holds
to_int (((mod (u,m)) + (mod (v,m))),m),u + v are_congruent_mod m . i
proof end;

theorem Th36: :: INT_6:36
for u, v being Integer
for m being CR_Sequence
for i being natural number st i in dom m holds
to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i
proof end;

theorem Th37: :: INT_6:37
for u, v being Integer
for m being CR_Sequence
for i being natural number st i in dom m holds
to_int (((mod (u,m)) (#) (mod (v,m))),m),u * v are_congruent_mod m . i
proof end;

theorem :: INT_6:38
for u, v being Integer
for m being CR_Sequence st 0 <= u + v & u + v < Product m holds
to_int (((mod (u,m)) + (mod (v,m))),m) = u + v
proof end;

theorem :: INT_6:39
for u, v being Integer
for m being CR_Sequence st 0 <= u - v & u - v < Product m holds
to_int (((mod (u,m)) - (mod (v,m))),m) = u - v
proof end;

theorem :: INT_6:40
for u, v being Integer
for m being CR_Sequence st 0 <= u * v & u * v < Product m holds
to_int (((mod (u,m)) (#) (mod (v,m))),m) = u * v
proof end;

begin

theorem :: INT_6:41
for u being integer-valued FinSequence
for m being CR_Sequence st len u = len m holds
ex z being Integer st
( 0 <= z & z < Product m & ( for i being natural number st i in dom u holds
z,u . i are_congruent_mod m . i ) )
proof end;

theorem :: INT_6:42
for u being integer-valued FinSequence
for m being CR_Sequence
for z1, z2 being Integer st 0 <= z1 & z1 < Product m & ( for i being natural number st i in dom m holds
z1,u . i are_congruent_mod m . i ) & 0 <= z2 & z2 < Product m & ( for i being natural number st i in dom m holds
z2,u . i are_congruent_mod m . i ) holds
z1 = z2 by Lm8;