:: Linear Congruence Relation and Complete Residue Systems
:: by Xiquan Liang , Li Yan and Junjie Zhao
::
:: Received August 28, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users


theorem Th1: :: INT_4:1
for X being real-membered set
for a being Real holds X,a ++ X are_equipotent
proof end;

registration
let X be finite real-membered set ;
let a be Real;
cluster K626(X,a) -> finite ;
coherence
a ++ X is finite by Th1, CARD_1:38;
end;

theorem Th2: :: INT_4:2
for X being real-membered set
for a being Real holds card X = card (a ++ X) by Th1, CARD_1:5;

Lm1: for a being Integer
for X being Subset of INT holds a ++ X c= INT
proof end;

Lm2: for a being Integer
for X being Subset of INT holds a ** X c= INT
proof end;

Lm3: for x being Integer
for X being Subset of INT
for a being Integer holds
( x in a ** X iff ex y being Integer st
( y in X & x = a * y ) )
proof end;

theorem Th3: :: INT_4:3
for X being real-membered set
for a being Real st a <> 0 holds
X,a ** X are_equipotent
proof end;

theorem Th4: :: INT_4:4
for X being real-membered set
for a being Real holds
( ( a = 0 & not X is empty implies a ** X = {0} ) & ( not a ** X = {0} or a = 0 or X = {0} ) )
proof end;

registration
let X be finite real-membered set ;
let a be Real;
cluster K632(X,a) -> finite ;
coherence
a ** X is finite
proof end;
end;

theorem Th5: :: INT_4:5
for X being real-membered set
for a being Real st a <> 0 holds
card X = card (a ** X) by Th3, CARD_1:5;

Lm4: for i1, i2, i3 being Integer st i1 divides i2 & i1 divides i3 holds
i1 divides i2 - i3
proof end;

Lm5: for a, b, i being Integer st i divides a & i divides a - b holds
i divides b
proof end;

Lm6: for p, n being Nat st p is prime & p,n are_coprime holds
not p divides n
proof end;

Lm7: for p being Nat st p > 0 holds
p >= 1 + 0
by NAT_1:13;

theorem Th6: :: INT_4:6
for i1, i being Integer st i divides i1 & i1 <> 0 holds
|.i.| <= |.i1.|
proof end;

theorem Th7: :: INT_4:7
for i1, i2, i3 being Integer st i3 <> 0 holds
( i1 divides i2 iff i1 * i3 divides i2 * i3 )
proof end;

theorem :: INT_4:8
for a, b, m being Nat
for n being Element of NAT st a mod m = b mod m holds
(a |^ n) mod m = (b |^ n) mod m
proof end;

theorem Th9: :: INT_4:9
for i1, i2, i3, i being Integer st i1 * i,i2 * i are_congruent_mod i3 & i,i3 are_coprime holds
i1,i2 are_congruent_mod i3
proof end;

theorem Th10: :: INT_4:10
for i1, i2, i3 being Integer
for k being Nat st i1,i2 are_congruent_mod i3 holds
i1 * k,i2 * k are_congruent_mod i3 * k
proof end;

theorem Th11: :: INT_4:11
for i1, i2, i3, i being Integer st i1,i2 are_congruent_mod i holds
i1 * i3,i2 * i3 are_congruent_mod i
proof end;

theorem :: INT_4:12
canceled;

Th12: for i being Integer holds 0 = 0 mod i
by INT_1:73;

theorem Th13: :: INT_4:13
for b being Integer st b > 0 holds
for a being Integer ex q, r being Integer st
( a = (b * q) + r & r >= 0 & r < b )
proof end;

theorem :: INT_4:14
canceled;

::$CT
theorem Th15: :: INT_4:15
for a, b, m being Integer st a,m are_coprime holds
ex x being Integer st ((a * x) - b) mod m = 0
proof end;

theorem Th16: :: INT_4:16
for a, b, m being Integer st m > 0 & a,m are_coprime holds
ex n being Nat st ((a * n) - b) mod m = 0
proof end;

theorem :: INT_4:17
for a, b, m being Integer st m <> 0 & not a gcd m divides b holds
for x being Integer holds not ((a * x) - b) mod m = 0
proof end;

theorem :: INT_4:18
for a, b, m being Integer st m <> 0 & a gcd m divides b holds
ex x being Integer st ((a * x) - b) mod m = 0
proof end;

theorem Th19: :: INT_4:19
for p, q, n being Nat st n > 0 & p > 0 holds
(p * q) mod (p |^ n) = p * (q mod (p |^ (n -' 1)))
proof end;

theorem :: INT_4:20
for p, q, n being Nat holds (p * q) mod (p * n) = p * (q mod n)
proof end;

theorem Th21: :: INT_4:21
for p, q, n being Nat st n > 0 & p is prime & p,q are_coprime holds
not p divides q mod (p |^ n)
proof end;

theorem Th22: :: INT_4:22
for p, q, n being Nat st n > 0 holds
( (p - q) mod n = 0 iff p mod n = q mod n )
proof end;

theorem :: INT_4:23
for a, b, m being Nat st m > 0 holds
( a mod m = b mod m iff m divides a - b )
proof end;

theorem :: INT_4:24
for p, q, n being Nat st n > 0 & p is prime & p,q are_coprime holds
for x being Integer holds not ((p * (x ^2)) - q) mod (p |^ n) = 0
proof end;

theorem :: INT_4:25
for p, q, n being Nat st n > 0 & p is prime & p,q are_coprime holds
for x being Integer holds not ((p * x) - q) mod (p |^ n) = 0
proof end;

definition
let m be Integer;
func Cong m -> Relation of INT means :Def1: :: INT_4:def 1
 for x, y being Integer holds
( [x,y] in it iff x,y are_congruent_mod m );
existence
ex b1 being Relation of INT st
for x, y being Integer holds
( [x,y] in b1 iff x,y are_congruent_mod m )
proof end;
uniqueness
for b1, b2 being Relation of INT st ( for x, y being Integer holds
( [x,y] in b1 iff x,y are_congruent_mod m ) ) & ( for x, y being Integer holds
( [x,y] in b2 iff x,y are_congruent_mod m ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Cong INT_4:def 1 :
for m being Integer
for b2 being Relation of INT holds
( b2 = Cong m iff for x, y being Integer holds
( [x,y] in b2 iff x,y are_congruent_mod m ) );

registration
let m be Integer;
cluster Cong m -> total ;
coherence
Cong m is total
proof end;
end;

Lm8: for m being Integer holds Cong m is Equivalence_Relation of INT
proof end;

registration
let m be Integer;
cluster Cong m -> reflexive symmetric transitive ;
coherence
( Cong m is reflexive & Cong m is symmetric & Cong m is transitive ) by Lm8;
end;

theorem Th26: :: INT_4:26
for a, b, m, x being Integer st m <> 0 & ((a * x) - b) mod m = 0 holds
for y being Integer holds
( ( a,m are_coprime & ((a * y) - b) mod m = 0 implies y in Class ((Cong m),x) ) & ( y in Class ((Cong m),x) implies ((a * y) - b) mod m = 0 ) )
proof end;

theorem :: INT_4:27
for a, b, m, x being Integer st m <> 0 & a,m are_coprime & ((a * x) - b) mod m = 0 holds
ex s being Integer st [x,(b * s)] in Cong m
proof end;

theorem :: INT_4:28
for a, m being Element of NAT st a <> 0 & m > 1 & a,m are_coprime holds
for b, x being Integer st ((a * x) - b) mod m = 0 holds
[x,(b * (a |^ ((Euler m) -' 1)))] in Cong m
proof end;

theorem :: INT_4:29
for a, b, m being Integer st m <> 0 & a gcd m divides b holds
ex fp being FinSequence of INT st
( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds
((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds
not fp . c1,fp . c2 are_congruent_mod m ) )
proof end;

theorem Th30: :: INT_4:30
for fp being FinSequence of NAT
for d, b, n being Element of NAT st b in dom fp & len fp = n + 1 holds
Del ((fp ^ <*d*>),b) = (Del (fp,b)) ^ <*d*>
proof end;

theorem Th31: :: INT_4:31
for fp being FinSequence of NAT st len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) holds
for b being Element of NAT st b in dom fp holds
(Product (Del (fp,b))) gcd (fp . b) = 1
proof end;

theorem Th32: :: INT_4:32
for fp being FinSequence of NAT
for a being Nat st a in dom fp holds
fp . a divides Product fp
proof end;

theorem :: INT_4:33
for p being Nat
for fp being FinSequence of NAT
for a being Nat st a in dom fp & p divides fp . a holds
p divides Product fp
proof end;

theorem :: INT_4:34
for fp being FinSequence of NAT
for n being Element of NAT
for a being Nat st len fp = n + 1 & a >= 1 & a <= n holds
(Del (fp,a)) . n = fp . (len fp)
proof end;

theorem Th35: :: INT_4:35
for fp being FinSequence of NAT
for a being Nat
for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds
fp . b divides Product (Del (fp,a))
proof end;

Lm9: for i1, i2 being Integer
for n being Nat st n > 0 & i1 mod n = 0 holds
(i1 * i2) mod n = 0
proof end;

theorem Th36: :: INT_4:36
for fp being FinSequence of NAT
for a being Nat st ( for b being Nat st b in dom fp holds
a divides fp . b ) holds
a divides Sum fp
proof end;

theorem :: INT_4:37
for fp being FinSequence of NAT st len fp >= 2 & ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds
fp . b <> 0 ) holds
for fp1 being FinSequence of NAT ex x being Integer st
for b being Element of NAT st b in dom fp holds
(x - (fp1 . b)) mod (fp . b) = 0
proof end;

theorem Th38: :: INT_4:38
for fp being FinSequence of NAT
for a being Nat st ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds
fp . b divides a ) holds
Product fp divides a
proof end;

theorem :: INT_4:39
for x, y being Integer
for fp being FinSequence of NAT st ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds
fp . b > 0 ) holds
for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds
( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds
x,y are_congruent_mod Product fp
proof end;

Lm10: for x, y being Integer holds
( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) )
proof end;

Lm11: for x, y being Integer st x divides y holds
y = (y div x) * x
proof end;

Lm12: for x, y being Integer st ( x <> 0 or y <> 0 ) holds
x div (x gcd y),y div (x gcd y) are_coprime
proof end;

Lm13: for i, x, y being Integer st x divides i & y divides i & x,y are_coprime holds
x * y divides i
proof end;

theorem Th40: :: INT_4:40
for m1, m2, c1, c2 being Integer st m1 <> 0 & m2 <> 0 & m1,m2 are_coprime holds
ex r being Integer st
( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 * m2 ) & ((m1 * r) - (c2 - c1)) mod m2 = 0 )
proof end;

theorem Th41: :: INT_4:41
for m1, m2, c1, c2 being Integer st m1 <> 0 & m2 <> 0 & not m1 gcd m2 divides c1 - c2 holds
for x being Integer holds
( not (x - c1) mod m1 = 0 or not (x - c2) mod m2 = 0 )
proof end;

theorem Th42: :: INT_4:42
for m1, m2, c1, c2 being Integer st m1 <> 0 & m2 <> 0 & m1 gcd m2 divides c2 - c1 holds
ex r being Integer st
( ( for x being Integer st (x - c1) mod m1 = 0 & (x - c2) mod m2 = 0 holds
x,c1 + (m1 * r) are_congruent_mod m1 lcm m2 ) & (((m1 div (m1 gcd m2)) * r) - ((c2 - c1) div (m1 gcd m2))) mod (m2 div (m1 gcd m2)) = 0 )
proof end;

theorem :: INT_4:43
for m1, m2, a, b, c1, c2 being Integer st m1 <> 0 & m2 <> 0 & a gcd m1 divides c1 & b gcd m2 divides c2 & m1,m2 are_coprime holds
ex w, r, s being Integer st
( ( for x being Integer st ((a * x) - c1) mod m1 = 0 & ((b * x) - c2) mod m2 = 0 holds
x,r + ((m1 div (a gcd m1)) * w) are_congruent_mod (m1 div (a gcd m1)) * (m2 div (b gcd m2)) ) & (((a div (a gcd m1)) * r) - (c1 div (a gcd m1))) mod (m1 div (a gcd m1)) = 0 & (((b div (b gcd m2)) * s) - (c2 div (b gcd m2))) mod (m2 div (b gcd m2)) = 0 & (((m1 div (a gcd m1)) * w) - (s - r)) mod (m2 div (b gcd m2)) = 0 )
proof end;

theorem :: INT_4:44
for m1, m2, m3, a, b, c being Integer st m1 <> 0 & m2 <> 0 & m3 <> 0 & m1,m2 are_coprime & m1,m3 are_coprime & m2,m3 are_coprime holds
ex r, s being Integer st
for x being Integer st (x - a) mod m1 = 0 & (x - b) mod m2 = 0 & (x - c) mod m3 = 0 holds
( x,(a + (m1 * r)) + ((m1 * m2) * s) are_congruent_mod (m1 * m2) * m3 & ((m1 * r) - (b - a)) mod m2 = 0 & (((m1 * m2) * s) - ((c - a) - (m1 * r))) mod m3 = 0 )
proof end;

theorem :: INT_4:45
for m1, m2, m3, a, b, c being Integer st m1 <> 0 & m2 <> 0 & m3 <> 0 & ( not m1 gcd m2 divides a - b or not m1 gcd m3 divides a - c or not m2 gcd m3 divides b - c ) holds
for x being Integer holds
( not (x - a) mod m1 = 0 or not (x - b) mod m2 = 0 or not (x - c) mod m3 = 0 ) by Th41;

theorem Th46: :: INT_4:46
for n1, n2, n3 being non zero Nat holds (n1 gcd n3) lcm (n2 gcd n3) = (n1 lcm n2) gcd n3
proof end;

theorem :: INT_4:47
for a, b, c being Integer
for n1, n2, n3 being non zero Nat st n1 gcd n2 divides a - b holds
ex r, s being Integer st
for x being Integer st (x - a) mod n1 = 0 & (x - b) mod n2 = 0 & (x - c) mod n3 = 0 holds
( x,(a + (n1 * r)) + ((n1 lcm n2) * s) are_congruent_mod (n1 lcm n2) lcm n3 & (((n1 div (n1 gcd n2)) * r) - ((b - a) div (n1 gcd n2))) mod (n2 div (n1 gcd n2)) = 0 & ((((n1 lcm n2) div ((n1 lcm n2) gcd n3)) * s) - ((c - (a + (n1 * r))) div ((n1 lcm n2) gcd n3))) mod (n3 div ((n1 lcm n2) gcd n3)) = 0 )
proof end;

definition
let m be Nat;
let X be set ;
pred X is_CRS_of m means :: INT_4:def 2
 ex fp being FinSequence of INT st
( X = rng fp & len fp = m & ( for b being Nat st b in dom fp holds
fp . b in Class ((Cong m),(b -' 1)) ) );
end;

:: deftheorem defines is_CRS_of INT_4:def 2 :
for m being Nat
for X being set holds
( X is_CRS_of m iff ex fp being FinSequence of INT st
( X = rng fp & len fp = m & ( for b being Nat st b in dom fp holds
fp . b in Class ((Cong m),(b -' 1)) ) ) );

theorem :: INT_4:48
for m being Element of NAT holds { a where a is Nat : a < m } is_CRS_of m
proof end;

theorem Th49: :: INT_4:49
for m being Element of NAT
for X being finite set st X is_CRS_of m holds
( card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) )
proof end;

theorem Th50: :: INT_4:50
for m being Element of NAT holds
( {} is_CRS_of m iff m = 0 )
proof end;

theorem Th51: :: INT_4:51
for m being Element of NAT
for X being finite set st card X = m holds
ex fp being FinSequence st
( len fp = m & ( for a being Element of NAT st a in dom fp holds
fp . a in X ) & fp is one-to-one )
proof end;

theorem Th52: :: INT_4:52
for m being Element of NAT
for X being finite Subset of INT st card X = m & ( for x, y being Integer st x in X & y in X & x <> y holds
not [x,y] in Cong m ) holds
X is_CRS_of m
proof end;

theorem :: INT_4:53
for m being Element of NAT
for a being Integer
for X being finite Subset of INT st X is_CRS_of m holds
a ++ X is_CRS_of m
proof end;

theorem :: INT_4:54
for m being Element of NAT
for a being Integer
for X being finite Subset of INT st a,m are_coprime & X is_CRS_of m holds
a ** X is_CRS_of m
proof end;