:: 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;