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


begin

Lm1:  for f being INT -valued FinSequence holds f is FinSequence of INT
proofend;

registration
let f be complex-valued FinSequence;
let n be Nat;
clusterf | n ->  complex-valued ;
coherence
 f | n is complex-valued ;
end;

registration
let f be INT -valued FinSequence;
let n be Nat;
clusterf | n ->  INT -valued ;
coherence
 f | n is INT -valued ;
end;

registration
let f be INT -valued FinSequence;
let n be Nat;
clusterf /^ n ->  INT -valued ;
coherence
 f /^ n is INT -valued
proofend;
end;

registration
let i be Integer;
cluster<*i*> ->  INT -valued ;
coherence
 <*i*> is INT -valued
proofend;
end;

registration
let f, g be INT -valued FinSequence;
clusterf ^ g ->  INT -valued ;
coherence
 f ^ g is INT -valued
proofend;
end;

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

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

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

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

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

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

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

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

Lm5:  for z being INT -valued FinSequence holds z is FinSequence of REAL
proofend;

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

theorem Th6: :: INT_6:6
for f being complex-valued FinSequence st ex i being Nat st
( i in dom f &amp; f . i = 0 ) holds
Product f = 0
proofend;

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

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

theorem Th9: :: INT_6:9
for m being INT -valued FinSequence
for i being Nat st i in dom m &amp; m . i <> 0 holds
(Product m) / (m . i) is Integer
proofend;

theorem Th10: :: INT_6:10
for m being INT -valued FinSequence
for i being Nat st i in dom m holds
ex z being Integer st z * (m . i) = Product m
proofend;

Lm6:  for m being INT -valued FinSequence
for i, j being Nat st i in dom m &amp; j in dom m &amp; j <> i &amp; m . j <> 0 holds
ex z being Integer st z * (m . i) = (Product m) / (m . j)
proofend;

theorem :: INT_6:11
for m being INT -valued FinSequence
for i, j being Nat st i in dom m &amp; j in dom m &amp; j <> i &amp; m . j <> 0 holds
(Product m) / ((m . i) * (m . j)) is Integer
proofend;

theorem :: INT_6:12
for m being INT -valued FinSequence
for i, j being Nat st i in dom m &amp; j in dom m &amp; j <> i &amp; 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 &amp; i divides abs i )
proofend;

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

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

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

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

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

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

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

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

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

begin

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

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

:: deftheorem Def1 defines multiplicative-trivial INT_6:def_1_:_
 for f being INT -valued FinSequence holds
( not f is multiplicative-trivial iff for i being Nat holds
( not i in dom f or not f . i = 0 ) );

registration
cluster Relation-like multiplicative-trivial NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued for set ;
existence
 ex b1 being INT -valued FinSequence st b1 is multiplicative-trivial
proofend;
cluster Relation-like non multiplicative-trivial NAT -defined INT -valued Function-like V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued for set ;
existence
 not for b1 being INT -valued FinSequence holds b1 is multiplicative-trivial by Def1;
cluster Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding for set ;
existence
 ex b1 being INT -valued FinSequence st
( not b1 is empty &amp; b1 is positive-yielding )
proofend;
end;

theorem :: INT_6:23
for m being multiplicative-trivial INT -valued FinSequence holds Product m = 0
proofend;

definition
let f be INT -valued FinSequence;
attrf is Chinese_Remainder  means :Def2: :: INT_6:def 2
 for i, j being Nat st i in dom f &amp; j in dom f &amp; i <> j holds
f . i,f . j are_relative_prime ;
end;

:: deftheorem Def2 defines Chinese_Remainder INT_6:def_2_:_
 for f being INT -valued FinSequence holds
( f is Chinese_Remainder iff for i, j being Nat st i in dom f &amp; j in dom f &amp; i <> j holds
f . i,f . j are_relative_prime );

registration
cluster Relation-like NAT -defined INT -valued Function-like non empty V32() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding Chinese_Remainder for set ;
existence
 ex b1 being INT -valued FinSequence st
( not b1 is empty &amp; b1 is positive-yielding &amp; b1 is Chinese_Remainder )
proofend;
end;

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

registration
cluster Relation-like INT -valued Function-like non empty FinSequence-like positive-yielding Chinese_Remainder  ->  non multiplicative-trivial for set ;
coherence
 for b1 being CR_Sequence holds not b1 is multiplicative-trivial
proofend;
end;

registration
cluster Relation-like multiplicative-trivial INT -valued Function-like FinSequence-like  ->  INT -valued non empty for set ;
coherence
 for b1 being INT -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 Nat st 0 < m &amp; m <= len f holds
f | m is CR_Sequence
proofend;

Lm7:  for m being CR_Sequence holds Product m > 0
proofend;

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

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

Lm8:  for u being INT -valued FinSequence
for m being CR_Sequence
for z1, z2 being Integer st 0 <= z1 &amp; z1 < Product m &amp; ( for i being Nat st i in dom m holds
z1,u . i are_congruent_mod m . i ) &amp; 0 <= z2 &amp; z2 < Product m &amp; ( for i being Nat st i in dom m holds
z2,u . i are_congruent_mod m . i ) holds
z1 = z2
proofend;

begin

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

:: deftheorem Def3 defines mod INT_6:def_3_:_
 for u being Integer
for m being INT -valued FinSequence
for b3 being FinSequence holds
( b3 = mod (u,m) iff ( len b3 = len m &amp; ( for i being Nat st i in dom b3 holds
b3 . i = u mod (m . i) ) ) );

registration
let u be Integer;
let m be INT -valued FinSequence;
cluster mod (u,m) ->  INT -valued ;
coherence
 mod (u,m) is INT -valued
proofend;
end;

definition
let m be CR_Sequence;
mode CR_coefficients of m ->  FinSequence means :Def4: :: INT_6:def 4
( len it = len m &amp; ( for i being Nat st i in dom it holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) &amp; s * mm,1 are_congruent_mod m . i &amp; it . i = s * ((Product m) / (m . i)) ) ) );
existence
 ex b1 being FinSequence st
( len b1 = len m &amp; ( for i being Nat st i in dom b1 holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) &amp; s * mm,1 are_congruent_mod m . i &amp; b1 . i = s * ((Product m) / (m . i)) ) ) )
proofend;
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 &amp; ( for i being Nat st i in dom b2 holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) &amp; s * mm,1 are_congruent_mod m . i &amp; b2 . i = s * ((Product m) / (m . i)) ) ) ) );

registration
let m be CR_Sequence;
cluster  ->  INT -valued for CR_coefficients of m;
coherence
 for b1 being CR_coefficients of m holds b1 is INT -valued
proofend;
end;

theorem Th26: :: INT_6:26
for m being CR_Sequence
for c being CR_coefficients of m
for i being Nat st i in dom c holds
c . i,1 are_congruent_mod m . i
proofend;

theorem Th27: :: INT_6:27
for m being CR_Sequence
for c being CR_coefficients of m
for i, j being Nat st i in dom c &amp; j in dom c &amp; i <> j holds
c . i, 0 are_congruent_mod m . j
proofend;

theorem :: INT_6:28
for m being CR_Sequence
for c1, c2 being CR_coefficients of m
for i being Nat st i in dom c1 holds
c1 . i,c2 . i are_congruent_mod m . i
proofend;

theorem Th29: :: INT_6:29
for u being INT -valued FinSequence
for m being CR_Sequence st len m = len u holds
for c being CR_coefficients of m
for i being Nat st i in dom m holds
Sum (u (#) c),u . i are_congruent_mod m . i
proofend;

theorem Th30: :: INT_6:30
for u being INT -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
proofend;

definition
let u be INT -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)
proofend;
uniqueness
 for b1, b2 being Integer st ( for c being CR_coefficients of m holds b1 = (Sum (u (#) c)) mod (Product m) ) &amp; ( for c being CR_coefficients of m holds b2 = (Sum (u (#) c)) mod (Product m) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines to_int INT_6:def_5_:_
 for u being INT -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 INT -valued FinSequence
for m being CR_Sequence st len m = len u holds
( 0 <= to_int (u,m) &amp; to_int (u,m) < Product m )
proofend;

theorem Th32: :: INT_6:32
for u being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
u,(mod (u,m)) . i are_congruent_mod m . i
proofend;

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

Lm9:  for u, v being Integer
for m being CR_Sequence
for i being Nat st i in dom m holds
((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i
proofend;

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

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

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

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

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

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

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

begin

theorem :: INT_6:41
for u being INT -valued FinSequence
for m being CR_Sequence st len u = len m holds
ex z being Integer st
( 0 <= z &amp; z < Product m &amp; ( for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i ) )
proofend;

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