:: by Xiquan Liang , Li Yan and Junjie Zhao

::

:: Received August 28, 2007

:: Copyright (c) 2007-2021 Association of Mizar Users

registration
end;

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

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

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

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

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

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

i1 * i3,i2 * i3 are_congruent_mod i

proof end;

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 )

for a being Integer ex q, r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

proof end;

::$CT

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

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

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

ex x being Integer st ((a * x) - b) mod m = 0

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

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

for x being Integer holds not ((p * x) - q) mod (p |^ n) = 0

proof end;

definition

let m be Integer;

ex b_{1} being Relation of INT st

for x, y being Integer holds

( [x,y] in b_{1} iff x,y are_congruent_mod m )

for b_{1}, b_{2} being Relation of INT st ( for x, y being Integer holds

( [x,y] in b_{1} iff x,y are_congruent_mod m ) ) & ( for x, y being Integer holds

( [x,y] in b_{2} iff x,y are_congruent_mod m ) ) holds

b_{1} = b_{2}

end;
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 for x, y being Integer holds

( [x,y] in it iff x,y are_congruent_mod m );

ex b

for x, y being Integer holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def1 defines Cong INT_4:def 1 :

for m being Integer

for b_{2} being Relation of INT holds

( b_{2} = Cong m iff for x, y being Integer holds

( [x,y] in b_{2} iff x,y are_congruent_mod m ) );

for m being Integer

for b

( b

( [x,y] in b

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

proof end;

registration

let m be Integer;

coherence

( Cong m is reflexive & Cong m is symmetric & Cong m is transitive ) by Lm8;

end;
coherence

( Cong m is reflexive & Cong m is symmetric & Cong m is transitive ) by Lm8;

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

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

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

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

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

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

(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 :: 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

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)

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

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

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

(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

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

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 )

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 )

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 )

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 )

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 )

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

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 )

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;

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

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

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

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

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

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

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;