begin
theorem Th1:
theorem Th2:
theorem Th3:
Lm1:
for a being Integer holds
( a divides - a & - a divides a )
Lm2:
for a, b, c being Integer st a divides b & b divides c holds
a divides c
Lm3:
for a, b being Integer holds
( a divides b iff a divides - b )
Lm4:
for a, b being Integer holds
( a divides b iff - a divides b )
Lm5:
for a being Integer holds
( a divides 0 & 1 divides a & - 1 divides a )
Lm6:
for a, b, c being Integer st a divides b & a divides c holds
a divides b mod c
Lm7:
for k, l being Nat holds
( k divides l iff ex t being Nat st l = k * t )
Lm8:
for i, j being Nat st i divides j & j divides i holds
i = j
:: deftheorem INT_2:def 1 :
canceled;
:: deftheorem Def2 defines lcm INT_2:def 2 :
theorem Th4:
Lm9:
for j, i being Nat st 0 < j & i divides j holds
i <= j
:: deftheorem Def3 defines gcd INT_2:def 3 :
theorem Th5:
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem
theorem
theorem
theorem Th12:
theorem
theorem Th14:
theorem
theorem
theorem Th17:
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem Th31:
theorem
theorem
theorem
theorem Th35:
:: deftheorem Def4 defines are_relative_prime INT_2:def 4 :
theorem
canceled;
theorem
canceled;
theorem
theorem Th39:
theorem Th40:
theorem
:: deftheorem Def5 defines prime INT_2:def 5 :
theorem
canceled;
theorem Th43:
theorem Th44:
theorem
canceled;
theorem Th46:
theorem
theorem
begin
theorem
theorem
theorem