:: 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 b₁ being integer-valued FinSequence st b₁ 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 b₁ being integer-valued FinSequence holds b₁ 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 b₁ being integer-valued FinSequence st
( not b₁ is empty & b₁ 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 b₁ being integer-valued FinSequence st
( not b₁ is empty & b₁ is positive-yielding & b₁ 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 b₁ being CR_Sequence holds not b₁ is multiplicative-trivial

proof end;

end;

registration

cluster V1() multiplicative-trivial Function-like FinSequence-like integer-valued -> non empty integer-valued set ;
coherence
for b₁ being integer-valued FinSequence st b₁ is multiplicative-trivial holds
not b₁ 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 b₁ being FinSequence st
( len b₁ = len m & ( for i being natural number st i in dom b₁ holds
b₁ . i = u mod (m . i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st len b₁ = len m & ( for i being natural number st i in dom b₁ holds
b₁ . i = u mod (m . i) ) & len b₂ = len m & ( for i being natural number st i in dom b₂ holds
b₂ . i = u mod (m . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines mod INT_6:def 3 :
for u being Integer
for m being integer-valued FinSequence
for b₃ being FinSequence holds
( b₃ = mod (u,m) iff ( len b₃ = len m & ( for i being natural number st i in dom b₃ holds
b₃ . 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 b₁ being FinSequence st
( len b₁ = len m & ( for i being natural number st i in dom b₁ holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & b₁ . i = s * ((Product m) / (m . i)) ) ) )

proof end;

end;

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

registration

let m be CR_Sequence;
cluster -> integer-valued CR_coefficients of m;
coherence
for b₁ being CR_coefficients of m holds b₁ 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 b₁ being Integer st
for c being CR_coefficients of m holds b₁ = (Sum (u (#) c)) mod (Product m)

proof end;

uniqueness
for b₁, b₂ being Integer st ( for c being CR_coefficients of m holds b₁ = (Sum (u (#) c)) mod (Product m) ) & ( for c being CR_coefficients of m holds b₂ = (Sum (u (#) c)) mod (Product m) ) holds
b₁ = b₂

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 b₃ being Integer holds
( b₃ = to_int (u,m) iff for c being CR_coefficients of m holds b₃ = (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;