:: Modular Integer Arithmetic
:: by Christoph Schwarzweller
::
:: Copyright (c) 2008-2019 Association of Mizar Users

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

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

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

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

registration
let i be Integer;
coherence
proof end;
end;

registration
let f, g be INT -valued FinSequence;
cluster f ^ g -> INT -valued ;
coherence
f ^ g is INT -valued
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 Nat st k <= len m1 holds
(m1 (#) m2) | k = (m1 | k) (#) (m2 | k)
proof end;

registration
let F be INT -valued FinSequence;
coherence
Sum F is integer
proof end;
coherence
proof end;
end;

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

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

theorem Th6: :: INT_6:6
for f being complex-valued FinSequence st ex i being Nat 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 INT -valued FinSequence
for i being Nat st i in dom m & m . i <> 0 holds
() / (m . i) is Integer
proof end;

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

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

proof end;

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

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

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

theorem Th14: :: INT_6:14
for i, j being Integer holds i gcd j = i gcd |.j.|
proof end;

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

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

theorem Th17: :: INT_6:17
for i, j being Integer holds (i * j) gcd i = |.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_coprime holds
i gcd (j * k) = i gcd k
proof end;

theorem Th20: :: INT_6:20
for i, j being Integer st i,j are_coprime 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_coprime & 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_coprime holds
ex s being Integer st s * i,1 are_congruent_mod j
proof end;

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

Lm7: for u being object st u in {1} holds
u in INT

by INT_1:def 1;

registration
existence
ex b1 being INT -valued FinSequence st b1 is multiplicative-trivial
proof end;
existence
not for b1 being INT -valued FinSequence holds b1 is multiplicative-trivial
by Def1;
existence
ex b1 being INT -valued FinSequence st
( not b1 is empty & b1 is positive-yielding )
proof end;
end;

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

definition
let f be INT -valued FinSequence;
attr f is Chinese_Remainder means :Def2: :: INT_6:def 2
for i, j being Nat st i in dom f & j in dom f & i <> j holds
f . i,f . j are_coprime ;
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 & j in dom f & i <> j holds
f . i,f . j are_coprime );

registration
existence
ex b1 being INT -valued FinSequence st
( not b1 is empty & b1 is positive-yielding & b1 is Chinese_Remainder )
proof end;
end;

definition end;

registration
coherence
for b1 being CR_Sequence holds not b1 is multiplicative-trivial
proof end;
end;

registration
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 & m <= len f holds
f | m is CR_Sequence
proof end;

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

registration
let m be CR_Sequence;
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 Nat st i in dom m holds
for mm being Integer st mm = () / (m . i) holds
mm,m . i are_coprime
proof end;

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

proof end;

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 & ( 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 & ( for i being Nat 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 Nat st i in dom b1 holds
b1 . i = u mod (m . i) ) & len b2 = len m & ( for i being Nat 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 INT -valued FinSequence
for b3 being FinSequence holds
( b3 = mod (u,m) iff ( len b3 = len m & ( 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
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 Nat st i in dom it holds
ex s, mm being Integer st
( mm = () / (m . i) & s * mm,1 are_congruent_mod m . i & it . i = s * (() / (m . i)) ) ) );
existence
ex b1 being FinSequence st
( len b1 = len m & ( for i being Nat st i in dom b1 holds
ex s, mm being Integer st
( mm = () / (m . i) & s * mm,1 are_congruent_mod m . i & b1 . i = s * (() / (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 Nat st i in dom b2 holds
ex s, mm being Integer st
( mm = () / (m . i) & s * mm,1 are_congruent_mod m . i & b2 . i = s * (() / (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
proof end;
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
proof end;

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 & 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 Nat 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 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
proof end;

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

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 ();
existence
ex b1 being Integer st
for c being CR_coefficients of m holds b1 = (Sum (u (#) c)) mod ()
proof end;
uniqueness
for b1, b2 being Integer st ( for c being CR_coefficients of m holds b1 = (Sum (u (#) c)) mod () ) & ( for c being CR_coefficients of m holds b2 = (Sum (u (#) c)) mod () ) holds
b1 = b2
proof end;
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 () );

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) & 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 Nat 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 Nat st i in dom m holds
((mod (u,m)) + (mod (v,m))) . i,u + v are_congruent_mod m . i
proof end;

Lm10: 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

proof end;

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

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

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

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

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 & z < Product m & ( for i being Nat st i in dom u holds
z,u . i are_congruent_mod m . i ) )
proof end;

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