begin
theorem Th1:
theorem Th2:
Lm1:
for a being Integer
for X being Subset of holds a ++ X c= INT
Lm2:
for a being Integer
for X being Subset of holds a ** X c= INT
Lm3:
for x being Integer
for X being Subset of
for a being Integer holds
( x in a ** X iff ex y being Integer st
( y in X & x = a * y ) )
theorem Th3:
theorem Th4:
theorem Th5:
begin
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:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem
theorem
begin
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem
theorem
theorem
begin
definition
let m be
Integer;
func Cong m -> Relation of
means :
Def1:
for
x,
y being
Integer holds
(
[x,y] in it iff
x,
y are_congruent_mod m );
existence
ex b1 being Relation of 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 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:
theorem
theorem
theorem
begin
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem
theorem Th35:
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:
theorem
theorem Th38:
theorem
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:
theorem Th41:
theorem Th42:
theorem
theorem
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
theorem Th46:
theorem
begin
:: deftheorem Def2 defines is_CRS_of INT_4:def 2 :
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem