:: INT_3 semantic presentation 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) ) proof let b be BinOp of INT; ::_thesis: ( b = multint iff for a, b being Element of INT holds b . (a,b) = multreal . (a,b) ) hereby ::_thesis: ( ( for a, b being Element of INT holds b . (a,b) = multreal . (a,b) ) implies b = multint ) assume A1: b = multint ; ::_thesis: for i1, i2 being Element of INT holds b . (i1,i2) = multreal . (i1,i2) let i1, i2 be Element of INT ; ::_thesis: b . (i1,i2) = multreal . (i1,i2) thus b . (i1,i2) = i1 * i2 by A1, BINOP_2:def_22 .= multreal . (i1,i2) by BINOP_2:def_11 ; ::_thesis: verum end; assume A2: for i1, i2 being Element of INT holds b . (i1,i2) = multreal . (i1,i2) ; ::_thesis: b = multint now__::_thesis:_for_i1,_i2_being_Element_of_INT_holds_b_._(i1,i2)_=_multint_._(i1,i2) let i1, i2 be Element of INT ; ::_thesis: b . (i1,i2) = multint . (i1,i2) thus b . (i1,i2) = multreal . (i1,i2) by A2 .= i1 * i2 by BINOP_2:def_11 .= multint . (i1,i2) by BINOP_2:def_22 ; ::_thesis: verum end; hence b = multint by BINOP_1:2; ::_thesis: verum end; 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 ) proof let b be UnOp of INT; ::_thesis: ( b = compint iff for a being Element of INT holds b . a = compreal . a ) hereby ::_thesis: ( ( for a being Element of INT holds b . a = compreal . a ) implies b = compint ) assume A1: b = compint ; ::_thesis: for i being Element of INT holds b . i = compreal . i let i be Element of INT ; ::_thesis: b . i = compreal . i thus b . i = - i by A1, BINOP_2:def_19 .= compreal . i by BINOP_2:def_7 ; ::_thesis: verum end; assume A2: for i being Element of INT holds b . i = compreal . i ; ::_thesis: b = compint now__::_thesis:_for_i_being_Element_of_INT_holds_b_._i_=_compint_._i let i be Element of INT ; ::_thesis: b . i = compint . i thus b . i = compreal . i by A2 .= - i by BINOP_2:def_7 .= compint . i by BINOP_2:def_19 ; ::_thesis: verum end; hence b = compint by FUNCT_2:63; ::_thesis: verum end; 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 proof let x be Element of INT.Ring; ::_thesis: x in REAL x in INT ; hence x in REAL by NUMBERS:15; ::_thesis: verum end; 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 ) proof assume A1: ( a = c & b = d ) ; ::_thesis: a * b = c * d multint . (a,b) = multreal . (a,b) by Def1 .= c * d by A1, BINOP_2:def_11 ; hence a * b = c * d ; ::_thesis: verum end; identifya + b with c + d when a = c, b = d; compatibility ( a = c & b = d implies a + b = c + d ) proof assume A2: ( a = c & b = d ) ; ::_thesis: a + b = c + d addint . (a,b) = addreal . (a,b) by GR_CY_1:def_1 .= c + d by A2, BINOP_2:def_9 ; hence a + b = c + d ; ::_thesis: verum end; 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 proof let x be Element of INT.Ring; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. INT.Ring) = x & (1. INT.Ring) * x = x ) 1 in INT by INT_1:def_2; then 1 = 1. INT.Ring by FUNCT_7:def_1; hence ( x * (1. INT.Ring) = x & (1. INT.Ring) * x = x ) ; ::_thesis: verum end; end; Lm4: 1_ INT.Ring = 1 proof reconsider e = 1 as Element of INT.Ring by INT_1:def_1; for x being Element of INT.Ring holds ( x * e = x & e * x = x ) ; then 1_ INT.Ring = e by GROUP_1:def_4; hence 1_ INT.Ring = 1 ; ::_thesis: verum end; 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 ) proof thus for a, b being Element of INT.Ring holds a + b = b + a ; :: according to RLVECT_1:def_2 ::_thesis: ( 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 ) thus for a, b, c being Element of INT.Ring holds (a + b) + c = a + (b + c) ; :: according to RLVECT_1:def_3 ::_thesis: ( 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 ) hereby :: according to RLVECT_1:def_4 ::_thesis: ( 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 ) reconsider t = 0 as Element of REAL ; let a be Element of INT.Ring; ::_thesis: a + (0. INT.Ring) = a reconsider a9 = a as Element of REAL by Lm1; A1: addreal . (a9,t) = a9 + t by BINOP_2:def_9 .= a ; a + (0. INT.Ring) = addreal . (a,(0. INT.Ring)) by GR_CY_1:def_1 .= addreal . (a,0) by Lm2, FUNCT_7:def_1 ; hence a + (0. INT.Ring) = a by A1; ::_thesis: verum end; thus INT.Ring is right_complementable ::_thesis: ( INT.Ring is distributive & INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated ) proof let a be Element of INT.Ring; :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable reconsider a9 = a as Integer ; reconsider v = - a9 as Element of INT.Ring ; take v ; :: according to ALGSTR_0:def_11 ::_thesis: a + v = 0. INT.Ring thus a + v = 0. INT.Ring by FUNCT_7:def_1; ::_thesis: verum end; thus for a, b, c being Element of INT.Ring holds ( a * (b + c) = (a * b) + (a * c) & (b + c) * a = (b * a) + (c * a) ) ; :: according to VECTSP_1:def_7 ::_thesis: ( INT.Ring is commutative & INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated ) thus for x, y being Element of INT.Ring holds x * y = y * x ; :: according to GROUP_1:def_12 ::_thesis: ( INT.Ring is associative & INT.Ring is domRing-like & not INT.Ring is degenerated ) thus for a, b, c being Element of INT.Ring holds (a * b) * c = a * (b * c) ; :: according to GROUP_1:def_3 ::_thesis: ( INT.Ring is domRing-like & not INT.Ring is degenerated ) thus for a, b being Element of INT.Ring holds ( not a * b = 0. INT.Ring or a = 0. INT.Ring or b = 0. INT.Ring ) by Lm3, XCMPLX_1:6; :: according to VECTSP_2:def_1 ::_thesis: not INT.Ring is degenerated thus 0. INT.Ring <> 1. INT.Ring by Lm2, Lm4, FUNCT_7:def_1; :: according to STRUCT_0:def_8 ::_thesis: verum end; 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 ) proof reconsider b9 = - b as Element of INT.Ring ; assume b = a ; ::_thesis: - a = - b then b9 + a = 0. INT.Ring by FUNCT_7:def_1; hence - a = - b by RLVECT_1:6; ::_thesis: verum end; 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 proof abs a in INT by INT_1:def_2; hence |.a.| is Element of INT.Ring ; ::_thesis: verum end; 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 proof dom absreal = REAL by FUNCT_2:def_1; then A1: dom (absreal | INT) = the carrier of INT.Ring by NUMBERS:15, RELAT_1:62; for y being set st y in rng (absreal | INT) holds y in NAT proof let y be set ; ::_thesis: ( y in rng (absreal | INT) implies y in NAT ) assume y in rng (absreal | INT) ; ::_thesis: y in NAT then consider x being set such that A2: [x,y] in absreal | INT by XTUPLE_0:def_13; A3: (absreal | INT) . x = y by A2, FUNCT_1:1; A4: x in dom (absreal | INT) by A2, XTUPLE_0:def_12; then reconsider x = x as Integer by A1; A5: (absreal | INT) . x = absreal . x by A1, A4, FUNCT_1:49; now__::_thesis:_(_(_0_<=_x_&_(absreal_|_INT)_._x_is_Element_of_NAT_)_or_(_not_0_<=_x_&_(absreal_|_INT)_._x_is_Element_of_NAT_)_) percases ( 0 <= x or not 0 <= x ) ; caseA6: 0 <= x ; ::_thesis: (absreal | INT) . x is Element of NAT (absreal | INT) . x = abs x by A5, EUCLID:def_2 .= x by A6, ABSVALUE:def_1 ; hence (absreal | INT) . x is Element of NAT by A6, INT_1:3; ::_thesis: verum end; caseA7: not 0 <= x ; ::_thesis: (absreal | INT) . x is Element of NAT (absreal | INT) . x = abs x by A5, EUCLID:def_2 .= - x by A7, ABSVALUE:def_1 ; hence (absreal | INT) . x is Element of NAT by A7, INT_1:3; ::_thesis: verum end; end; end; hence y in NAT by A3; ::_thesis: verum end; then rng (absreal | INT) c= NAT by TARSKI:def_3; then reconsider f = absreal | INT as Function of the carrier of INT.Ring,NAT by A1, FUNCT_2:def_1, RELSET_1:4; take f ; ::_thesis: for a being Element of INT.Ring holds f . a = absreal . a thus for a being Element of INT.Ring holds f . a = absreal . a by FUNCT_1:49; ::_thesis: verum end; 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 proof deffunc H1( Element of INT.Ring) -> set = absreal . $1; thus for f1, f2 being Function of the carrier of INT.Ring,NAT st ( for x being Element of INT.Ring holds f1 . x = H1(x) ) & ( for x being Element of INT.Ring holds f2 . x = H1(x) ) holds f1 = f2 from BINOP_2:sch_1(); ::_thesis: verum end; 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 proof let a be Element of INT.Ring; ::_thesis: absint . a = abs a reconsider a9 = a as Integer ; absint . a = absreal . a9 by Def5 .= abs a9 by EUCLID:def_2 ; hence absint . a = abs a ; ::_thesis: verum end; Lm5: for a being Integer holds ( a = 0 or absreal . a >= 1 ) proof let a be Integer; ::_thesis: ( a = 0 or absreal . a >= 1 ) assume A1: a <> 0 ; ::_thesis: absreal . a >= 1 now__::_thesis:_(_(_0_<=_a_&_absreal_._a_>=_1_)_or_(_a_<_0_&_absreal_._a_>=_1_)_) percases ( 0 <= a or a < 0 ) ; case 0 <= a ; ::_thesis: absreal . a >= 1 then reconsider a = a as Element of NAT by INT_1:3; A2: absreal . a = abs a by EUCLID:def_2 .= a by ABSVALUE:def_1 ; 0 + 1 < a + 1 by A1, XREAL_1:6; hence absreal . a >= 1 by A2, NAT_1:13; ::_thesis: verum end; caseA3: a < 0 ; ::_thesis: absreal . a >= 1 then a <= - 1 by INT_1:8; then A4: - (- 1) <= - a by XREAL_1:24; absreal . a = abs a by EUCLID:def_2 .= - a by A3, ABSVALUE:def_1 ; hence absreal . a >= 1 by A4; ::_thesis: verum end; end; end; hence absreal . a >= 1 ; ::_thesis: verum end; 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 ) ) proof let a, b be Element of INT.Ring; ::_thesis: ( b <> 0. INT.Ring implies 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 ) ) ) assume A1: b <> 0. INT.Ring ; ::_thesis: 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 ) ) reconsider a9 = a as Integer ; let b9 be Integer; ::_thesis: ( b9 = b & 0 <= b9 implies ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ) assume A2: b9 = b ; ::_thesis: ( not 0 <= b9 or ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ) defpred S1[ Nat] means ex s being Integer st $1 = a9 - (s * b9); assume A3: 0 <= b9 ; ::_thesis: ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) A4: ex k being Nat st S1[k] proof now__::_thesis:_(_(_0_<=_a9_&_ex_k_being_Nat_st_S1[k]_)_or_(_a9_<_0_&_ex_k_being_Nat_st_S1[k]_)_) percases ( 0 <= a9 or a9 < 0 ) ; case 0 <= a9 ; ::_thesis: ex k being Nat st S1[k] then reconsider a9 = a9 as Element of NAT by INT_1:3; a9 - (0 * b9) = a9 ; hence ex k being Nat st S1[k] ; ::_thesis: verum end; caseA5: a9 < 0 ; ::_thesis: ex k being Nat st S1[k] 1 + 0 <= b9 by A1, A2, A3, Lm3, INT_1:7; then 1 - 1 <= b9 - 1 by XREAL_1:9; then reconsider m = b9 - 1 as Element of NAT by INT_1:3; reconsider n = - a9 as Element of NAT by A5, INT_1:3; ( a9 - (a9 * b9) = (- a9) * (b9 - 1) & n * m is Element of NAT ) ; hence ex k being Nat st S1[k] ; ::_thesis: verum end; end; end; hence ex k being Nat st S1[k] ; ::_thesis: verum end; ex k being Nat st ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A4); then consider k9 being Nat such that A6: ex s being Integer st ( k9 = a9 - (s * b9) & ( for n being Nat st ex s9 being Integer st n = a9 - (s9 * b9) holds k9 <= n ) ) ; consider l9 being Integer such that A7: k9 = a9 - (l9 * b9) by A6; reconsider k = k9, l = l9 as Element of INT.Ring by INT_1:def_2; A8: ( k9 = 0 or k9 < b9 ) proof assume k9 <> 0 ; ::_thesis: k9 < b9 assume b9 <= k9 ; ::_thesis: contradiction then reconsider k = k9 - b9 as Element of NAT by INT_1:5; A9: k9 > k proof reconsider b9 = b9 as Element of NAT by A3, INT_1:3; assume k9 <= k ; ::_thesis: contradiction then consider x being Nat such that A10: k = k9 + x by NAT_1:10; - x = b9 by A10; hence contradiction by A1, A2, Lm2, FUNCT_7:def_1; ::_thesis: verum end; k9 - b9 = a9 - ((l9 + 1) * b9) by A7; hence contradiction by A6, A9; ::_thesis: verum end; A11: ( k = 0. INT.Ring or absint . k < absint . b ) proof reconsider b9 = b9 as Element of NAT by A3, INT_1:3; assume A12: k <> 0. INT.Ring ; ::_thesis: absint . k < absint . b A13: absint . k = absreal . k by Def5 .= abs k9 by EUCLID:def_2 .= k9 by ABSVALUE:def_1 ; absint . b = absreal . b9 by A2, Def5 .= abs b9 by EUCLID:def_2 .= b9 by ABSVALUE:def_1 ; hence absint . k < absint . b by A8, A12, A13, FUNCT_7:def_1; ::_thesis: verum end; k + (l * b) = a by A2, A7; hence ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A11; ::_thesis: verum end; 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 ) proof let a, b be Element of INT.Ring; ::_thesis: ( b <> 0. INT.Ring implies 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 ) ) assume A1: b <> 0. INT.Ring ; ::_thesis: 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 ) reconsider a9 = a as Integer ; let b9 be Integer; ::_thesis: ( b9 = b & 0 <= b9 implies ex q, r being Element of INT.Ring st ( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) ) assume A2: b9 = b ; ::_thesis: ( not 0 <= b9 or ex q, r being Element of INT.Ring st ( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) ) defpred S1[ Nat] means ex s being Integer st $1 = a9 - (s * b9); assume A3: 0 <= b9 ; ::_thesis: ex q, r being Element of INT.Ring st ( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) A4: ex k being Nat st S1[k] proof now__::_thesis:_(_(_0_<=_a9_&_ex_k_being_Nat_st_S1[k]_)_or_(_a9_<_0_&_ex_k_being_Nat_st_S1[k]_)_) percases ( 0 <= a9 or a9 < 0 ) ; case 0 <= a9 ; ::_thesis: ex k being Nat st S1[k] then reconsider a9 = a9 as Element of NAT by INT_1:3; a9 - (0 * b9) = a9 ; hence ex k being Nat st S1[k] ; ::_thesis: verum end; caseA5: a9 < 0 ; ::_thesis: ex k being Nat st S1[k] 1 + 0 <= b9 by A1, A2, A3, Lm3, INT_1:7; then 1 - 1 <= b9 - 1 by XREAL_1:9; then reconsider m = b9 - 1 as Element of NAT by INT_1:3; reconsider n = - a9 as Element of NAT by A5, INT_1:3; ( a9 - (a9 * b9) = (- a9) * (b9 - 1) & n * m is Element of NAT ) ; hence ex k being Nat st S1[k] ; ::_thesis: verum end; end; end; hence ex k being Nat st S1[k] ; ::_thesis: verum end; ex k being Nat st ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A4); then consider k9 being Nat such that A6: ex s being Integer st ( k9 = a9 - (s * b9) & ( for n being Nat st ex s9 being Integer st n = a9 - (s9 * b9) holds k9 <= n ) ) ; consider l9 being Integer such that A7: k9 = a9 - (l9 * b9) by A6; reconsider k = k9, l = l9 as Element of INT.Ring by INT_1:def_2; A8: ( k9 = 0 or k9 < b9 ) proof assume k9 <> 0 ; ::_thesis: k9 < b9 assume b9 <= k9 ; ::_thesis: contradiction then reconsider k = k9 - b9 as Element of NAT by INT_1:5; A9: k9 > k proof reconsider b9 = b9 as Element of NAT by A3, INT_1:3; assume k9 <= k ; ::_thesis: contradiction then consider x being Nat such that A10: k = k9 + x by NAT_1:10; - x = b9 by A10; hence contradiction by A1, A2, Lm2, FUNCT_7:def_1; ::_thesis: verum end; k9 - b9 = a9 - ((l9 + 1) * b9) by A7; hence contradiction by A6, A9; ::_thesis: verum end; A11: ( 0. INT.Ring <= k & k < abs b ) proof reconsider b9 = b9 as Element of NAT by A3, INT_1:3; reconsider k9 = k9 as Element of NAT by ORDINAL1:def_12; A12: absint . b = absreal . b9 by A2, Def5 .= abs b9 by EUCLID:def_2 .= b9 by ABSVALUE:def_1 ; now__::_thesis:_(_(_k9_=_0_&_0._INT.Ring_<=_k_&_k_<_abs_b_)_or_(_k9_<_b9_&_0._INT.Ring_<=_k_&_k_<_abs_b_)_) percases ( k9 = 0 or k9 < b9 ) by A8; case k9 = 0 ; ::_thesis: ( 0. INT.Ring <= k & k < abs b ) hence ( 0. INT.Ring <= k & k < abs b ) by A1, A2, A12, Lm3, Th1; ::_thesis: verum end; case k9 < b9 ; ::_thesis: ( 0. INT.Ring <= k & k < abs b ) hence ( 0. INT.Ring <= k & k < abs b ) by A12, Lm2, Th1, FUNCT_7:def_1; ::_thesis: verum end; end; end; hence ( 0. INT.Ring <= k & k < abs b ) ; ::_thesis: verum end; k + (l * b) = a by A2, A7; hence ex q, r being Element of INT.Ring st ( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) by A11; ::_thesis: verum end; 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 ) proof let a, b, q1, q2, r1, r2 be Element of INT.Ring; ::_thesis: ( 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 implies ( q1 = q2 & r1 = r2 ) ) assume that A1: b <> 0. INT.Ring and A2: a = (q1 * b) + r1 and A3: 0. INT.Ring <= r1 and A4: r1 < abs b and A5: a = (q2 * b) + r2 and A6: 0. INT.Ring <= r2 and A7: r2 < abs b ; ::_thesis: ( q1 = q2 & r1 = r2 ) reconsider r29 = r2 as Integer ; reconsider r19 = r1 as Integer ; reconsider q29 = q2 as Integer ; reconsider q19 = q1 as Integer ; reconsider b9 = b as Integer ; now__::_thesis:_(_(_0_<=_r19_-_r29_&_q1_=_q2_)_or_(_r19_-_r29_<_0_&_q1_=_q2_)_) percases ( 0 <= r19 - r29 or r19 - r29 < 0 ) ; caseA8: 0 <= r19 - r29 ; ::_thesis: q1 = q2 A9: (q29 - q19) * b9 = r19 - r29 by A2, A5; now__::_thesis:_(_(_0_=_r19_-_r29_&_q1_=_q2_)_or_(_0_<>_r19_-_r29_&_q1_=_q2_)_) percases ( 0 = r19 - r29 or 0 <> r19 - r29 ) ; case 0 = r19 - r29 ; ::_thesis: q1 = q2 then ( q29 - q19 = 0 or b9 = 0 ) by A9, XCMPLX_1:6; hence q1 = q2 by A1, FUNCT_7:def_1; ::_thesis: verum end; case 0 <> r19 - r29 ; ::_thesis: q1 = q2 then A10: 0 <> q29 - q19 by A9; A11: (absreal . (q29 - q19)) * (absreal . b9) >= absreal . b9 proof reconsider e = q2 + (- q1) as Element of INT.Ring ; reconsider d9 = q29 - q19 as Integer ; absreal . b9 = absint . b by Def5; then reconsider c = absreal . b9 as Element of NAT ; absreal . d9 = absint . e by Def5; then reconsider d = absreal . d9 as Element of NAT ; d * c >= 1 * c by A10, Lm5, NAT_1:4; hence (absreal . (q29 - q19)) * (absreal . b9) >= absreal . b9 ; ::_thesis: verum end; A12: r19 + (- r29) <= r19 + 0 by A6, Lm3, XREAL_1:6; A13: abs b = absint . b by Th1 .= absreal . b by Def5 ; r19 - r29 = abs ((q29 - q19) * b9) by A2, A5, A8, ABSVALUE:def_1 .= (abs (q29 - q19)) * (abs b9) by COMPLEX1:65 .= (absreal . (q29 - q19)) * (abs b9) by EUCLID:def_2 .= (absreal . (q29 - q19)) * (absreal . b9) by EUCLID:def_2 ; hence q1 = q2 by A4, A11, A12, A13, XXREAL_0:2; ::_thesis: verum end; end; end; hence q1 = q2 ; ::_thesis: verum end; caseA14: r19 - r29 < 0 ; ::_thesis: q1 = q2 ( - (r19 - r29) = r29 - r19 & (q19 - q29) * b9 = r29 - r19 ) by A2, A5; then A15: 0 <> q19 - q29 by A14, XREAL_1:58; A16: (absreal . (q19 - q29)) * (absreal . b9) >= absreal . b9 proof reconsider e = q1 + (- q2) as Element of INT.Ring ; reconsider d9 = q19 - q29 as Integer ; absreal . b9 = absint . b by Def5; then reconsider c = absreal . b9 as Element of NAT ; absreal . d9 = absint . e by Def5; then reconsider d = absreal . d9 as Element of NAT ; d * c >= 1 * c by A15, Lm5, NAT_1:4; hence (absreal . (q19 - q29)) * (absreal . b9) >= absreal . b9 ; ::_thesis: verum end; A17: abs b = absint . b by Th1 .= absreal . b by Def5 ; - (r19 - r29) > 0 by A14, XREAL_1:58; then A18: r29 - r19 = abs ((q19 - q29) * b9) by A2, A5, ABSVALUE:def_1 .= (abs (q19 - q29)) * (abs b9) by COMPLEX1:65 .= (absreal . (q19 - q29)) * (abs b9) by EUCLID:def_2 .= (absreal . (q19 - q29)) * (absreal . b9) by EUCLID:def_2 ; r29 + (- r19) <= r29 + 0 by A3, Lm3, XREAL_1:6; hence q1 = q2 by A7, A16, A17, A18, XXREAL_0:2; ::_thesis: verum end; end; end; hence ( q1 = q2 & r1 = r2 ) by A2, A5; ::_thesis: verum end; 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 ) proof reconsider b9 = b as Integer ; now__::_thesis:_(_(_0_<=_b9_&_ex_b1,_r_being_Element_of_INT.Ring_st_ (_a_=_(b1_*_b)_+_r_&_0._INT.Ring_<=_r_&_r_<_abs_b_)_)_or_(_b9_<_0_&_ex_b1,_r_being_Element_of_INT.Ring_st_ (_a_=_(b1_*_b)_+_r_&_0._INT.Ring_<=_r_&_r_<_abs_b_)_)_) percases ( 0 <= b9 or b9 < 0 ) ; case 0 <= b9 ; ::_thesis: ex b1, r being Element of INT.Ring st ( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b ) hence ex b1, r being Element of INT.Ring st ( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b ) by A1, Lm7; ::_thesis: verum end; caseA2: b9 < 0 ; ::_thesis: ex b1, r being Element of INT.Ring st ( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b ) reconsider c = - b9 as Element of INT.Ring ; 0 < - b9 by A2, XREAL_1:58; then consider q, r being Element of INT.Ring such that A3: a = (q * c) + r and A4: 0. INT.Ring <= r and A5: r < abs c by Lm3, Lm7; reconsider t = - q as Element of INT.Ring ; A6: (t * b) + r = a by A3; absint . c = absreal . c by Def5 .= abs (- b9) by EUCLID:def_2 .= - b9 by A2, ABSVALUE:def_1 .= abs b9 by A2, ABSVALUE:def_1 .= absreal . b9 by EUCLID:def_2 .= absint . b by Def5 .= abs b by Th1 ; then r < abs b by A5, Th1; hence ex b1, r being Element of INT.Ring st ( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b ) by A4, A6; ::_thesis: verum end; end; end; hence ex b1, r being Element of INT.Ring st ( a = (b1 * b) + r & 0. INT.Ring <= r & r < abs b ) ; ::_thesis: verum end; 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 ) proof reconsider b9 = b as Integer ; now__::_thesis:_(_(_0_<=_b9_&_ex_b1,_q_being_Element_of_INT.Ring_st_ (_a_=_(q_*_b)_+_b1_&_0._INT.Ring_<=_b1_&_b1_<_abs_b_)_)_or_(_b9_<_0_&_ex_b1,_q_being_Element_of_INT.Ring_st_ (_a_=_(q_*_b)_+_b1_&_0._INT.Ring_<=_b1_&_b1_<_abs_b_)_)_) percases ( 0 <= b9 or b9 < 0 ) ; case 0 <= b9 ; ::_thesis: ex b1, q being Element of INT.Ring st ( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b ) then ex q, r being Element of INT.Ring st ( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) by A1, Lm7; hence ex b1, q being Element of INT.Ring st ( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b ) ; ::_thesis: verum end; caseA2: b9 < 0 ; ::_thesis: ex b1, q being Element of INT.Ring st ( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b ) reconsider c = - b9 as Element of INT.Ring ; 0 < - b9 by A2, XREAL_1:58; then consider q, r being Element of INT.Ring such that A3: a = (q * c) + r and A4: 0. INT.Ring <= r and A5: r < abs c by Lm3, Lm7; reconsider t = - q as Element of INT.Ring ; A6: (t * b) + r = a by A3; absint . c = absreal . c by Def5 .= abs (- b9) by EUCLID:def_2 .= - b9 by A2, ABSVALUE:def_1 .= abs b9 by A2, ABSVALUE:def_1 .= absreal . b9 by EUCLID:def_2 .= absint . b by Def5 .= abs b by Th1 ; then r < abs b by A5, Th1; hence ex b1, q being Element of INT.Ring st ( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b ) by A4, A6; ::_thesis: verum end; end; end; hence ex b1, q being Element of INT.Ring st ( a = (q * b) + b1 & 0. INT.Ring <= b1 & b1 < abs b ) ; ::_thesis: verum end; 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) proof let a, b be Element of INT.Ring; ::_thesis: ( b <> 0. INT.Ring implies a = ((a div b) * b) + (a mod b) ) consider d being Element of INT.Ring such that A1: d = a div b ; assume A2: b <> 0. INT.Ring ; ::_thesis: a = ((a div b) * b) + (a mod b) then ex r being Element of INT.Ring st ( a = (d * b) + r & 0. INT.Ring <= r & r < abs b ) by A1, Def6; hence a = ((a div b) * b) + (a mod b) by A2, A1, Def7; ::_thesis: verum end; 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 proof take absint ; :: according to INT_3:def_8 ::_thesis: for a, b being Element of INT.Ring st b <> 0. INT.Ring holds ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) let a, b be Element of INT.Ring; ::_thesis: ( b <> 0. INT.Ring implies ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ) reconsider b9 = b as Integer ; assume A1: b <> 0. INT.Ring ; ::_thesis: ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) now__::_thesis:_(_(_0_<=_b9_&_ex_q,_r_being_Element_of_INT.Ring_st_ (_a_=_(q_*_b)_+_r_&_(_r_=_0._INT.Ring_or_absint_._r_<_absint_._b_)_)_)_or_(_b9_<_0_&_ex_q,_r_being_Element_of_INT.Ring_st_ (_a_=_(q_*_b)_+_r_&_(_r_=_0._INT.Ring_or_absint_._r_<_absint_._b_)_)_)_) percases ( 0 <= b9 or b9 < 0 ) ; case 0 <= b9 ; ::_thesis: ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) hence ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A1, Lm6; ::_thesis: verum end; caseA2: b9 < 0 ; ::_thesis: ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) reconsider c = - b9 as Element of INT.Ring ; 0 < - b9 by A2, XREAL_1:58; then consider q, r being Element of INT.Ring such that A3: a = (q * c) + r and A4: ( r = 0. INT.Ring or absint . r < absint . c ) by Lm3, Lm6; A5: ( r = 0. INT.Ring or absint . r < absint . b ) proof assume A6: r <> 0. INT.Ring ; ::_thesis: absint . r < absint . b absint . c = absreal . c by Def5 .= abs (- b9) by EUCLID:def_2 .= - b9 by A2, ABSVALUE:def_1 .= abs b9 by A2, ABSVALUE:def_1 .= absreal . b9 by EUCLID:def_2 .= absint . b by Def5 ; hence absint . r < absint . b by A4, A6; ::_thesis: verum end; reconsider t = - q as Element of INT.Ring ; (t * b) + r = a by A3; hence ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A5; ::_thesis: verum end; end; end; hence ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ; ::_thesis: verum end; 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 ) ) proof let F be non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr ; ::_thesis: 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 ) ) let f be Function of the carrier of F,NAT; ::_thesis: 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 ) ) now__::_thesis:_for_a,_b_being_Element_of_F_st_b_<>_0._F_&_b_<>_0._F_holds_ ex_q,_r_being_Element_of_F_st_ (_a_=_(q_*_b)_+_r_&_(_r_=_0._F_or_f_._r_<_f_._b_)_) let a, b be Element of F; ::_thesis: ( b <> 0. F & b <> 0. F implies ex q, r being Element of F st ( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) ) assume A1: b <> 0. F ; ::_thesis: ( b <> 0. F implies ex q, r being Element of F st ( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) ) ex q, r being Element of F st ( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) proof consider x being Element of F such that A2: x * b = 1. F by A1, VECTSP_1:def_9; ((a * x) * b) + (0. F) = (a * (1. F)) + (0. F) by A2, GROUP_1:def_3 .= a + (0. F) by VECTSP_1:def_6 .= a by RLVECT_1:def_4 ; hence ex q, r being Element of F st ( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) ; ::_thesis: verum end; hence ( b <> 0. F implies ex q, r being Element of F st ( a = (q * b) + r & ( r = 0. F or f . r < f . b ) ) ) ; ::_thesis: verum end; hence 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 ) ) ; ::_thesis: verum end; 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 ) proof take INT.Ring ; ::_thesis: ( INT.Ring is strict & INT.Ring is Euclidian & INT.Ring is domRing-like & not INT.Ring is degenerated & INT.Ring is distributive & INT.Ring is commutative ) thus ( INT.Ring is strict & INT.Ring is Euclidian & INT.Ring is domRing-like & not INT.Ring is degenerated & INT.Ring is distributive & INT.Ring is commutative ) ; ::_thesis: verum end; 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 proof take INT.Ring ; ::_thesis: INT.Ring is strict thus INT.Ring is strict ; ::_thesis: verum end; 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 proof let E be EuclidianRing; ::_thesis: E is gcdDomain set d = the DegreeFunction of E; now__::_thesis:_for_x,_y_being_Element_of_E_ex_z_being_Element_of_E_st_ (_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_E_st_zz_divides_x_&_zz_divides_y_holds_ zz_divides_z_)_) let x, y be Element of E; ::_thesis: ex z being Element of E st ( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds zz divides z ) ) now__::_thesis:_(_(_x_=_0._E_&_ex_z_being_Element_of_E_st_ (_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_E_st_zz_divides_x_&_zz_divides_y_holds_ zz_divides_z_)_)_)_or_(_x_<>_0._E_&_ex_z_being_Element_of_E_st_ (_z_divides_x_&_z_divides_y_&_(_for_zz_being_Element_of_E_st_zz_divides_x_&_zz_divides_y_holds_ zz_divides_z_)_)_)_) percases ( x = 0. E or x <> 0. E ) ; caseA1: x = 0. E ; ::_thesis: ex z being Element of E st ( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds zz divides z ) ) y * (0. E) = 0. E by VECTSP_1:6; then A2: y divides 0. E by GCD_1:def_1; for zz being Element of E st zz divides x & zz divides y holds zz divides y ; hence ex z being Element of E st ( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds zz divides z ) ) by A1, A2; ::_thesis: verum end; caseA3: x <> 0. E ; ::_thesis: ex z being Element of E st ( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds zz divides z ) ) set M = { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; defpred S1[ Nat] means ex z being Element of E st ( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & z <> 0. E & $1 = the DegreeFunction of E . z ); ((1. E) * x) + ((0. E) * y) = ((1. E) * x) + (0. E) by VECTSP_1:7 .= (1. E) * x by RLVECT_1:def_4 .= x by VECTSP_1:def_6 ; then A4: x in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; ex k being Element of NAT st k = the DegreeFunction of E . x ; then A5: ex k being Nat st S1[k] by A3, A4; ex k being Nat st ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A5); then consider k being Nat such that A6: ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) ; consider g being Element of E such that A7: g in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } and A8: g <> 0. E and A9: ( k = the DegreeFunction of E . g & ( for n being Nat st ex z being Element of E st ( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } & z <> 0. E & n = the DegreeFunction of E . z ) holds k <= n ) ) by A6; set G = { z where z is Element of E : ex r being Element of E st z = r * g } ; A10: for z being set st z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } holds z in { z where z is Element of E : ex r being Element of E st z = r * g } proof let z be set ; ::_thesis: ( z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } implies z in { z where z is Element of E : ex r being Element of E st z = r * g } ) assume z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; ::_thesis: z in { z where z is Element of E : ex r being Element of E st z = r * g } then consider z2 being Element of E such that A11: z = z2 and A12: ex s, t being Element of E st z2 = (s * x) + (t * y) ; consider u, v being Element of E such that A13: z2 = (u * x) + (v * y) by A12; reconsider z = z as Element of E by A11; consider q, r being Element of E such that A14: z = (q * g) + r and A15: ( r = 0. E or the DegreeFunction of E . r < the DegreeFunction of E . g ) by A8, Def9; r in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } proof consider z1 being Element of E such that A16: g = z1 and A17: ex s, t being Element of E st z1 = (s * x) + (t * y) by A7; consider s, t being Element of E such that A18: z1 = (s * x) + (t * y) by A17; z + (- (q * g)) = r + ((q * g) + (- (q * g))) by A14, RLVECT_1:def_3 .= r + (0. E) by RLVECT_1:def_10 .= r by RLVECT_1:def_4 ; then r = z + (- ((q * (s * x)) + (q * (t * y)))) by A16, A18, VECTSP_1:def_7 .= z + ((- (q * (s * x))) + (- (q * (t * y)))) by RLVECT_1:31 .= (((u * x) + (v * y)) + (- (q * (s * x)))) + (- (q * (t * y))) by A11, A13, RLVECT_1:def_3 .= (((u * x) + (- (q * (s * x)))) + (v * y)) + (- (q * (t * y))) by RLVECT_1:def_3 .= ((u * x) + (- (q * (s * x)))) + ((v * y) + (- (q * (t * y)))) by RLVECT_1:def_3 .= ((u * x) + ((- q) * (s * x))) + ((v * y) + (- (q * (t * y)))) by GCD_1:48 .= ((u * x) + ((- q) * (s * x))) + ((v * y) + ((- q) * (t * y))) by GCD_1:48 .= ((u * x) + (((- q) * s) * x)) + ((v * y) + ((- q) * (t * y))) by GROUP_1:def_3 .= ((u * x) + (((- q) * s) * x)) + ((v * y) + (((- q) * t) * y)) by GROUP_1:def_3 .= ((u + ((- q) * s)) * x) + ((v * y) + (((- q) * t) * y)) by VECTSP_1:def_7 .= ((u + ((- q) * s)) * x) + ((v + ((- q) * t)) * y) by VECTSP_1:def_7 ; hence r in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; ::_thesis: verum end; then r = 0. E by A9, A15; then z = q * g by A14, RLVECT_1:def_4; hence z in { z where z is Element of E : ex r being Element of E st z = r * g } ; ::_thesis: verum end; A19: for z being Element of E st z divides x & z divides y holds z divides g proof let z be Element of E; ::_thesis: ( z divides x & z divides y implies z divides g ) assume that A20: z divides x and A21: z divides y ; ::_thesis: z divides g consider u being Element of E such that A22: x = z * u by A20, GCD_1:def_1; consider zz being Element of E such that A23: g = zz and A24: ex s, t being Element of E st zz = (s * x) + (t * y) by A7; consider s, t being Element of E such that A25: zz = (s * x) + (t * y) by A24; consider v being Element of E such that A26: y = z * v by A21, GCD_1:def_1; g = ((s * u) * z) + (t * (v * z)) by A22, A26, A23, A25, GROUP_1:def_3 .= ((s * u) * z) + ((t * v) * z) by GROUP_1:def_3 .= ((s * u) + (t * v)) * z by VECTSP_1:def_7 ; hence z divides g by GCD_1:def_1; ::_thesis: verum end; ((0. E) * x) + ((1. E) * y) = (0. E) + ((1. E) * y) by VECTSP_1:7 .= (1. E) * y by RLVECT_1:4 .= y by VECTSP_1:def_6 ; then A27: y in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; for z being set st z in { z where z is Element of E : ex r being Element of E st z = r * g } holds z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } proof let z be set ; ::_thesis: ( z in { z where z is Element of E : ex r being Element of E st z = r * g } implies z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ) assume z in { z where z is Element of E : ex r being Element of E st z = r * g } ; ::_thesis: z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } then consider z2 being Element of E such that A28: z = z2 and A29: ex s being Element of E st z2 = s * g ; reconsider z = z as Element of E by A28; consider u being Element of E such that A30: z2 = u * g by A29; consider z1 being Element of E such that A31: g = z1 and A32: ex s, t being Element of E st z1 = (s * x) + (t * y) by A7; consider s, t being Element of E such that A33: z1 = (s * x) + (t * y) by A32; z = (u * (s * x)) + (u * (t * y)) by A28, A30, A31, A33, VECTSP_1:def_2 .= ((u * s) * x) + (u * (t * y)) by GROUP_1:def_3 .= ((u * s) * x) + ((u * t) * y) by GROUP_1:def_3 ; hence z in { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } ; ::_thesis: verum end; then A34: { z where z is Element of E : ex s, t being Element of E st z = (s * x) + (t * y) } = { z where z is Element of E : ex r being Element of E st z = r * g } by A10, TARSKI:1; ( g divides x & g divides y ) proof ( ex zz being Element of E st ( x = zz & ex r being Element of E st zz = r * g ) & ex zzz being Element of E st ( y = zzz & ex r being Element of E st zzz = r * g ) ) by A4, A27, A34; hence ( g divides x & g divides y ) by GCD_1:def_1; ::_thesis: verum end; hence ex z being Element of E st ( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds zz divides z ) ) by A19; ::_thesis: verum end; end; end; hence ex z being Element of E st ( z divides x & z divides y & ( for zz being Element of E st zz divides x & zz divides y holds zz divides z ) ) ; ::_thesis: verum end; hence E is gcdDomain by GCD_1:def_11; ::_thesis: verum end; 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 proof for a, b being Element of INT.Ring st b <> 0. INT.Ring holds ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) proof let a, b be Element of INT.Ring; ::_thesis: ( b <> 0. INT.Ring implies ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ) reconsider b9 = b as Integer ; assume A1: b <> 0. INT.Ring ; ::_thesis: ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) now__::_thesis:_(_(_0_<=_b9_&_ex_q,_r_being_Element_of_INT.Ring_st_ (_a_=_(q_*_b)_+_r_&_(_r_=_0._INT.Ring_or_absint_._r_<_absint_._b_)_)_)_or_(_b9_<_0_&_ex_q,_r_being_Element_of_INT.Ring_st_ (_a_=_(q_*_b)_+_r_&_(_r_=_0._INT.Ring_or_absint_._r_<_absint_._b_)_)_)_) percases ( 0 <= b9 or b9 < 0 ) ; case 0 <= b9 ; ::_thesis: ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) hence ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A1, Lm6; ::_thesis: verum end; caseA2: b9 < 0 ; ::_thesis: ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) reconsider c = - b9 as Element of INT.Ring ; 0 < - b9 by A2, XREAL_1:58; then consider q, r being Element of INT.Ring such that A3: a = (q * c) + r and A4: ( r = 0. INT.Ring or absint . r < absint . c ) by Lm3, Lm6; A5: ( r = 0. INT.Ring or absint . r < absint . b ) proof assume A6: r <> 0. INT.Ring ; ::_thesis: absint . r < absint . b absint . c = absreal . c by Def5 .= abs (- b9) by EUCLID:def_2 .= - b9 by A2, ABSVALUE:def_1 .= abs b9 by A2, ABSVALUE:def_1 .= absreal . b9 by EUCLID:def_2 .= absint . b by Def5 ; hence absint . r < absint . b by A4, A6; ::_thesis: verum end; reconsider t = - q as Element of INT.Ring ; (t * b) + r = a by A3; hence ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A5; ::_thesis: verum end; end; end; hence ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ; ::_thesis: verum end; hence absint is DegreeFunction of INT.Ring by Def9; ::_thesis: verum end; 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 proof let F be non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr ; ::_thesis: F is Euclidian set f = the 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 the Function of the carrier of F,NAT . r < the Function of the carrier of F,NAT . b ) ) by Lm8; hence F is Euclidian by Def8; ::_thesis: verum end; 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 proof let F be non empty almost_left_invertible associative commutative right_zeroed well-unital doubleLoopStr ; ::_thesis: for f being Function of the carrier of F,NAT holds f is DegreeFunction of F let f be Function of the carrier of F,NAT; ::_thesis: f is DegreeFunction of F 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 ) ) by Lm8; hence f is DegreeFunction of F by Def9; ::_thesis: verum end; 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 proof reconsider n = n as non zero Nat by A1; defpred S1[ Element of Segm n, Element of Segm n, set ] means $3 = ($1 * $2) mod n; A1: for k, l being Element of Segm n ex c being Element of Segm n st S1[k,l,c] proof let k, l be Element of Segm n; ::_thesis: ex c being Element of Segm n st S1[k,l,c] reconsider k9 = k, l9 = l as Element of NAT ; (k9 * l9) mod n < n by NAT_D:1; then reconsider c = (k9 * l9) mod n as Element of Segm n by NAT_1:44; take c ; ::_thesis: S1[k,l,c] thus S1[k,l,c] ; ::_thesis: verum end; ex c being BinOp of (Segm n) st for k, l being Element of Segm n holds S1[k,l,c . (k,l)] from BINOP_1:sch_3(A1); hence ex b1 being BinOp of (Segm n) st for k, l being Element of Segm n holds b1 . (k,l) = (k * l) mod n ; ::_thesis: verum end; 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 proof reconsider n = n as non zero Nat by A1; deffunc H1( Element of Segm n, Element of Segm n) -> Element of NAT = ($1 * $2) mod n; for o1, o2 being BinOp of (Segm n) st ( for a, b being Element of Segm n holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Segm n holds o2 . (a,b) = H1(a,b) ) holds o1 = o2 from BINOP_2:sch_2(); hence 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 ; ::_thesis: verum end; 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 proof reconsider n = n as non zero Nat by A1; set f = { [k,((n - k) mod n)] where k is Element of NAT : k < n } ; A1: for x being set st x in { [k,((n - k) mod n)] where k is Element of NAT : k < n } holds ex y, z being set st x = [y,z] proof let x be set ; ::_thesis: ( x in { [k,((n - k) mod n)] where k is Element of NAT : k < n } implies ex y, z being set st x = [y,z] ) assume x in { [k,((n - k) mod n)] where k is Element of NAT : k < n } ; ::_thesis: ex y, z being set st x = [y,z] then ex k being Element of NAT st ( x = [k,((n - k) mod n)] & k < n ) ; hence ex y, z being set st x = [y,z] ; ::_thesis: verum end; for x, y1, y2 being set st [x,y1] in { [k,((n - k) mod n)] where k is Element of NAT : k < n } & [x,y2] in { [k,((n - k) mod n)] where k is Element of NAT : k < n } holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: ( [x,y1] in { [k,((n - k) mod n)] where k is Element of NAT : k < n } & [x,y2] in { [k,((n - k) mod n)] where k is Element of NAT : k < n } implies y1 = y2 ) assume that A2: [x,y1] in { [k,((n - k) mod n)] where k is Element of NAT : k < n } and A3: [x,y2] in { [k,((n - k) mod n)] where k is Element of NAT : k < n } ; ::_thesis: y1 = y2 consider k being Element of NAT such that A4: [x,y1] = [k,((n - k) mod n)] and k < n by A2; A5: y1 = (n - k) mod n by A4, XTUPLE_0:1; consider k9 being Element of NAT such that A6: [x,y2] = [k9,((n - k9) mod n)] and k9 < n by A3; A7: y2 = (n - k9) mod n by A6, XTUPLE_0:1; k = x by A4, XTUPLE_0:1 .= k9 by A6, XTUPLE_0:1 ; hence y1 = y2 by A5, A7; ::_thesis: verum end; then reconsider f = { [k,((n - k) mod n)] where k is Element of NAT : k < n } as Function by A1, FUNCT_1:def_1, RELAT_1:def_1; A8: for x being set st x in Segm n holds x in dom f proof let x be set ; ::_thesis: ( x in Segm n implies x in dom f ) assume A9: x in Segm n ; ::_thesis: x in dom f then reconsider x = x as Element of NAT ; x < n by A9, NAT_1:44; then [x,((n - x) mod n)] in f ; hence x in dom f by XTUPLE_0:def_12; ::_thesis: verum end; for x being set st x in dom f holds x in Segm n proof let x be set ; ::_thesis: ( x in dom f implies x in Segm n ) assume x in dom f ; ::_thesis: x in Segm n then consider y being set such that A10: [x,y] in f by XTUPLE_0:def_12; consider k being Element of NAT such that A11: [x,y] = [k,((n - k) mod n)] and A12: k < n by A10; x = k by A11, XTUPLE_0:1; hence x in Segm n by A12, NAT_1:44; ::_thesis: verum end; then A13: dom f = Segm n by A8, TARSKI:1; for y being set st y in rng f holds y in Segm n proof let y be set ; ::_thesis: ( y in rng f implies y in Segm n ) assume y in rng f ; ::_thesis: y in Segm n then consider x being set such that A14: [x,y] in f by XTUPLE_0:def_13; consider k being Element of NAT such that A15: [x,y] = [k,((n - k) mod n)] and A16: k < n by A14; k - k < n - k by A16, XREAL_1:9; then reconsider z = n - k as Element of NAT by INT_1:3; A17: z mod n < n by NAT_D:1; y = (n - k) mod n by A15, XTUPLE_0:1; hence y in Segm n by A17, NAT_1:44; ::_thesis: verum end; then rng f c= Segm n by TARSKI:def_3; then reconsider f = f as UnOp of (Segm n) by A13, FUNCT_2:def_1, RELSET_1:4; for k being Element of Segm n holds f . k = (n - k) mod n proof let k be Element of Segm n; ::_thesis: f . k = (n - k) mod n reconsider k = k as Element of NAT ; k < n by NAT_1:44; then [k,((n - k) mod n)] in f ; hence f . k = (n - k) mod n by A13, FUNCT_1:def_2; ::_thesis: verum end; hence ex b1 being UnOp of (Segm n) st for k being Element of Segm n holds b1 . k = (n - k) mod n ; ::_thesis: verum end; 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 proof reconsider n = n as non zero Nat by A1; deffunc H1( Element of Segm n) -> set = (n - $1) mod n; for f1, f2 being UnOp of (Segm n) st ( for a being Element of Segm n holds f1 . a = H1(a) ) & ( for a being Element of Segm n holds f2 . a = H1(a) ) holds f1 = f2 from LMOD_7:sch_2(); hence 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 ; ::_thesis: verum end; 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 ) ) proof let n be Nat; ::_thesis: ( n > 0 implies 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 ) ) ) assume A1: n > 0 ; ::_thesis: 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 ) ) let a, b be Element of Segm n; ::_thesis: ( ( 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 ) ) reconsider n = n as non zero Nat by A1; consider c being Element of NAT such that A2: c = (a + b) mod n ; consider t being Nat such that A3: ( ( a + b = (n * t) + c & c < n ) or ( c = 0 & n = 0 ) ) by A2, NAT_D:def_2; A4: now__::_thesis:_(_a_+_b_>=_n_implies_(addint_n)_._(a,b)_=_(a_+_b)_-_n_) assume A5: a + b >= n ; ::_thesis: (addint n) . (a,b) = (a + b) - n t = 1 proof now__::_thesis:_(_(_t_=_0_&_t_=_1_)_or_(_t_<>_0_&_t_=_1_)_) percases ( t = 0 or t <> 0 ) ; case t = 0 ; ::_thesis: t = 1 hence t = 1 by A3, A5; ::_thesis: verum end; caseA6: t <> 0 ; ::_thesis: t = 1 t < 2 proof ( a < n & b < n ) by NAT_1:44; then A7: ( (n * t) + c >= n * t & a + b < (n * 1) + (n * 1) ) by NAT_1:11, XREAL_1:8; assume t >= 2 ; ::_thesis: contradiction then n * t >= n * 2 by XREAL_1:64; hence contradiction by A3, A7, XXREAL_0:2; ::_thesis: verum end; then t < 1 + 1 ; then A8: t <= 1 by NAT_1:13; 1 + 0 <= t by A6, INT_1:7; hence t = 1 by A8, XXREAL_0:1; ::_thesis: verum end; end; end; hence t = 1 ; ::_thesis: verum end; hence (addint n) . (a,b) = (a + b) - n by A2, A3, GR_CY_1:def_4; ::_thesis: verum end; A9: ( (addint n) . (a,b) = (a + b) - n implies a + b >= n ) proof assume (addint n) . (a,b) = (a + b) - n ; ::_thesis: a + b >= n then A10: (a + b) mod n = (a + b) - n by GR_CY_1:def_4; consider t being Nat such that A11: a + b = (n * t) + ((a + b) mod n) and (a + b) mod n < n by NAT_D:def_2; assume A12: a + b < n ; ::_thesis: contradiction t = 0 proof assume t <> 0 ; ::_thesis: contradiction then 1 + 0 <= t by INT_1:7; then A13: 1 * n <= t * n by XREAL_1:64; t * n <= (t * n) + ((a + b) mod n) by NAT_1:11; hence contradiction by A12, A11, A13, XXREAL_0:2; ::_thesis: verum end; hence contradiction by A10, A11; ::_thesis: verum end; A14: now__::_thesis:_(_a_+_b_<_n_implies_(addint_n)_._(a,b)_=_a_+_b_) assume A15: a + b < n ; ::_thesis: (addint n) . (a,b) = a + b t = 0 proof assume t <> 0 ; ::_thesis: contradiction then 1 + 0 <= t by INT_1:7; then A16: 1 * n <= t * n by XREAL_1:64; n * t <= (n * t) + c by NAT_1:11; hence contradiction by A3, A15, A16, XXREAL_0:2; ::_thesis: verum end; hence (addint n) . (a,b) = a + b by A2, A3, GR_CY_1:def_4; ::_thesis: verum end; ( (addint n) . (a,b) = a + b implies a + b < n ) proof assume (addint n) . (a,b) = a + b ; ::_thesis: a + b < n then (a + b) mod n = a + b by GR_CY_1:def_4; hence a + b < n by NAT_D:1; ::_thesis: verum end; hence ( ( 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 ) ) by A14, A9, A4; ::_thesis: verum end; Lm9: for a, b being Nat st b <> 0 holds ex k being Element of NAT st ( k * b <= a & a < (k + 1) * b ) proof let a, b be Nat; ::_thesis: ( b <> 0 implies ex k being Element of NAT st ( k * b <= a & a < (k + 1) * b ) ) set k9 = a div b; assume b <> 0 ; ::_thesis: ex k being Element of NAT st ( k * b <= a & a < (k + 1) * b ) then A1: ex t being Nat st ( a = (b * (a div b)) + t & t < b ) by NAT_D:def_1; ((a div b) + 1) * b = ((a div b) * b) + b ; then ((a div b) + 1) * b > a by A1, XREAL_1:6; hence ex k being Element of NAT st ( k * b <= a & a < (k + 1) * b ) by A1, NAT_1:11; ::_thesis: verum end; 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) ) proof let n be Nat; ::_thesis: ( n > 0 implies 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) ) ) assume A1: n > 0 ; ::_thesis: 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) ) let a, b be Element of Segm n; ::_thesis: for k being Nat holds ( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . (a,b) = (a * b) - (k * n) ) reconsider a = a, b = b as Element of NAT by ORDINAL1:def_12; let k be Nat; ::_thesis: ( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . (a,b) = (a * b) - (k * n) ) A2: now__::_thesis:_(_k_*_n_<=_a_*_b_&_a_*_b_<_(k_+_1)_*_n_implies_(multint_n)_._(a,b)_=_(a_*_b)_-_(k_*_n)_) assume that A3: k * n <= a * b and A4: a * b < (k + 1) * n ; ::_thesis: (multint n) . (a,b) = (a * b) - (k * n) consider c being Element of NAT such that A5: c = (a * b) mod n ; consider t being Nat such that A6: ( ( a * b = (n * t) + c & c < n ) or ( c = 0 & n = 0 ) ) by A5, NAT_D:def_2; now__::_thesis:_(multint_n)_._(a,b)_=_(a_*_b)_-_(k_*_n) consider q being Nat such that A7: a * b = (k * n) + q by A3, NAT_1:10; t = k proof now__::_thesis:_(_(_t_<=_k_&_t_=_k_)_or_(_t_>_k_&_t_=_k_)_) percases ( t <= k or t > k ) ; case t <= k ; ::_thesis: t = k then consider r being Nat such that A8: t + r = k by NAT_1:10; A9: (n * t) + c = (t * n) + ((r * n) + q) by A1, A6, A7, A8; now__::_thesis:_(_(_t_=_k_&_t_=_k_)_or_(_t_<>_k_&_t_=_k_)_) percases ( t = k or t <> k ) ; case t = k ; ::_thesis: t = k hence t = k ; ::_thesis: verum end; caseA10: t <> k ; ::_thesis: t = k r >= 1 proof assume A11: r < 1 ; ::_thesis: contradiction r = 0 proof assume r <> 0 ; ::_thesis: contradiction then 1 + 0 <= r by INT_1:7; hence contradiction by A11; ::_thesis: verum end; hence contradiction by A8, A10; ::_thesis: verum end; then r * n >= 1 * n by NAT_1:4; then A12: (r * n) + q >= (1 * n) + q by XREAL_1:6; (1 * n) + q >= n by NAT_1:11; hence t = k by A1, A6, A9, A12, XXREAL_0:2; ::_thesis: verum end; end; end; hence t = k ; ::_thesis: verum end; case t > k ; ::_thesis: t = k then t >= k + 1 by INT_1:7; then A13: n * t >= n * (k + 1) by NAT_1:4; (n * t) + c >= n * t by NAT_1:11; hence t = k by A4, A6, A13, XXREAL_0:2; ::_thesis: verum end; end; end; hence t = k ; ::_thesis: verum end; hence (multint n) . (a,b) = (a * b) - (k * n) by A1, A5, A6, Def10; ::_thesis: verum end; hence (multint n) . (a,b) = (a * b) - (k * n) ; ::_thesis: verum end; now__::_thesis:_(_(multint_n)_._(a,b)_=_(a_*_b)_-_(k_*_n)_implies_(_k_*_n_<=_a_*_b_&_a_*_b_<_(k_+_1)_*_n_)_) assume (multint n) . (a,b) = (a * b) - (k * n) ; ::_thesis: ( k * n <= a * b & a * b < (k + 1) * n ) then (a * b) mod n = (a * b) - (k * n) by A1, Def10; then A14: ( ((a * b) - (k * n)) + (k * n) >= 0 + (k * n) & ex t being Nat st ( a * b = (n * t) + ((a * b) - (n * k)) & (a * b) - (n * k) < n ) ) by A1, NAT_D:def_2, XREAL_1:6; (k + 1) * n = (k * n) + n ; hence ( k * n <= a * b & a * b < (k + 1) * n ) by A14, XREAL_1:6; ::_thesis: verum end; hence ( ( k * n <= a * b & a * b < (k + 1) * n ) iff (multint n) . (a,b) = (a * b) - (k * n) ) by A2; ::_thesis: verum end; 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 ) ) proof let n be Nat; ::_thesis: ( n > 0 implies 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 ) ) ) assume A1: n > 0 ; ::_thesis: 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 ) ) let a be Element of Segm n; ::_thesis: ( ( 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 ) ) reconsider n = n as non zero Nat by A1; reconsider a = a as Element of NAT by ORDINAL1:def_12; A2: a < n by NAT_1:44; then a - a < n - a by XREAL_1:9; then reconsider b = n - a as Element of NAT by INT_1:3; consider c being Element of NAT such that A3: c = b mod n ; A4: ( (compint n) . a = 0 implies a = 0 ) proof a - a < n - a by A2, XREAL_1:9; then reconsider a9 = n - a as Element of NAT by INT_1:3; assume A5: (compint n) . a = 0 ; ::_thesis: a = 0 n <= n + a by NAT_1:11; then A6: n - a <= (n + a) - a by XREAL_1:9; consider t being Nat such that A7: a9 = (n * t) + (a9 mod n) and a9 mod n < n by NAT_D:def_2; assume a <> 0 ; ::_thesis: contradiction then n - a <> n ; then A8: n - a < n by A6, XXREAL_0:1; t = 0 proof assume t <> 0 ; ::_thesis: contradiction then 1 + 0 <= t by INT_1:7; then A9: 1 * n <= t * n by XREAL_1:64; t * n <= (t * n) + (a9 mod n) by NAT_1:11; hence contradiction by A8, A7, A9, XXREAL_0:2; ::_thesis: verum end; then a9 = 0 by A5, A7, Def11; hence contradiction by NAT_1:44; ::_thesis: verum end; consider t being Nat such that A10: ( ( b = (n * t) + c & c < n ) or ( c = 0 & n = 0 ) ) by A3, NAT_D:def_2; A11: n - a <= n proof assume n - a > n ; ::_thesis: contradiction then (n - a) + a > n + a by XREAL_1:6; hence contradiction by NAT_1:11; ::_thesis: verum end; A12: now__::_thesis:_(_a_=_0_implies_(compint_n)_._a_=_0_) assume A13: a = 0 ; ::_thesis: (compint n) . a = 0 A14: t = 1 proof now__::_thesis:_(_(_t_=_0_&_t_=_1_)_or_(_t_<>_0_&_t_=_1_)_) percases ( t = 0 or t <> 0 ) ; case t = 0 ; ::_thesis: t = 1 hence t = 1 by A10, A13; ::_thesis: verum end; caseA15: t <> 0 ; ::_thesis: t = 1 t < 2 proof assume t >= 2 ; ::_thesis: contradiction then A16: n * t >= n * 2 by XREAL_1:64; A17: n <= (n * 1) + (n * 1) by NAT_1:11; (n * t) + c >= n * t by NAT_1:11; then n - a >= n * 2 by A10, A16, XXREAL_0:2; then n * 1 = 2 * n by A13, A17, XXREAL_0:1; hence contradiction by A1; ::_thesis: verum end; then t < 1 + 1 ; then A18: t <= 1 by NAT_1:13; 1 + 0 <= t by A15, INT_1:7; hence t = 1 by A18, XXREAL_0:1; ::_thesis: verum end; end; end; hence t = 1 ; ::_thesis: verum end; c = 0 proof assume c <> 0 ; ::_thesis: contradiction then n + c > n + 0 by XREAL_1:6; hence contradiction by A10, A11, A14; ::_thesis: verum end; hence (compint n) . a = 0 by A3, Def11; ::_thesis: verum end; now__::_thesis:_(_a_<>_0_implies_(compint_n)_._a_=_n_-_a_) assume A19: a <> 0 ; ::_thesis: (compint n) . a = n - a A20: n - a < n proof assume n - a >= n ; ::_thesis: contradiction then n - a = n by A11, XXREAL_0:1; hence contradiction by A19; ::_thesis: verum end; t = 0 proof assume t <> 0 ; ::_thesis: contradiction then 1 + 0 <= t by INT_1:7; then A21: 1 * n <= t * n by XREAL_1:64; n * t <= (n * t) + c by NAT_1:11; hence contradiction by A10, A20, A21, XXREAL_0:2; ::_thesis: verum end; hence (compint n) . a = n - a by A3, A10, Def11; ::_thesis: verum end; hence ( ( 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 ) ) by A12, A4; ::_thesis: verum end; 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 ) proof set n = 1; set R = INT.Ring 1; A1: for x being Element of (INT.Ring 1) st x <> 0. (INT.Ring 1) holds ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1) proof let x be Element of (INT.Ring 1); ::_thesis: ( x <> 0. (INT.Ring 1) implies ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1) ) assume x <> 0. (INT.Ring 1) ; ::_thesis: ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1) then x <> 0 by FUNCT_7:def_1; hence ex y being Element of (INT.Ring 1) st y * x = 1. (INT.Ring 1) by CARD_1:49, TARSKI:def_1; ::_thesis: verum end; A2: for a, b being Element of (INT.Ring 1) holds a + b = b + a proof let a, b be Element of (INT.Ring 1); ::_thesis: a + b = b + a thus a + b = 0 by CARD_1:49, TARSKI:def_1 .= b + a by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum end; A3: for a being Element of (INT.Ring 1) holds a + (0. (INT.Ring 1)) = a proof let a be Element of (INT.Ring 1); ::_thesis: a + (0. (INT.Ring 1)) = a a = 0 by CARD_1:49, TARSKI:def_1; hence a + (0. (INT.Ring 1)) = a by CARD_1:49, TARSKI:def_1; ::_thesis: verum end; A4: for a, b, c being Element of (INT.Ring 1) holds (a * b) * c = a * (b * c) proof let a, b, c be Element of (INT.Ring 1); ::_thesis: (a * b) * c = a * (b * c) thus (a * b) * c = 0 by CARD_1:49, TARSKI:def_1 .= a * (b * c) by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum end; A5: for a being Element of (INT.Ring 1) holds a + (- a) = 0. (INT.Ring 1) proof let a be Element of (INT.Ring 1); ::_thesis: a + (- a) = 0. (INT.Ring 1) thus a + (- a) = 0 by CARD_1:49, TARSKI:def_1 .= 0. (INT.Ring 1) by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum end; A6: INT.Ring 1 is right_complementable proof let v be Element of (INT.Ring 1); :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable take - v ; :: according to ALGSTR_0:def_11 ::_thesis: v + (- v) = 0. (INT.Ring 1) thus v + (- v) = 0. (INT.Ring 1) by A5; ::_thesis: verum end; A7: for a, b, c being Element of (INT.Ring 1) holds (a + b) + c = a + (b + c) proof let a, b, c be Element of (INT.Ring 1); ::_thesis: (a + b) + c = a + (b + c) thus (a + b) + c = 0 by CARD_1:49, TARSKI:def_1 .= a + (b + c) by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum end; A8: for a being Element of (INT.Ring 1) holds ( (1. (INT.Ring 1)) * a = a & a * (1. (INT.Ring 1)) = a ) proof let a be Element of (INT.Ring 1); ::_thesis: ( (1. (INT.Ring 1)) * a = a & a * (1. (INT.Ring 1)) = a ) A9: a * (1. (INT.Ring 1)) = 0 by CARD_1:49, TARSKI:def_1 .= a by CARD_1:49, TARSKI:def_1 ; (1. (INT.Ring 1)) * a = 0 by CARD_1:49, TARSKI:def_1 .= a by CARD_1:49, TARSKI:def_1 ; hence ( (1. (INT.Ring 1)) * a = a & a * (1. (INT.Ring 1)) = a ) by A9; ::_thesis: verum end; A10: INT.Ring 1 is well-unital proof let x be Element of (INT.Ring 1); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (INT.Ring 1)) = x & (1. (INT.Ring 1)) * x = x ) thus x * (1. (INT.Ring 1)) = x by A8; ::_thesis: (1. (INT.Ring 1)) * x = x thus (1. (INT.Ring 1)) * x = x by A8; ::_thesis: verum end; A11: for a, b being Element of (INT.Ring 1) holds a * b = b * a proof let a, b be Element of (INT.Ring 1); ::_thesis: a * b = b * a thus a * b = 0 by CARD_1:49, TARSKI:def_1 .= b * a by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum end; A12: for a, b, c being Element of (INT.Ring 1) holds a * (b + c) = (a * b) + (a * c) proof let a, b, c be Element of (INT.Ring 1); ::_thesis: a * (b + c) = (a * b) + (a * c) thus a * (b + c) = 0 by CARD_1:49, TARSKI:def_1 .= (a * b) + (a * c) by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum end; A13: for a, b, c being Element of (INT.Ring 1) holds (b + c) * a = (b * a) + (c * a) proof let a, b, c be Element of (INT.Ring 1); ::_thesis: (b + c) * a = (b * a) + (c * a) thus (b + c) * a = 0 by CARD_1:49, TARSKI:def_1 .= (b * a) + (c * a) by CARD_1:49, TARSKI:def_1 ; ::_thesis: verum end; 0. (INT.Ring 1) = 0 by CARD_1:49, TARSKI:def_1 .= 1. (INT.Ring 1) by CARD_1:49, TARSKI:def_1 ; hence ( 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 ) by A1, A2, A11, A7, A4, A3, A13, A12, A6, A10, GROUP_1:def_3, GROUP_1:def_12, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, VECTSP_1:def_7, VECTSP_1:def_9; ::_thesis: verum end; 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 proof let n be Nat; ::_thesis: ( 1 < n implies 1. (INT.Ring n) = 1 ) assume 1 < n ; ::_thesis: 1. (INT.Ring n) = 1 then 1 in Segm n by NAT_1:44; hence 1. (INT.Ring n) = 1 by FUNCT_7:def_1; ::_thesis: verum end; 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 ) proof let n be Nat; ::_thesis: ( n > 1 implies ( not INT.Ring n is degenerated & INT.Ring n is commutative Ring ) ) assume A1: n > 1 ; ::_thesis: ( not INT.Ring n is degenerated & INT.Ring n is commutative Ring ) then reconsider n = n as non zero Nat ; set F = INT.Ring n; A2: 1. (INT.Ring n) = 1 by A1, Lm11; A3: for a being Element of (INT.Ring n) holds ( (1. (INT.Ring n)) * a = a & a * (1. (INT.Ring n)) = a ) proof let a be Element of (INT.Ring n); ::_thesis: ( (1. (INT.Ring n)) * a = a & a * (1. (INT.Ring n)) = a ) reconsider a9 = a as Element of Segm n ; A4: ( 1 * a9 < (0 + 1) * n & 1 is Element of Segm n ) by A1, NAT_1:44; then A5: (multint n) . (a,1) = a9 - (0 * n) by Th8 .= a9 ; (multint n) . (1,a) = a9 - (0 * n) by A4, Th8 .= a9 ; hence ( (1. (INT.Ring n)) * a = a & a * (1. (INT.Ring n)) = a ) by A1, A5, Lm11; ::_thesis: verum end; A6: INT.Ring n is well-unital proof let x be Element of (INT.Ring n); :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. (INT.Ring n)) = x & (1. (INT.Ring n)) * x = x ) thus x * (1. (INT.Ring n)) = x by A3; ::_thesis: (1. (INT.Ring n)) * x = x thus (1. (INT.Ring n)) * x = x by A3; ::_thesis: verum end; A7: for a, b being Element of (INT.Ring n) holds a + b = b + a proof let a, b be Element of (INT.Ring n); ::_thesis: a + b = b + a reconsider a9 = a as Element of Segm n ; reconsider b9 = b as Element of Segm n ; now__::_thesis:_(_(_a9_+_b9_<_n_&_(addint_n)_._(a,b)_=_(addint_n)_._(b,a)_)_or_(_a9_+_b9_>=_n_&_(addint_n)_._(a,b)_=_(addint_n)_._(b,a)_)_) percases ( a9 + b9 < n or a9 + b9 >= n ) ; caseA8: a9 + b9 < n ; ::_thesis: (addint n) . (a,b) = (addint n) . (b,a) hence (addint n) . (a,b) = a9 + b9 by Th7 .= (addint n) . (b,a) by A8, Th7 ; ::_thesis: verum end; caseA9: a9 + b9 >= n ; ::_thesis: (addint n) . (a,b) = (addint n) . (b,a) hence (addint n) . (a,b) = (a9 + b9) - n by Th7 .= (addint n) . (b,a) by A9, Th7 ; ::_thesis: verum end; end; end; hence a + b = b + a ; ::_thesis: verum end; A10: for a, b, c being Element of (INT.Ring n) holds (a * b) * c = a * (b * c) proof let a, b, c be Element of (INT.Ring n); ::_thesis: (a * b) * c = a * (b * c) reconsider a9 = a, b9 = b, c9 = c as Element of Segm n ; reconsider aa = a9 as Element of NAT ; reconsider aa = aa as Integer ; reconsider bb = b9 as Element of NAT ; reconsider bb = bb as Integer ; reconsider cc = c9 as Element of NAT ; reconsider cc = cc as Integer ; A11: cc < n by NAT_1:44; aa < n by NAT_1:44; then A12: (a9 * ((b9 * c9) mod n)) mod n = ((aa mod n) * ((bb * cc) mod n)) mod n by NAT_D:63 .= (aa * (bb * cc)) mod n by NAT_D:67 .= ((aa * bb) * cc) mod n .= (((aa * bb) mod n) * (cc mod n)) mod n by NAT_D:67 .= (((a9 * b9) mod n) * c9) mod n by A11, NAT_D:63 ; (aa * bb) mod n < n by NAT_D:62; then A13: (a9 * b9) mod n is Element of Segm n by NAT_1:44; (bb * cc) mod n < n by NAT_D:62; then A14: (b9 * c9) mod n is Element of Segm n by NAT_1:44; A15: a * (b * c) = (multint n) . (a9,((b9 * c9) mod n)) by Def10 .= (a9 * ((b9 * c9) mod n)) mod n by A14, Def10 ; (a * b) * c = (multint n) . (((a9 * b9) mod n),c9) by Def10 .= (((a9 * b9) mod n) * c9) mod n by A13, Def10 ; hence (a * b) * c = a * (b * c) by A15, A12; ::_thesis: verum end; A16: for a, b being Element of (INT.Ring n) holds a * b = b * a proof let a, b be Element of (INT.Ring n); ::_thesis: a * b = b * a reconsider a9 = a as Element of Segm n ; reconsider b9 = b as Element of Segm n ; consider k being Element of NAT such that A17: ( k * n <= a9 * b9 & a9 * b9 < (k + 1) * n ) by Lm9; (multint n) . (a9,b9) = (a9 * b9) - (k * n) by A17, Th8 .= (multint n) . (b9,a9) by A17, Th8 ; hence a * b = b * a ; ::_thesis: verum end; A18: for a, b, c being Element of (INT.Ring n) holds (a + b) + c = a + (b + c) proof let a, b, c be Element of (INT.Ring n); ::_thesis: (a + b) + c = a + (b + c) reconsider a9 = a, b9 = b, c9 = c as Element of Segm n ; reconsider aa = a9 as Element of NAT ; reconsider aa = aa as Integer ; reconsider bb = b9 as Element of NAT ; reconsider bb = bb as Integer ; reconsider cc = c9 as Element of NAT ; reconsider cc = cc as Integer ; A19: cc < n by NAT_1:44; aa < n by NAT_1:44; then A20: (a9 + ((b9 + c9) mod n)) mod n = ((aa mod n) + ((bb + cc) mod n)) mod n by NAT_D:63 .= (aa + (bb + cc)) mod n by NAT_D:66 .= ((aa + bb) + cc) mod n .= (((aa + bb) mod n) + (cc mod n)) mod n by NAT_D:66 .= (((a9 + b9) mod n) + c9) mod n by A19, NAT_D:63 ; (aa + bb) mod n < n by NAT_D:62; then A21: (a9 + b9) mod n is Element of Segm n by NAT_1:44; (bb + cc) mod n < n by NAT_D:62; then A22: (b9 + c9) mod n is Element of Segm n by NAT_1:44; A23: a + (b + c) = (addint n) . (a9,((b9 + c9) mod n)) by GR_CY_1:def_4 .= (a9 + ((b9 + c9) mod n)) mod n by A22, GR_CY_1:def_4 ; (a + b) + c = (addint n) . (((a9 + b9) mod n),c9) by GR_CY_1:def_4 .= (((a9 + b9) mod n) + c9) mod n by A21, GR_CY_1:def_4 ; hence (a + b) + c = a + (b + c) by A23, A20; ::_thesis: verum end; 0 in Segm n by NAT_1:44; then A24: 0. (INT.Ring n) = 0 by FUNCT_7:def_1; A25: for a being Element of (INT.Ring n) holds a + (0. (INT.Ring n)) = a proof let a be Element of (INT.Ring n); ::_thesis: a + (0. (INT.Ring n)) = a reconsider a9 = a as Element of Segm n ; a9 + 0 < n by NAT_1:44; hence a + (0. (INT.Ring n)) = a by A24, Th7; ::_thesis: verum end; A26: INT.Ring n is right_complementable proof let a be Element of (INT.Ring n); :: according to ALGSTR_0:def_16 ::_thesis: a is right_complementable reconsider a9 = a as Element of Segm n ; reconsider a9 = a9 as Element of NAT ; percases ( a9 = 0 or a9 <> 0 ) ; supposeA27: a9 = 0 ; ::_thesis: a is right_complementable take 0. (INT.Ring n) ; :: according to ALGSTR_0:def_11 ::_thesis: a + (0. (INT.Ring n)) = 0. (INT.Ring n) thus a + (0. (INT.Ring n)) = 0. (INT.Ring n) by A24, A25, A27; ::_thesis: verum end; suppose a9 <> 0 ; ::_thesis: a is right_complementable then reconsider b = n - a9 as Element of Segm n by Lm10; reconsider v = b as Element of (INT.Ring n) ; take v ; :: according to ALGSTR_0:def_11 ::_thesis: a + v = 0. (INT.Ring n) thus a + v = (a9 + b) mod n by GR_CY_1:def_4 .= 0. (INT.Ring n) by A24, NAT_D:25 ; ::_thesis: verum end; end; end; A28: for a, b, c being Element of (INT.Ring n) holds (b + c) * a = (b * a) + (c * a) proof let a, b, c be Element of (INT.Ring n); ::_thesis: (b + c) * a = (b * a) + (c * a) reconsider a9 = a, b9 = b, c9 = c as Element of Segm n ; reconsider aa = a9 as Element of NAT ; reconsider aa = aa as Integer ; reconsider bb = b9 as Element of NAT ; reconsider bb = bb as Integer ; reconsider cc = c9 as Element of NAT ; reconsider cc = cc as Integer ; A29: aa < n by NAT_1:44; A30: (((b9 * a9) mod n) + ((c9 * a9) mod n)) mod n = ((bb * aa) + (cc * aa)) mod n by NAT_D:66 .= ((bb + cc) * aa) mod n .= (((bb + cc) mod n) * (aa mod n)) mod n by NAT_D:67 .= (((b9 + c9) mod n) * a9) mod n by A29, NAT_D:63 ; (bb + cc) mod n < n by NAT_D:62; then A31: (b9 + c9) mod n is Element of Segm n by NAT_1:44; (cc * aa) mod n < n by NAT_D:62; then A32: (c9 * a9) mod n is Element of Segm n by NAT_1:44; (bb * aa) mod n < n by NAT_D:62; then A33: (b9 * a9) mod n is Element of Segm n by NAT_1:44; A34: (b + c) * a = (multint n) . (((b9 + c9) mod n),a9) by GR_CY_1:def_4 .= (((b9 + c9) mod n) * a9) mod n by A31, Def10 ; (b * a) + (c * a) = (addint n) . (((multint n) . (b,a)),((c9 * a9) mod n)) by Def10 .= (addint n) . (((b9 * a9) mod n),((c9 * a9) mod n)) by Def10 .= (((b9 * a9) mod n) + ((c9 * a9) mod n)) mod n by A33, A32, GR_CY_1:def_4 ; hence (b + c) * a = (b * a) + (c * a) by A34, A30; ::_thesis: verum end; for a, b, c being Element of (INT.Ring n) holds a * (b + c) = (a * b) + (a * c) proof let a, b, c be Element of (INT.Ring n); ::_thesis: a * (b + c) = (a * b) + (a * c) thus a * (b + c) = (b + c) * a by A16 .= (b * a) + (c * a) by A28 .= (a * b) + (c * a) by A16 .= (a * b) + (a * c) by A16 ; ::_thesis: verum end; then reconsider F = INT.Ring n as commutative Ring by A7, A16, A18, A10, A25, A28, A26, A6, GROUP_1:def_3, GROUP_1:def_12, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, VECTSP_1:def_7; not F is degenerated by A24, A2, STRUCT_0:def_8; hence ( not INT.Ring n is degenerated & INT.Ring n is commutative Ring ) ; ::_thesis: verum end; 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 ) proof let p be Nat; ::_thesis: ( p > 1 implies ( 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 ) ) assume A1: p > 1 ; ::_thesis: ( 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 ) then reconsider p = p as non zero Nat ; reconsider P = INT.Ring p as Ring by A1, Th11; reconsider p = p as non zero Element of NAT by ORDINAL1:def_12; A2: now__::_thesis:_(_INT.Ring_p_is_non_empty_non_degenerated_right_complementable_almost_left_invertible_associative_commutative_Abelian_add-associative_right_zeroed_well-unital_distributive_doubleLoopStr_implies_p_is_Prime_) assume A3: INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; ::_thesis: p is Prime for n being Nat holds ( not n divides p or n = 1 or n = p ) proof let n be Nat; ::_thesis: ( not n divides p or n = 1 or n = p ) assume n divides p ; ::_thesis: ( n = 1 or n = p ) then consider k being Nat such that A4: p = n * k by NAT_D:def_3; A5: n <= p proof assume A6: n > p ; ::_thesis: contradiction now__::_thesis:_(_(_k_=_0_&_contradiction_)_or_(_k_<>_0_&_contradiction_)_) percases ( k = 0 or k <> 0 ) ; case k = 0 ; ::_thesis: contradiction hence contradiction by A4; ::_thesis: verum end; caseA7: k <> 0 ; ::_thesis: contradiction then k >= 1 + 0 by INT_1:7; then k * p >= 1 * p by XREAL_1:64; hence contradiction by A4, A6, A7, XREAL_1:68; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; A8: k <= p proof assume A9: k > p ; ::_thesis: contradiction now__::_thesis:_(_(_n_=_0_&_contradiction_)_or_(_n_<>_0_&_contradiction_)_) percases ( n = 0 or n <> 0 ) ; case n = 0 ; ::_thesis: contradiction hence contradiction by A4; ::_thesis: verum end; caseA10: n <> 0 ; ::_thesis: contradiction then n >= 1 + 0 by INT_1:7; then n * p >= 1 * p by XREAL_1:64; hence contradiction by A4, A9, A10, XREAL_1:68; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; now__::_thesis:_(_(_k_=_p_&_(_n_=_1_or_n_=_p_)_)_or_(_k_<>_p_&_(_n_=_1_or_n_=_p_)_)_) percases ( k = p or k <> p ) ; case k = p ; ::_thesis: ( n = 1 or n = p ) then 1 * p = p * n by A4; hence ( n = 1 or n = p ) by XCMPLX_1:5; ::_thesis: verum end; case k <> p ; ::_thesis: ( n = 1 or n = p ) then A11: k < p by A8, XXREAL_0:1; now__::_thesis:_(_(_n_=_p_&_(_n_=_1_or_n_=_p_)_)_or_(_n_<>_p_&_contradiction_)_) percases ( n = p or n <> p ) ; case n = p ; ::_thesis: ( n = 1 or n = p ) then 1 * p = k * p by A4; then k = 1 by XCMPLX_1:5; hence ( n = 1 or n = p ) by A4; ::_thesis: verum end; case n <> p ; ::_thesis: contradiction then n < p by A5, XXREAL_0:1; then reconsider n2 = n as Element of Segm p by NAT_1:44; 0 in p by NAT_1:44; then A12: 0 = 0. (INT.Ring p) by FUNCT_7:def_1; k <> 0 by A4; then A13: k <> 0. (INT.Ring p) by A12; reconsider k2 = k as Element of Segm p by A11, NAT_1:44; reconsider n9 = n2 as Element of (INT.Ring p) ; reconsider k9 = k2 as Element of (INT.Ring p) ; n <> 0 by A4; then A14: n <> 0. (INT.Ring p) by A12; n9 * k9 = (n2 * k2) mod p by Def10 .= 0. (INT.Ring p) by A12, A4, INT_1:62 ; hence contradiction by A3, A14, A13, VECTSP_1:12; ::_thesis: verum end; end; end; hence ( n = 1 or n = p ) ; ::_thesis: verum end; end; end; hence ( n = 1 or n = p ) ; ::_thesis: verum end; hence p is Prime by A1, INT_2:def_4; ::_thesis: verum end; now__::_thesis:_(_p_is_Prime_implies_INT.Ring_p_is_non_empty_non_degenerated_right_complementable_almost_left_invertible_associative_commutative_Abelian_add-associative_right_zeroed_well-unital_distributive_doubleLoopStr_) assume A15: p is Prime ; ::_thesis: INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for a being Element of P st a <> 0. P holds ex b being Element of P st b * a = 1. P proof reconsider e = 1 as Integer ; let a be Element of P; ::_thesis: ( a <> 0. P implies ex b being Element of P st b * a = 1. P ) reconsider a9 = a as Element of Segm p ; reconsider a9 = a9 as Element of NAT ; reconsider a2 = a9 as Integer ; 1 * p = p ; then A16: 1 divides p by NAT_D:def_3; assume A17: a <> 0. P ; ::_thesis: ex b being Element of P st b * a = 1. P A18: for m being Nat st m divides a9 & m divides p holds m divides 1 proof let m be Nat; ::_thesis: ( m divides a9 & m divides p implies m divides 1 ) assume that A19: m divides a9 and A20: m divides p ; ::_thesis: m divides 1 consider k being Nat such that A21: a9 = m * k by A19, NAT_D:def_3; m <= a9 proof assume A22: m > a9 ; ::_thesis: contradiction now__::_thesis:_(_(_k_=_0_&_contradiction_)_or_(_k_<>_0_&_contradiction_)_) percases ( k = 0 or k <> 0 ) ; case k = 0 ; ::_thesis: contradiction hence contradiction by A17, A21, FUNCT_7:def_1; ::_thesis: verum end; caseA23: k <> 0 ; ::_thesis: contradiction then k >= 1 + 0 by INT_1:7; then k * a9 >= 1 * a9 by XREAL_1:64; hence contradiction by A21, A22, A23, XREAL_1:68; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; then m <> p by NAT_1:44; hence m divides 1 by A15, A20, INT_2:def_4; ::_thesis: verum end; 1 * a9 = a9 ; then 1 divides a9 by NAT_D:def_3; then a9 gcd p = 1 by A16, A18, NAT_D:def_5; then consider s, t being Integer such that A24: 1 = (s * a9) + (t * p) by NAT_D:68; s mod p >= 0 by NAT_D:62; then A25: s mod p is Element of NAT by INT_1:3; s mod p < p by NAT_D:62; then reconsider b9 = s mod p as Element of Segm p by A25, NAT_1:44; reconsider b = b9 as Element of P ; b * a = (a9 * b9) mod p by Def10 .= ((a2 mod p) * ((s mod p) mod p)) mod p by NAT_D:67 .= ((a2 mod p) * (s mod p)) mod p by NAT_D:65 .= (a2 * s) mod p by NAT_D:67 .= e mod p by A24, NAT_D:61 .= e by A1, NAT_D:63 .= 1. P by A1, Lm11 ; hence ex b being Element of P st b * a = 1. P ; ::_thesis: verum end; hence INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr by A1, Th11, VECTSP_1:def_9; ::_thesis: verum end; hence ( 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 ) by A2; ::_thesis: verum end; registration clusterV10() prime -> non zero for set ; coherence for b1 being Prime holds not b1 is zero proof let k be Prime; ::_thesis: not k is zero assume k is zero ; ::_thesis: contradiction then k in SetPrimenumber 2 by NEWTON:def_7; hence contradiction ; ::_thesis: verum end; 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 ) proof p > 1 by INT_2:def_4; hence ( 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 ) by Th12; ::_thesis: verum end; 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 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 ) proof take INT.Ring ; ::_thesis: ( INT.Ring is strict & INT.Ring is infinite ) thus ( INT.Ring is strict & INT.Ring is infinite ) ; ::_thesis: verum end; end;