let n be natural number ; :: thesis: ( n > 1 implies ( not INT.Ring n is degenerated & INT.Ring n is commutative well-unital distributive Ring ) )
assume A1: n > 1 ; :: thesis: ( not INT.Ring n is degenerated & INT.Ring n is commutative well-unital distributive Ring )
then reconsider n = n as non zero natural number ;
set F = INT.Ring n;
0 in Segm n by NAT_1:45;
then A2: 0. (INT.Ring n) = 0 by FUNCT_7:def 1;
A3: 1. (INT.Ring n) = 1 by A1, Lm12;
A4: 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 a' = a as Element of Segm n ;
reconsider b' = b as Element of Segm n ;

now

per cases ( a' + b' < n or a' + b' >= n ) ;

case A5: a' + b' < n ; :: thesis: (addint n) . a,b = (addint n) . b,a

hence (addint n) . a,b = a' + b' by Th17
.= (addint n) . b,a by A5, Th17 ;
:: thesis: verum

end;

case A6: a' + b' >= n ; :: thesis: (addint n) . a,b = (addint n) . b,a

hence (addint n) . a,b = (a' + b') - n by Th17
.= (addint n) . b,a by A6, Th17 ;
:: thesis: verum

end;

end;

end;

hence a + b = b + a ; :: 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 a' = a as Element of Segm n ;
reconsider b' = b as Element of Segm n ;
consider k being Element of NAT such that
A8: ( k * n <= a' * b' & a' * b' < (k + 1) * n ) by Lm10;
(multint n) . a',b' = (a' * b') - (k * n) by A8, Th18
.= (multint n) . b',a' by A8, Th18 ;
hence a * b = b * a ; :: thesis: verum

end;

A9: 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 a' = a, b' = b, c' = c as Element of Segm n ;
reconsider aa = a' as Element of NAT ;
reconsider aa = aa as Integer ;
reconsider bb = b' as Element of NAT ;
reconsider bb = bb as Integer ;
reconsider cc = c' as Element of NAT ;
reconsider cc = cc as Integer ;
A10: ( aa >= 0 & aa < n & bb >= 0 & bb < n & cc >= 0 & cc < n ) by NAT_1:45;
( (aa + bb) mod n >= 0 & (aa + bb) mod n < n ) by Th9;
then A11: (a' + b') mod n is Element of Segm n by NAT_1:45;
( (bb + cc) mod n >= 0 & (bb + cc) mod n < n ) by Th9;
then A12: (b' + c') mod n is Element of Segm n by NAT_1:45;
A13: (a + b) + c = (addint n) . ((a' + b') mod n),c' by GR_CY_1:def 5
.= (((a' + b') mod n) + c') mod n by A11, GR_CY_1:def 5 ;
A14: a + (b + c) = (addint n) . a',((b' + c') mod n) by GR_CY_1:def 5
.= (a' + ((b' + c') mod n)) mod n by A12, GR_CY_1:def 5 ;
(a' + ((b' + c') mod n)) mod n = ((aa mod n) + ((bb + cc) mod n)) mod n by A10, Th10
.= (aa + (bb + cc)) mod n by Th14
.= ((aa + bb) + cc) mod n
.= (((aa + bb) mod n) + (cc mod n)) mod n by Th14
.= (((a' + b') mod n) + c') mod n by A10, Th10 ;
hence (a + b) + c = a + (b + c) by A13, A14; :: thesis: verum

end;

A15: 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 a' = a, b' = b, c' = c as Element of Segm n ;
reconsider aa = a' as Element of NAT ;
reconsider aa = aa as Integer ;
reconsider bb = b' as Element of NAT ;
reconsider bb = bb as Integer ;
reconsider cc = c' as Element of NAT ;
reconsider cc = cc as Integer ;
A16: ( aa >= 0 & aa < n & bb >= 0 & bb < n & cc >= 0 & cc < n ) by NAT_1:45;
( (aa * bb) mod n >= 0 & (aa * bb) mod n < n ) by Th9;
then A17: (a' * b') mod n is Element of Segm n by NAT_1:45;
( (bb * cc) mod n >= 0 & (bb * cc) mod n < n ) by Th9;
then A18: (b' * c') mod n is Element of Segm n by NAT_1:45;
A19: (a * b) * c = (multint n) . ((a' * b') mod n),c' by Def11
.= (((a' * b') mod n) * c') mod n by A17, Def11 ;
A20: a * (b * c) = (multint n) . a',((b' * c') mod n) by Def11
.= (a' * ((b' * c') mod n)) mod n by A18, Def11 ;
(a' * ((b' * c') mod n)) mod n = ((aa mod n) * ((bb * cc) mod n)) mod n by A16, Th10
.= (aa * (bb * cc)) mod n by Th15
.= ((aa * bb) * cc) mod n
.= (((aa * bb) mod n) * (cc mod n)) mod n by Th15
.= (((a' * b') mod n) * c') mod n by A16, Th10 ;
hence (a * b) * c = a * (b * c) by A19, A20; :: thesis: verum

end;

A21: 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 a' = a as Element of Segm n ;
a' + 0 < n by NAT_1:45;
hence a + (0. (INT.Ring n)) = a by A2, Th17; :: thesis: verum

end;

A22: 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 a' = a as Element of Segm n ;
A23: ( 0 * n <= 1 * a' & 1 * a' < (0 + 1) * n ) by NAT_1:45;
A24: 1 is Element of Segm n by A1, NAT_1:45;
then A25: (multint n) . 1,a = a' - (0 * n) by A23, Th18
.= a' ;
(multint n) . a,1 = a' - (0 * n) by A23, A24, Th18
.= a' ;
hence ( (1. (INT.Ring n)) * a = a & a * (1. (INT.Ring n)) = a ) by A1, A25, Lm12; :: thesis: verum

end;

A26: 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 a' = a, b' = b, c' = c as Element of Segm n ;
reconsider aa = a' as Element of NAT ;
reconsider aa = aa as Integer ;
reconsider bb = b' as Element of NAT ;
reconsider bb = bb as Integer ;
reconsider cc = c' as Element of NAT ;
reconsider cc = cc as Integer ;
A27: ( aa >= 0 & aa < n & bb >= 0 & bb < n & cc >= 0 & cc < n ) by NAT_1:45;
( (bb + cc) mod n >= 0 & (bb + cc) mod n < n ) by Th9;
then A28: (b' + c') mod n is Element of Segm n by NAT_1:45;
( (bb * aa) mod n >= 0 & (bb * aa) mod n < n ) by Th9;
then A29: (b' * a') mod n is Element of Segm n by NAT_1:45;
( (cc * aa) mod n >= 0 & (cc * aa) mod n < n ) by Th9;
then A30: (c' * a') mod n is Element of Segm n by NAT_1:45;
A31: (b + c) * a = (multint n) . ((b' + c') mod n),a' by GR_CY_1:def 5
.= (((b' + c') mod n) * a') mod n by A28, Def11 ;
A32: (b * a) + (c * a) = (addint n) . ((multint n) . b,a),((c' * a') mod n) by Def11
.= (addint n) . ((b' * a') mod n),((c' * a') mod n) by Def11
.= (((b' * a') mod n) + ((c' * a') mod n)) mod n by A29, A30, GR_CY_1:def 5 ;
(((b' * a') mod n) + ((c' * a') mod n)) mod n = ((bb * aa) + (cc * aa)) mod n by Th14
.= ((bb + cc) * aa) mod n
.= (((bb + cc) mod n) * (aa mod n)) mod n by Th15
.= (((b' + c') mod n) * a') mod n by A27, Th10 ;
hence (b + c) * a = (b * a) + (c * a) by A31, A32; :: thesis: verum

end;

A33: 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 A7
.= (b * a) + (c * a) by A26
.= (a * b) + (c * a) by A7
.= (a * b) + (a * c) by A7 ; :: thesis: verum

end;

A34: 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 a' = a as Element of Segm n ;
reconsider a' = a' as Element of NAT ;

per cases ( a' = 0 or a' <> 0 ) ;

suppose A35: a' = 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 A2, A21, A35; :: thesis: verum

end;

suppose a' <> 0 ; :: thesis: a is right_complementable

then a' > 0 ;
then reconsider b = n - a' as Element of Segm n by Lm11;
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 = (a' + b) mod n by GR_CY_1:def 5
.= 0. (INT.Ring n) by A2, NAT_D:25 ; :: thesis: verum

end;

end;

end;

INT.Ring n is well-unital

proof

let x be Element of (INT.Ring n); :: according to VECTSP_1:def 16 :: thesis: ( x * (1. (INT.Ring n)) = x & (1. (INT.Ring n)) * x = x )
thus x * (1. (INT.Ring n)) = x by A22; :: thesis: (1. (INT.Ring n)) * x = x
thus (1. (INT.Ring n)) * x = x by A22; :: thesis: verum

end;

then reconsider F = INT.Ring n as commutative Ring by A4, A7, A9, A15, A21, A26, A33, A34, GROUP_1:def 4, GROUP_1:def 16, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, VECTSP_1:def 18;
not F is degenerated by A2, A3, STRUCT_0:def 8;
hence ( not INT.Ring n is degenerated & INT.Ring n is commutative well-unital distributive Ring ) ; :: thesis: verum