begin
:: deftheorem Def1 defines multint INT_3:def 1 :
:: deftheorem defines compint INT_3:def 2 :
definition
func INT.Ring -> doubleLoopStr equals
doubleLoopStr(#
INT ,
addint ,
multint ,
(In 1,INT ),
(In 0 ,INT ) #);
coherence
doubleLoopStr(# INT ,addint ,multint ,(In 1,INT ),(In 0 ,INT ) #) is doubleLoopStr
;
end;
:: deftheorem defines INT.Ring INT_3:def 3 :
Lm1:
for x being Element of INT.Ring holds x in REAL
set M = INT.Ring ;
Lm2:
0 in INT
by INT_1:def 2;
then Lm3:
0 = 0. INT.Ring
by FUNCT_7:def 1;
Lm5:
1_ INT.Ring = 1
:: deftheorem INT_3:def 4 :
canceled;
:: deftheorem defines abs INT_3:def 5 :
:: deftheorem Def6 defines absint INT_3:def 6 :
theorem Th1:
Lm6:
for a being Integer holds
( a = 0 or absreal . a >= 1 )
Lm7:
for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b9 being Integer st b9 = b & 0 <= b9 holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )
Lm8:
for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b9 being Integer st b9 = b & 0 <= b9 holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b )
theorem Th2:
:: deftheorem Def7 defines div INT_3:def 7 :
:: deftheorem Def8 defines mod INT_3:def 8 :
theorem
begin
:: deftheorem Def9 defines Euclidian INT_3:def 9 :
Lm9:
for F being non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr
for f being Function of the carrier of F,NAT
for a, b being Element of F st b <> 0. F holds
ex q, r being Element of F st
( a = (q * b) + r & ( r = 0. F or f . r < f . b ) )
:: deftheorem Def10 defines DegreeFunction INT_3:def 10 :
theorem Th4:
theorem Th5:
theorem
begin
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
theorem
canceled;
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
begin
:: deftheorem Def11 defines multint INT_3:def 11 :
:: deftheorem Def12 defines compint INT_3:def 12 :
theorem Th17:
Lm10:
for a, b being natural number st b <> 0 holds
ex k being Element of NAT st
( k * b <= a & a < (k + 1) * b )
theorem Th18:
theorem
definition
let n be
natural number ;
func INT.Ring n -> doubleLoopStr equals
doubleLoopStr(#
(Segm n),
(addint n),
(multint n),
(In 1,(Segm n)),
(In 0 ,(Segm n)) #);
coherence
doubleLoopStr(# (Segm n),(addint n),(multint n),(In 1,(Segm n)),(In 0 ,(Segm n)) #) is doubleLoopStr
;
end;
:: deftheorem defines INT.Ring INT_3:def 13 :
theorem Th20:
Lm12:
for n being natural number st 1 < n holds
1. (INT.Ring n) = 1
theorem Th21:
theorem Th22:
theorem
theorem