:: by Christoph Schwarzweller

::

:: Received May 13, 2008

:: Copyright (c) 2008-2016 Association of Mizar Users

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

proof end;

registration
end;

registration
end;

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

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

Product F is integer

end;
coherence

Sum F is integer

proof end;

coherence Product F is integer

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

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

( i in dom f & f . i = 0 ) holds

Product f = 0

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

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

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

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

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

x,y are_congruent_mod i * j

proof end;

definition

let f be INT -valued FinSequence;

( not f is multiplicative-trivial iff for i being Nat holds

( not i in dom f or not f . i = 0 ) ) ;

end;
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 for i being Nat holds

( not i in dom f or not f . i = 0 );

( not f is multiplicative-trivial iff for i being Nat holds

( not i in dom f or not f . i = 0 ) ) ;

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

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

ex b_{1} being INT -valued FinSequence st b_{1} is multiplicative-trivial

not for b_{1} being INT -valued FinSequence holds b_{1} is multiplicative-trivial
by Def1;

ex b_{1} being INT -valued FinSequence st

( not b_{1} is empty & b_{1} is positive-yielding )
end;

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

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

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

( not b

proof end;

definition

let f be INT -valued FinSequence;

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

for i, j being Nat st i in dom f & j in dom f & i <> j holds

f . i,f . j are_coprime ;

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

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

ex b_{1} being INT -valued FinSequence st

( not b_{1} is empty & b_{1} is positive-yielding & b_{1} is Chinese_Remainder )
end;

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

( not b

proof end;

definition
end;

registration

for b_{1} being CR_Sequence holds not b_{1} is multiplicative-trivial
end;

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

coherence for b

proof end;

registration

for b_{1} being INT -valued FinSequence st b_{1} is multiplicative-trivial holds

not b_{1} is empty
;

end;

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

coherence for b

not b

Lm8: for m being CR_Sequence holds Product m > 0

proof end;

registration
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

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;

ex b_{1} being FinSequence st

( len b_{1} = len m & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = u mod (m . i) ) )

for b_{1}, b_{2} being FinSequence st len b_{1} = len m & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = u mod (m . i) ) & len b_{2} = len m & ( for i being Nat st i in dom b_{2} holds

b_{2} . i = u mod (m . i) ) holds

b_{1} = b_{2}

end;
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 ( len it = len m & ( for i being Nat st i in dom it holds

it . i = u mod (m . i) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines mod INT_6:def 3 :

for u being Integer

for m being INT -valued FinSequence

for b_{3} being FinSequence holds

( b_{3} = mod (u,m) iff ( len b_{3} = len m & ( for i being Nat st i in dom b_{3} holds

b_{3} . i = u mod (m . i) ) ) );

for u being Integer

for m being INT -valued FinSequence

for b

( b

b

registration
end;

definition

let m be CR_Sequence;

ex b_{1} being FinSequence st

( len b_{1} = len m & ( for i being Nat st i in dom b_{1} holds

ex s, mm being Integer st

( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & b_{1} . i = s * ((Product m) / (m . i)) ) ) )

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

ex b

( len b

ex s, mm being Integer st

( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & b

proof end;

:: deftheorem Def4 defines CR_coefficients INT_6:def 4 :

for m being CR_Sequence

for b_{2} being FinSequence holds

( b_{2} is CR_coefficients of m iff ( len b_{2} = len m & ( for i being Nat st i in dom b_{2} holds

ex s, mm being Integer st

( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & b_{2} . i = s * ((Product m) / (m . i)) ) ) ) );

for m being CR_Sequence

for b

( b

ex s, mm being Integer st

( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & b

registration

let m be CR_Sequence;

coherence

for b_{1} being CR_coefficients of m holds b_{1} is INT -valued

end;
coherence

for b

proof 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

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

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

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

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

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 ;

ex b_{1} being Integer st

for c being CR_coefficients of m holds b_{1} = (Sum (u (#) c)) mod (Product m)

for b_{1}, b_{2} being Integer st ( for c being CR_coefficients of m holds b_{1} = (Sum (u (#) c)) mod (Product m) ) & ( for c being CR_coefficients of m holds b_{2} = (Sum (u (#) c)) mod (Product m) ) holds

b_{1} = b_{2}

end;
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 for c being CR_coefficients of m holds it = (Sum (u (#) c)) mod (Product m);

ex b

for c being CR_coefficients of m holds b

proof end;

uniqueness for b

b

proof 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_{3} being Integer holds

( b_{3} = to_int (u,m) iff for c being CR_coefficients of m holds b_{3} = (Sum (u (#) c)) mod (Product m) );

for u being INT -valued FinSequence

for m being CR_Sequence st len m = len u holds

for b

( b

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 )

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

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

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

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

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

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

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

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

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

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

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;

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;