begin
theorem Th1:
theorem Th2:
Lm1:
for x, y being Integer holds
( ( x divides y implies y mod x = 0 ) & ( x <> 0 & y mod x = 0 implies x divides y ) )
:: deftheorem Def1 defines Poly-INT INT_5:def 1 :
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem Def2 defines is_quadratic_residue_mod INT_5:def 2 :
theorem Th9:
theorem
theorem Th11:
Lm2:
for i being Integer
for p being Prime holds
( i,p are_relative_prime or p divides i )
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem
theorem
:: deftheorem Def3 defines Lege INT_5:def 3 :
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem Th36:
theorem
theorem
begin
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
Lm3:
for fp being FinSequence of NAT holds Sum fp is Element of NAT
;
theorem Th49:
theorem
theorem