begin
:: deftheorem Def1 defines multint INT_3:def 1 :
for b1 being Element of K18(K19(K19(INT ,INT ),INT )) holds
( b1 = multint iff for a, b being Element of INT holds b1 . a,b = multreal . a,b );
:: deftheorem defines compint INT_3:def 2 :
for b1 being Element of K18(K19(INT ,INT )) holds
( b1 = compint iff for a being Element of INT holds b1 . a = compreal . a );
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 :
INT.Ring = doubleLoopStr(# INT ,addint ,multint ,(In 1,INT ),(In 0 ,INT ) #);
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 :
for a being Element of INT.Ring holds
( ( a >= 0. INT.Ring implies abs a = a ) & ( not a >= 0. INT.Ring implies abs a = - a ) );
:: deftheorem Def6 defines absint INT_3:def 6 :
for b1 being Function of the carrier of INT.Ring ,NAT holds
( b1 = absint iff for a being Element of INT.Ring holds b1 . a = absreal . a );
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 :
for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b3 being Element of INT.Ring holds
( b3 = a div b iff ex r being Element of INT.Ring st
( a = (b3 * b) + r & 0. INT.Ring <= r & r < abs b ) );
:: deftheorem Def8 defines mod INT_3:def 8 :
for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
for b3 being Element of INT.Ring holds
( b3 = a mod b iff ex q being Element of INT.Ring st
( a = (q * b) + b3 & 0. INT.Ring <= b3 & b3 < abs b ) );
theorem
begin
:: deftheorem Def9 defines Euclidian INT_3:def 9 :
for I being non empty doubleLoopStr holds
( I is Euclidian iff ex f being Function of the carrier of I,NAT st
for a, b being Element of I st b <> 0. I holds
ex q, r being Element of I st
( a = (q * b) + r & ( r = 0. I or f . r < f . b ) ) );
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 :
for E being non empty Euclidian doubleLoopStr
for b2 being Function of the carrier of E,NAT holds
( b2 is DegreeFunction of E iff for a, b being Element of E st b <> 0. E holds
ex q, r being Element of E st
( a = (q * b) + r & ( r = 0. E or b2 . r < b2 . b ) ) );
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 :
for n being natural number st n > 0 holds
for b2 being BinOp of (Segm n) holds
( b2 = multint n iff for k, l being Element of Segm n holds b2 . k,l = (k * l) mod n );
:: deftheorem Def12 defines compint INT_3:def 12 :
for n being natural number st n > 0 holds
for b2 being UnOp of (Segm n) holds
( b2 = compint n iff for k being Element of Segm n holds b2 . k = (n - k) mod n );
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 :
for n being natural number holds INT.Ring n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In 1,(Segm n)),(In 0 ,(Segm n)) #);
theorem Th20:
Lm12:
for n being natural number st 1 < n holds
1. (INT.Ring n) = 1
theorem Th21:
theorem Th22:
theorem
theorem