:: The Ring of Integers, Euclidean Rings and Modulo Integers :: by Christoph Schwarzweller :: :: Received February 4, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin definition redefine func multint means :Def1: :: INT_3:def 1 for a, b being Element of INT holds it . (a,b) = multreal . (a,b); compatibility for b1 being Element of K6(K7(K7(INT,INT),INT)) holds ( b1 = multint iff for a, b being Element of INT holds b1 . (a,b) = multreal . (a,b) ) proofend; end; :: deftheorem Def1 defines multint INT_3:def_1_:_ for b1 being Element of K6(K7(K7(INT,INT),INT)) holds ( b1 = multint iff for a, b being Element of INT holds b1 . (a,b) = multreal . (a,b) ); definition redefine func compint means :: INT_3:def 2 for a being Element of INT holds it . a = compreal . a; compatibility for b1 being Element of K6(K7(INT,INT)) holds ( b1 = compint iff for a being Element of INT holds b1 . a = compreal . a ) proofend; end; :: deftheorem defines compint INT_3:def_2_:_ for b1 being Element of K6(K7(INT,INT)) holds ( b1 = compint iff for a being Element of INT holds b1 . a = compreal . a ); 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_:_ INT.Ring = doubleLoopStr(# INT,addint,multint,(In (1,INT)),(In (0,INT)) #); Lm1: for x being Element of INT.Ring holds x in REAL proofend; registration cluster INT.Ring -> non empty strict ; coherence ( INT.Ring is strict & not INT.Ring is empty ) ; end; registration cluster the carrier of INT.Ring -> integer-membered ; coherence the carrier of INT.Ring is integer-membered ; end; registration let a, b be Element of INT.Ring; let c, d be Integer; identifya * b with c * d when a = c, b = d; compatibility ( a = c & b = d implies a * b = c * d ) proofend; identifya + b with c + d when a = c, b = d; compatibility ( a = c & b = d implies a + b = c + d ) proofend; end; set M = INT.Ring ; Lm2: 0 in INT by INT_1:def_2; then Lm3: 0 = 0. INT.Ring by FUNCT_7:def_1; registration cluster INT.Ring -> well-unital ; coherence INT.Ring is well-unital proofend; end; Lm4: 1_ INT.Ring = 1 proofend; registration cluster INT.Ring -> non degenerated right_complementable associative commutative Abelian add-associative right_zeroed distributive domRing-like ; coherence ( INT.Ring is Abelian & INT.Ring is add-associative & INT.Ring is right_zeroed & INT.Ring is right_complementable & INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated ) proofend; end; registration let a be Element of INT.Ring; let b be Integer; identify - a with - b when a = b; compatibility ( a = b implies - a = - b ) proofend; end; definition let a be Element of INT.Ring; :: original:|. redefine func abs a -> Element of INT.Ring equals :: INT_3:def 4 a if a >= 0. INT.Ring otherwise - a; coherence |.a.| is Element of INT.Ring proofend; compatibility for b1 being Element of INT.Ring holds ( ( a >= 0. INT.Ring implies ( b1 = |.a.| iff b1 = a ) ) & ( not a >= 0. INT.Ring implies ( b1 = |.a.| iff b1 = - a ) ) ) by Lm3, ABSVALUE:def_1; consistency for b1 being Element of INT.Ring holds verum ; end; :: deftheorem defines abs INT_3:def_4_:_ 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 ) ); definition func absint -> Function of the carrier of INT.Ring,NAT means :Def5: :: INT_3:def 5 for a being Element of INT.Ring holds it . a = absreal . a; existence ex b1 being Function of the carrier of INT.Ring,NAT st for a being Element of INT.Ring holds b1 . a = absreal . a proofend; uniqueness for b1, b2 being Function of the carrier of INT.Ring,NAT st ( for a being Element of INT.Ring holds b1 . a = absreal . a ) & ( for a being Element of INT.Ring holds b2 . a = absreal . a ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines absint INT_3:def_5_:_ 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: :: INT_3:1 for a being Element of INT.Ring holds absint . a = abs a proofend; Lm5: for a being Integer holds ( a = 0 or absreal . a >= 1 ) proofend; Lm6: 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 ) ) proofend; 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 & 0. INT.Ring <= r & r < abs b ) proofend; theorem Th2: :: INT_3:2 for a, b, q1, q2, r1, r2 being Element of INT.Ring st b <> 0. INT.Ring & a = (q1 * b) + r1 & 0. INT.Ring <= r1 & r1 < abs b & a = (q2 * b) + r2 & 0. INT.Ring <= r2 & r2 < abs b holds ( q1 = q2 & r1 = r2 ) proofend; definition let a, b be Element of INT.Ring; assume A1: b <> 0. INT.Ring ; funca div b -> Element of INT.Ring means :Def6: :: INT_3:def 6 ex r being Element of INT.Ring st ( a = (it * b) + r & 0. INT.Ring <= r & r < abs b ); existence ex b1, r being Element of INT.Ring st ( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b ) proofend; uniqueness for b1, b2 being Element of INT.Ring st ex r being Element of INT.Ring st ( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b ) & ex r being Element of INT.Ring st ( a = (b2 * b) + r & 0. INT.Ring <= r & r < abs b ) holds b1 = b2 by A1, Th2; end; :: deftheorem Def6 defines div INT_3:def_6_:_ 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 ) ); definition let a, b be Element of INT.Ring; assume A1: b <> 0. INT.Ring ; funca mod b -> Element of INT.Ring means :Def7: :: INT_3:def 7 ex q being Element of INT.Ring st ( a = (q * b) + it & 0. INT.Ring <= it & it < abs b ); existence ex b1, q being Element of INT.Ring st ( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b ) proofend; uniqueness for b1, b2 being Element of INT.Ring st ex q being Element of INT.Ring st ( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b ) & ex q being Element of INT.Ring st ( a = (q * b) + b2 & 0. INT.Ring <= b2 & b2 < abs b ) holds b1 = b2 by A1, Th2; end; :: deftheorem Def7 defines mod 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 mod b iff ex q being Element of INT.Ring st ( a = (q * b) + b3 & 0. INT.Ring <= b3 & b3 < abs b ) ); theorem :: INT_3:3 for a, b being Element of INT.Ring st b <> 0. INT.Ring holds a = ((a div b) * b) + (a mod b) proofend; begin definition let I be non empty doubleLoopStr ; attrI is Euclidian means :Def8: :: INT_3:def 8 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 ) ); end; :: deftheorem Def8 defines Euclidian INT_3:def_8_:_ 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 ) ) ); registration cluster INT.Ring -> Euclidian ; coherence INT.Ring is Euclidian proofend; end; Lm8: 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 ) ) proofend; registration cluster non empty non degenerated right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like Euclidian for doubleLoopStr ; existence ex b1 being Ring st ( b1 is strict & b1 is Euclidian & b1 is domRing-like & not b1 is degenerated & b1 is distributive & b1 is commutative ) proofend; end; definition mode EuclidianRing is non degenerated commutative domRing-like Euclidian Ring; end; registration cluster non empty non degenerated V77() right_complementable strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like Euclidian for doubleLoopStr ; existence ex b1 being EuclidianRing st b1 is strict proofend; end; definition let E be non empty Euclidian doubleLoopStr ; mode DegreeFunction of E -> Function of the carrier of E,NAT means :Def9: :: INT_3:def 9 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 it . r < it . b ) ); existence ex b1 being Function of the carrier of E,NAT st 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 b1 . r < b1 . b ) ) by Def8; end; :: deftheorem Def9 defines DegreeFunction INT_3:def_9_:_ 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: :: INT_3:4 for E being EuclidianRing holds E is gcdDomain proofend; registration cluster non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like Euclidian -> non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like gcd-like for doubleLoopStr ; coherence for b1 being non empty non degenerated right_complementable associative commutative Abelian add-associative right_zeroed right-distributive well-unital domRing-like doubleLoopStr st b1 is Euclidian holds b1 is gcd-like by Th4; end; definition :: original:absint redefine func absint -> DegreeFunction of INT.Ring ; coherence absint is DegreeFunction of INT.Ring proofend; end; theorem Th5: :: INT_3:5 for F being non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr holds F is Euclidian proofend; registration cluster non empty almost_left_invertible associative commutative right_zeroed well-unital -> non empty Euclidian for doubleLoopStr ; coherence for b1 being non empty doubleLoopStr st b1 is commutative & b1 is associative & b1 is well-unital & b1 is almost_left_invertible & b1 is right_zeroed & b1 is almost_left_invertible holds b1 is Euclidian by Th5; end; theorem :: INT_3:6 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 holds f is DegreeFunction of F proofend; begin definition let n be Nat; assume A1: n > 0 ; func multint n -> BinOp of (Segm n) means :Def10: :: INT_3:def 10 for k, l being Element of Segm n holds it . (k,l) = (k * l) mod n; existence ex b1 being BinOp of (Segm n) st for k, l being Element of Segm n holds b1 . (k,l) = (k * l) mod n proofend; uniqueness for b1, b2 being BinOp of (Segm n) st ( for k, l being Element of Segm n holds b1 . (k,l) = (k * l) mod n ) & ( for k, l being Element of Segm n holds b2 . (k,l) = (k * l) mod n ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines multint INT_3:def_10_:_ for n being Nat 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 ); definition let n be Nat; assume A1: n > 0 ; func compint n -> UnOp of (Segm n) means :Def11: :: INT_3:def 11 for k being Element of Segm n holds it . k = (n - k) mod n; existence ex b1 being UnOp of (Segm n) st for k being Element of Segm n holds b1 . k = (n - k) mod n proofend; uniqueness for b1, b2 being UnOp of (Segm n) st ( for k being Element of Segm n holds b1 . k = (n - k) mod n ) & ( for k being Element of Segm n holds b2 . k = (n - k) mod n ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines compint INT_3:def_11_:_ for n being Nat 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 Th7: :: INT_3:7 for n being Nat st n > 0 holds for a, b being Element of Segm n holds ( ( a + b < n implies (addint n) . (a,b) = a + b ) & ( (addint n) . (a,b) = a + b implies a + b < n ) & ( a + b >= n implies (addint n) . (a,b) = (a + b) - n ) & ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) ) proofend; Lm9: for a, b being Nat st b <> 0 holds ex k being Element of NAT st ( k * b <= a & a < (k + 1) * b ) proofend; theorem Th8: :: INT_3:8 for n being Nat st n > 0 holds for a, b being Element of Segm n for k being Nat holds ( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . (a,b) = (a * b) - (k * n) ) proofend; theorem :: INT_3:9 for n being Nat st n > 0 holds for a being Element of Segm n holds ( ( a = 0 implies (compint n) . a = 0 ) & ( (compint n) . a = 0 implies a = 0 ) & ( a <> 0 implies (compint n) . a = n - a ) & ( (compint n) . a = n - a implies a <> 0 ) ) proofend; definition let n be Nat; func INT.Ring n -> doubleLoopStr equals :: INT_3:def 12 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_12_:_ for n being Nat holds INT.Ring n = doubleLoopStr(# (Segm n),(addint n),(multint n),(In (1,(Segm n))),(In (0,(Segm n))) #); registration let n be non zero Nat; cluster INT.Ring n -> non empty strict ; coherence ( INT.Ring n is strict & not INT.Ring n is empty ) ; end; theorem Th10: :: INT_3:10 ( INT.Ring 1 is degenerated & INT.Ring 1 is Ring & INT.Ring 1 is almost_left_invertible & INT.Ring 1 is unital & INT.Ring 1 is distributive & INT.Ring 1 is commutative ) proofend; registration cluster non empty degenerated right_complementable almost_left_invertible strict unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital for doubleLoopStr ; existence ex b1 being Ring st ( b1 is strict & b1 is degenerated & b1 is unital & b1 is distributive & b1 is almost_left_invertible & b1 is commutative ) by Th10; end; Lm10: now__::_thesis:_for_a,_n_being_Nat_st_a_in_Segm_n_&_a_>_0_holds_ n_-_a_in_Segm_n let a, n be Nat; ::_thesis: ( a in Segm n & a > 0 implies n - a in Segm n ) assume a in Segm n ; ::_thesis: ( a > 0 implies n - a in Segm n ) then a < n by NAT_1:44; then A1: n - a is Element of NAT by INT_1:5; assume a > 0 ; ::_thesis: n - a in Segm n then n - a < n - 0 by XREAL_1:15; hence n - a in Segm n by A1, NAT_1:44; ::_thesis: verum end; Lm11: for n being Nat st 1 < n holds 1. (INT.Ring n) = 1 proofend; theorem Th11: :: INT_3:11 for n being Nat st n > 1 holds ( not INT.Ring n is degenerated & INT.Ring n is commutative Ring ) proofend; theorem Th12: :: INT_3:12 for p being Nat st p > 1 holds ( INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr iff p is Prime ) proofend; registration clusterV10() prime -> non zero for set ; coherence for b1 being Prime holds not b1 is zero proofend; end; registration let p be Prime; cluster INT.Ring p -> non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive ; coherence ( INT.Ring p is add-associative & INT.Ring p is right_zeroed & INT.Ring p is right_complementable & INT.Ring p is Abelian & INT.Ring p is commutative & INT.Ring p is associative & INT.Ring p is well-unital & INT.Ring p is distributive & INT.Ring p is almost_left_invertible & not INT.Ring p is degenerated ) proofend; end; theorem :: INT_3:13 1. INT.Ring = 1 by Lm4; theorem :: INT_3:14 for n being Nat st 1 < n holds 1. (INT.Ring n) = 1 by Lm11; begin :: from SCMRING3, 2011.08.19, A.T. registration cluster INT.Ring -> infinite ; coherence not INT.Ring is finite ; end; registration cluster non empty infinite right_complementable strict unital associative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital distributive left_unital for doubleLoopStr ; existence ex b1 being Ring st ( b1 is strict & b1 is infinite ) proofend; end;