:: The Chinese Remainder Theorem
:: by Andrzej Kondracki
::
:: Received December 30, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

theorem Th1: :: WSIERP_1:1
for x being real number holds
( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 )
proofend;

theorem Th2: :: WSIERP_1:2
for x being real number
for a being Nat holds
( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) )
proofend;

theorem Th3: :: WSIERP_1:3
for x, y being real number
for d being Nat st x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d holds
x = y
proofend;

Lm1:  for x, y being real number holds
( ( x >= 0 implies x + y >= y ) & ( x + y >= y implies x >= 0 ) & ( x > 0 implies x + y > y ) & ( x + y > y implies x > 0 ) & ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) )
proofend;

Lm2:  for x, y, z being real number st x >= 0 & y >= z holds
( x + y >= z & y >= z - x )
proofend;

Lm3:  for x, y, z being real number st ( ( x >= 0 & y > z ) or ( x > 0 & y >= z ) ) holds
( x + y > z & y > z - x )
proofend;

registration
let k be Integer;
let a be Nat;
clusterk |^ a ->  integer ;
coherence
 k |^ a is integer
proofend;
end;

Lm4:  for a being Nat ex b being Nat st
( a = 2 * b or a = (2 * b) + 1 )
proofend;

theorem Th4: :: WSIERP_1:4
for k, m, n being Integer st k divides m & k divides n holds
k divides m + n
proofend;

theorem Th5: :: WSIERP_1:5
for k, m, n, m1, n1 being Integer st k divides m & k divides n holds
k divides (m * m1) + (n * n1)
proofend;

theorem Th6: :: WSIERP_1:6
for m, n, k being Integer st m gcd n = 1 & k gcd n = 1 holds
(m * k) gcd n = 1
proofend;

theorem :: WSIERP_1:7
for a, b, c being Nat st a gcd b = 1 & c gcd b = 1 holds
(a * c) gcd b = 1 by Th6;

theorem Th8: :: WSIERP_1:8
for m being Integer holds
( 0 gcd m = abs m & 1 gcd m = 1 )
proofend;

theorem Th9: :: WSIERP_1:9
for k being Integer holds 1,k are_relative_prime
proofend;

theorem Th10: :: WSIERP_1:10
for a being Nat
for k, l being Integer st k,l are_relative_prime holds
k |^ a,l are_relative_prime
proofend;

theorem Th11: :: WSIERP_1:11
for a, b being Nat
for k, l being Integer st k,l are_relative_prime holds
k |^ a,l |^ b are_relative_prime
proofend;

theorem Th12: :: WSIERP_1:12
for b, a being Nat
for k, l being Integer st k gcd l = 1 holds
( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 )
proofend;

theorem :: WSIERP_1:13
for m, k being Integer holds
( abs m divides k iff m divides k )
proofend;

theorem Th14: :: WSIERP_1:14
for a, b, c being Nat st a divides b holds
a |^ c divides b |^ c
proofend;

theorem Th15: :: WSIERP_1:15
for a being Nat st a divides 1 holds
a = 1
proofend;

theorem :: WSIERP_1:16
for d, a, b being Nat st d divides a & a gcd b = 1 holds
d gcd b = 1 by Th15, NEWTON:57;

Lm5:  for a, b being Nat st a <> 0 holds
( a divides b iff b / a is Element of NAT )
proofend;

theorem Th17: :: WSIERP_1:17
for k, l being Integer st k <> 0 holds
( k divides l iff l / k is Integer )
proofend;

Lm6:  for b, a being Nat
for k being Integer st b <> 0 &amp; a * k = b holds
k is Element of NAT
proofend;

Lm7:  for a, b, c being Nat st a + b <= c holds
( a <= c &amp; b <= c )
proofend;

theorem :: WSIERP_1:18
for a, b, c being Nat st a <= b - c holds
( a <= b &amp; c <= b )
proofend;

Lm8:  for k, m being Integer holds
( k < m iff k <= m - 1 )
proofend;

Lm9:  for k, m being Integer holds
( k < m + 1 iff k <= m )
proofend;

definition
let D be non empty set ;
let D1 be non empty Subset of D;
let f1, f2 be FinSequence of D1;
:: original:^
redefine funcf1 ^ f2 ->  FinSequence of D1;
coherence
 f1 ^ f2 is FinSequence of D1
proofend;
end;

registration
let fr be FinSequence of INT ;
cluster Product fr ->  integer ;
coherence
 Product fr is integer
proofend;
end;

definition
let fp be FinSequence of NAT ;
:: original:Sum
redefine func Sum fp ->  Element of NAT ;
coherence
 Sum fp is Element of NAT
proofend;
end;

definition
let fp be FinSequence of NAT ;
:: original:Product
redefine func Product fp ->  Element of NAT ;
coherence
 Product fp is Element of NAT
proofend;
end;

Lm10:  for a being Nat
for fs being FinSequence st a in dom fs holds
ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 &amp; len fs1 = a - 1 &amp; len fs2 = (len fs) - a )
proofend;

definition
let a be Nat;
let fs be FinSequence;
redefine func Del (fs,a) means :Def1: :: WSIERP_1:def 1
it = fs if  not a in dom fs
otherwise ( (len it) + 1 = len fs &amp; ( for b being Nat holds
( ( b < a implies it . b = fs . b ) &amp; ( b >= a implies it . b = fs . (b + 1) ) ) ) );
compatibility
 for b1 being set holds
( ( not a in dom fs implies ( b1 = Del (fs,a) iff b1 = fs ) ) &amp; ( a in dom fs implies ( b1 = Del (fs,a) iff ( (len b1) + 1 = len fs &amp; ( for b being Nat holds
( ( b < a implies b1 . b = fs . b ) &amp; ( b >= a implies b1 . b = fs . (b + 1) ) ) ) ) ) ) )
proofend;
correctness
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def1 defines Del WSIERP_1:def_1_:_
 for a being Nat
for fs being FinSequence
for b3 being set holds
( ( not a in dom fs implies ( b3 = Del (fs,a) iff b3 = fs ) ) &amp; ( a in dom fs implies ( b3 = Del (fs,a) iff ( (len b3) + 1 = len fs &amp; ( for b being Nat holds
( ( b < a implies b3 . b = fs . b ) &amp; ( b >= a implies b3 . b = fs . (b + 1) ) ) ) ) ) ) );

Lm11:  for a being Nat
for fs, fs1, fs2 being FinSequence
for v being set st a in dom fs &amp; fs = (fs1 ^ <*v*>) ^ fs2 &amp; len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2
proofend;

Lm12:  for a being Nat
for fs being FinSequence holds dom (Del (fs,a)) c= dom fs
proofend;

definition
let D be non empty set ;
let a be Nat;
let fs be FinSequence of D;
:: original:Del
redefine func Del (fs,a) ->  FinSequence of D;
coherence
 Del (fs,a) is FinSequence of D
proofend;
end;

definition
let D be non empty set ;
let D1 be non empty Subset of D;
let a be Nat;
let fs be FinSequence of D1;
:: original:Del
redefine func Del (fs,a) ->  FinSequence of D1;
coherence
 Del (fs,a) is FinSequence of D1
proofend;
end;

Lm13:  for a being Nat
for fs1, fs2 being FinSequence holds
( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) &amp; ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) )
proofend;

Lm14:  for fs being FinSequence
for v being set holds
( Del ((<*v*> ^ fs),1) = fs &amp; Del ((fs ^ <*v*>),((len fs) + 1)) = fs )
proofend;

theorem :: WSIERP_1:19
for v1, v2, v3 being set holds
( Del (<*v1*>,1) = {} &amp; Del (<*v1,v2*>,1) = <*v2*> &amp; Del (<*v1,v2*>,2) = <*v1*> &amp; Del (<*v1,v2,v3*>,1) = <*v2,v3*> &amp; Del (<*v1,v2,v3*>,2) = <*v1,v3*> &amp; Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
proofend;

Lm15:  for fs being FinSequence st 1 <= len fs holds
( fs = <*(fs . 1)*> ^ (Del (fs,1)) &amp; fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> )
proofend;

Lm16:  for a being Nat
for ft being FinSequence of REAL st a in dom ft holds
(Product (Del (ft,a))) * (ft . a) = Product ft
proofend;

theorem :: WSIERP_1:20
for a being Nat
for ft being FinSequence of REAL st a in dom ft holds
(Sum (Del (ft,a))) + (ft . a) = Sum ft
proofend;

theorem :: WSIERP_1:21
for a being Nat
for fp being FinSequence of NAT st a in dom fp holds
(Product fp) / (fp . a) is Element of NAT
proofend;

:: BEGINING
theorem Th22: :: WSIERP_1:22
for q being Rational holds numerator q, denominator q are_relative_prime
proofend;

theorem :: WSIERP_1:23
for a being Nat
for k being Integer
for q being Rational st q = k / a &amp; a <> 0 &amp; k,a are_relative_prime holds
( k = numerator q &amp; a = denominator q )
proofend;

theorem Th24: :: WSIERP_1:24
for a, b being Nat st ex q being Rational st a = q |^ b holds
ex k being Integer st a = k |^ b
proofend;

theorem Th25: :: WSIERP_1:25
for a, d being Nat st ex q being Rational st a = q |^ d holds
ex b being Nat st a = b |^ d
proofend;

theorem :: WSIERP_1:26
for e, a, b being Nat st e > 0 &amp; a |^ e divides b |^ e holds
a divides b
proofend;

theorem Th27: :: WSIERP_1:27
for a, b being Nat ex m, n being Integer st a gcd b = (a * m) + (b * n)
proofend;

theorem Th28: :: WSIERP_1:28
for m, n being Integer ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)
proofend;

theorem Th29: :: WSIERP_1:29
for m, n, k being Integer st m divides n * k &amp; m gcd n = 1 holds
m divides k
proofend;

theorem :: WSIERP_1:30
for a, b, c being Nat st a gcd b = 1 &amp; a divides b * c holds
a divides c by Th29;

theorem Th31: :: WSIERP_1:31
for a, b being Nat st a <> 0 &amp; b <> 0 holds
ex c, d being Nat st a gcd b = (a * c) - (b * d)
proofend;

theorem :: WSIERP_1:32
for f, g, a, b being Nat st f > 0 &amp; g > 0 &amp; f gcd g = 1 &amp; a |^ f = b |^ g holds
ex e being Nat st
( a = e |^ g &amp; b = e |^ f )
proofend;

theorem Th33: :: WSIERP_1:33
for m, n, k being Integer holds
( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k )
proofend;

theorem :: WSIERP_1:34
for m, n, m1, n1, k being Integer st m <> 0 &amp; n <> 0 &amp; (m * m1) + (n * n1) = k holds
for x, y being Integer st (m * x) + (n * y) = k holds
ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) &amp; y = n1 - (t * (m / (m gcd n))) )
proofend;

theorem :: WSIERP_1:35
for a, b, c, d being Nat st a gcd b = 1 &amp; a * b = c |^ d holds
ex e, f being Nat st
( a = e |^ d &amp; b = f |^ d )
proofend;

:: Chinese remainder theorem
:: [WP: ] Chinese_Remainder_Theorem
theorem Th36: :: WSIERP_1:36
for fp being FinSequence of NAT
for d being Nat st ( for a being Nat st a in dom fp holds
(fp . a) gcd d = 1 ) holds
(Product fp) gcd d = 1
proofend;

theorem :: WSIERP_1:37
for fp being FinSequence of NAT st len fp >= 2 &amp; ( for b, c being Nat st b in dom fp &amp; c in dom fp &amp; b <> c holds
(fp . b) gcd (fp . c) = 1 ) holds
for fr being FinSequence of INT st len fr = len fp holds
ex fr1 being FinSequence of INT st
( len fr1 = len fp &amp; ( for b being Nat st b in dom fp holds
((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) )
proofend;

Lm17:  for k, m being Integer holds
( k divides m iff k divides abs m )
proofend;

Lm18:  for m, n being Integer holds (m * n) mod n = 0
proofend;

Lm19:  for k, n, m being Integer st k mod n = m mod n holds
(k - m) mod n = 0
proofend;

Lm20:  for n, m being Integer st n <> 0 &amp; m mod n = 0 holds
n divides m
proofend;

Lm21:  for x being Integer holds
( ( 1 < x implies ( 1 < sqrt x &amp; sqrt x < x ) ) &amp; ( 0 < x &amp; x < 1 implies ( 0 < sqrt x &amp; sqrt x < 1 &amp; x < sqrt x ) ) )
proofend;

:: [WP: ] Thue_Theorem
theorem :: WSIERP_1:38
for a being Nat
for k being Integer st a <> 0 &amp; a gcd k = 1 holds
ex b, e being Nat st
( 0 <> b &amp; 0 <> e &amp; b <= sqrt a &amp; e <= sqrt a &amp; ( a divides (k * b) + e or a divides (k * b) - e ) )
proofend;

theorem :: WSIERP_1:39
for a being Nat
for fs being FinSequence holds dom (Del (fs,a)) c= dom fs by Lm12;

theorem :: WSIERP_1:40
for fs being FinSequence
for v being set holds
( Del ((<*v*> ^ fs),1) = fs &amp; Del ((fs ^ <*v*>),((len fs) + 1)) = fs ) by Lm14;

begin

theorem :: WSIERP_1:41
for k being Integer
for n being Nat st n > 0 &amp; k mod n <> 0 holds
- (k div n) = ((- k) div n) + 1
proofend;

theorem :: WSIERP_1:42
for k being Integer
for n being Nat st n > 0 &amp; k mod n = 0 holds
- (k div n) = (- k) div n
proofend;