:: The Ring of Integers, Euclidean Rings and Modulo Integers
:: by Christoph Schwarzweller
::
:: Received February 4, 1999
:: Copyright (c) 1999 Association of Mizar Users
:: deftheorem Def1 defines multint INT_3:def 1 :
:: deftheorem defines compint INT_3:def 2 :
definition
func INT.Ring -> doubleLoopStr equals :: INT_3:def 3
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;
1 in INT
by INT_1:def 2;
then Lm4:
1 = 1. 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: :: INT_3:1
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 b' being Integer st b' = b & 0 <= b' 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 b' being Integer st b' = b & 0 <= b' holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b )
theorem Th2: :: INT_3:2
:: deftheorem Def7 defines div INT_3:def 7 :
:: deftheorem Def8 defines mod INT_3:def 8 :
theorem :: INT_3:3
:: deftheorem Def9 defines Euclidian INT_3:def 9 :
Lm9:
for F being non empty almost_left_invertible associative commutative well-unital right_zeroed 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: :: INT_3:4
theorem Th5: :: INT_3:5
theorem :: INT_3:6
theorem :: INT_3:7
canceled;
theorem Th8: :: INT_3:8
theorem Th9: :: INT_3:9
theorem Th10: :: INT_3:10
theorem :: INT_3:11
canceled;
theorem Th12: :: INT_3:12
theorem Th13: :: INT_3:13
theorem Th14: :: INT_3:14
theorem Th15: :: INT_3:15
theorem Th16: :: INT_3:16
:: deftheorem Def11 defines multint INT_3:def 11 :
:: deftheorem Def12 defines compint INT_3:def 12 :
theorem Th17: :: INT_3:17
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: :: INT_3:18
theorem :: INT_3:19
definition
let n be
natural number ;
func INT.Ring n -> doubleLoopStr equals :: INT_3:def 13
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: :: INT_3:20
Lm12:
for n being natural number st 1 < n holds
1. (INT.Ring n) = 1
theorem Th21: :: INT_3:21
theorem Th22: :: INT_3:22
theorem :: INT_3:23
theorem :: INT_3:24