:: Modular Integer Arithmetic
:: by Christoph Schwarzweller
::
:: Received May 13, 2008
:: Copyright (c) 2008-2021 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;

cluster f | n -> complex-valued ;

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;

cluster <*i*> -> INT -valued ;

coherence
<*i*> is INT -valued

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;

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 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
(Product m) / (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) = (Product m) / (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
(Product m) / ((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) = (Product m) / (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

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

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

cluster Relation-like multiplicative-trivial omega -defined INT -valued Function-like V35() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued for set ;

existence
ex b₁ being INT -valued FinSequence st b₁ is multiplicative-trivial

proof end;

cluster Relation-like non multiplicative-trivial omega -defined INT -valued Function-like V35() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued for set ;

existence
not for b₁ being INT -valued FinSequence holds b₁ is multiplicative-trivial by Def1;

cluster Relation-like omega -defined INT -valued Function-like non empty V35() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding for set ;

existence
ex b₁ being INT -valued FinSequence st
( not b₁ is empty & b₁ 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

cluster Relation-like omega -defined INT -valued Function-like non empty V35() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued positive-yielding Chinese_Remainder for set ;

existence
ex b₁ being INT -valued FinSequence st
( not b₁ is empty & b₁ is positive-yielding & b₁ is Chinese_Remainder )

proof end;

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 b₁ being CR_Sequence holds not b₁ is multiplicative-trivial

proof end;

end;

registration

cluster Relation-like multiplicative-trivial INT -valued Function-like FinSequence-like -> INT -valued non empty for set ;

coherence
for b₁ being INT -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 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;

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 Nat st i in dom m holds
for mm being Integer st mm = (Product m) / (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 b₁ being FinSequence st
( len b₁ = len m & ( for i being Nat 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 Nat st i in dom b₁ holds
b₁ . i = u mod (m . i) ) & len b₂ = len m & ( for i being Nat 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 INT -valued FinSequence
for b₃ being FinSequence holds
( b₃ = mod (u,m) iff ( len b₃ = len m & ( for i being Nat st i in dom b₃ holds
b₃ . 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 = (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 Nat 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 Nat 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 -> INT -valued for CR_coefficients of m;

coherence
for b₁ being CR_coefficients of m holds b₁ 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 (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 INT -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 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;