:: Linear Congruence Relation and Complete Residue Systems
:: by Xiquan Liang , Li Yan and Junjie Zhao
::
:: Received August 28, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: INT_4:1
theorem Th2: :: INT_4:2
Lm1:
for a being Integer
for X being Subset of INT holds a ++ X c= INT
Lm2:
for a being Integer
for X being Subset of INT holds a ** X c= INT
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 ) )
theorem Th3: :: INT_4:3
theorem Th4: :: INT_4:4
theorem Th5: :: INT_4:5
Lm4:
for i1, i2, i3 being Integer st i1 divides i2 & i1 divides i3 holds
i1 divides i2 - i3
Lm5:
for i, a, b being Integer st i divides a & i divides a - b holds
i divides b
Lm6:
for p, n being Nat st p is prime & p,n are_relative_prime holds
not p divides n
Lm7:
for p being Nat st p > 0 holds
p >= 1 + 0
by NAT_1:13;
theorem Th6: :: INT_4:6
theorem Th7: :: INT_4:7
theorem :: INT_4:8
theorem Th9: :: INT_4:9
theorem Th10: :: INT_4:10
theorem Th11: :: INT_4:11
theorem Th12: :: INT_4:12
theorem Th13: :: INT_4:13
theorem :: INT_4:14
theorem Th15: :: INT_4:15
theorem Th16: :: INT_4:16
theorem :: INT_4:17
theorem :: INT_4:18
theorem Th19: :: INT_4:19
theorem :: INT_4:20
theorem Th21: :: INT_4:21
theorem Th22: :: INT_4:22
theorem :: INT_4:23
theorem :: INT_4:24
theorem :: INT_4:25
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 )
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
end;
:: deftheorem Def1 defines Cong INT_4:def 1 :
Lm8:
for m being Integer holds Cong m is Equivalence_Relation of INT
theorem Th26: :: INT_4:26
theorem :: INT_4:27
theorem :: INT_4:28
theorem :: INT_4:29
theorem Th30: :: INT_4:30
theorem Th31: :: INT_4:31
theorem Th32: :: INT_4:32
theorem :: INT_4:33
theorem :: INT_4:34
theorem Th35: :: INT_4:35
Lm9:
for i1, i2 being Integer
for n being Nat st n > 0 & i1 mod n = 0 holds
(i1 * i2) mod n = 0
theorem Th36: :: INT_4:36
theorem :: INT_4:37
theorem Th38: :: INT_4:38
theorem :: INT_4:39
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 ) )
Lm11:
for x, y being Integer st x divides y holds
y = (y div x) * x
Lm12:
for x, y being Integer st ( x <> 0 or y <> 0 ) holds
x div (x gcd y),y div (x gcd y) are_relative_prime
Lm13:
for x, i, y being Integer st x divides i & y divides i & x,y are_relative_prime holds
x * y divides i
theorem Th40: :: INT_4:40
theorem Th41: :: INT_4:41
theorem Th42: :: INT_4:42
theorem :: INT_4:43
theorem :: INT_4:44
for
m1,
m2,
m3,
a,
b,
c being
Integer st
m1 <> 0 &
m2 <> 0 &
m3 <> 0 &
m1,
m2 are_relative_prime &
m1,
m3 are_relative_prime &
m2,
m3 are_relative_prime 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 )
theorem :: INT_4:45
theorem Th46: :: INT_4:46
theorem :: INT_4:47
:: deftheorem Def2 defines is_CRS_of INT_4:def 2 :
theorem Th48: :: INT_4:48
theorem Th49: :: INT_4:49
theorem Th50: :: INT_4:50
theorem Th51: :: INT_4:51
theorem Th52: :: INT_4:52
theorem :: INT_4:53
theorem :: INT_4:54