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;
A2: 1. (INT.Ring n) = 1 by A1, Lm12;
A3: for a being Element of holds
( (1. (INT.Ring n)) * a = a & a * (1. (INT.Ring n)) = a )

proof

let a be Element of ; :: thesis: ( (1. (INT.Ring n)) * a = a & a * (1. (INT.Ring n)) = a )
reconsider a' = a as Element of Segm n ;
A4: ( 1 * a' < (0 + 1) * n & 1 is Element of Segm n ) by A1, NAT_1:45;
then A5: (multint n) . a,1 = a' - (0 * n) by Th18
.= a' ;
(multint n) . 1,a = a' - (0 * n) by A4, Th18
.= a' ;
hence ( (1. (INT.Ring n)) * a = a & a * (1. (INT.Ring n)) = a ) by A1, A5, Lm12; :: thesis: verum

end;

A6: INT.Ring n is well-unital

proof

let x be Element of ; :: 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 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 holds a + b = b + a

proof

let a, b be Element of ; :: 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 A8: 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 A8, Th17 ;
:: thesis: verum

end;

case A9: 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 A9, Th17 ;
:: thesis: verum

end;

end;

end;

hence a + b = b + a ; :: thesis: verum

end;

A10: for a, b, c being Element of holds (a * b) * c = a * (b * c)

proof

let a, b, c be Element of ; :: 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 ;
A11: cc < n by NAT_1:45;
aa < n by NAT_1:45;
then A12: (a' * ((b' * c') mod n)) mod n = ((aa mod n) * ((bb * cc) mod n)) mod n by 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 A11, Th10 ;
(aa * bb) mod n < n by Th9;
then A13: (a' * b') mod n is Element of Segm n by NAT_1:45;
(bb * cc) mod n < n by Th9;
then A14: (b' * c') mod n is Element of Segm n by NAT_1:45;
A15: a * (b * c) = (multint n) . a',((b' * c') mod n) by Def11
.= (a' * ((b' * c') mod n)) mod n by A14, Def11 ;
(a * b) * c = (multint n) . ((a' * b') mod n),c' by Def11
.= (((a' * b') mod n) * c') mod n by A13, Def11 ;
hence (a * b) * c = a * (b * c) by A15, A12; :: thesis: verum

end;

A16: for a, b being Element of holds a * b = b * a

proof

let a, b be Element of ; :: 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
A17: ( k * n <= a' * b' & a' * b' < (k + 1) * n ) by Lm10;
(multint n) . a',b' = (a' * b') - (k * n) by A17, Th18
.= (multint n) . b',a' by A17, Th18 ;
hence a * b = b * a ; :: thesis: verum

end;

A18: for a, b, c being Element of holds (a + b) + c = a + (b + c)

proof

let a, b, c be Element of ; :: 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 ;
A19: cc < n by NAT_1:45;
aa < n by NAT_1:45;
then A20: (a' + ((b' + c') mod n)) mod n = ((aa mod n) + ((bb + cc) mod n)) mod n by 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 A19, Th10 ;
(aa + bb) mod n < n by Th9;
then A21: (a' + b') mod n is Element of Segm n by NAT_1:45;
(bb + cc) mod n < n by Th9;
then A22: (b' + c') mod n is Element of Segm n by NAT_1:45;
A23: a + (b + c) = (addint n) . a',((b' + c') mod n) by GR_CY_1:def 5
.= (a' + ((b' + c') mod n)) mod n by A22, GR_CY_1:def 5 ;
(a + b) + c = (addint n) . ((a' + b') mod n),c' by GR_CY_1:def 5
.= (((a' + b') mod n) + c') mod n by A21, GR_CY_1:def 5 ;
hence (a + b) + c = a + (b + c) by A23, A20; :: thesis: verum

end;

0 in Segm n by NAT_1:45;
then A24: 0. (INT.Ring n) = 0 by FUNCT_7:def 1;
A25: for a being Element of holds a + (0. (INT.Ring n)) = a

proof

let a be Element of ; :: 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 A24, Th17; :: thesis: verum

end;

A26: INT.Ring n is right_complementable

proof

let a be Element of ; :: 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 A27: 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 A24, A25, A27; :: thesis: verum

end;

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

then reconsider b = n - a' as Element of Segm n by Lm11;
reconsider v = b as Element of ;
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 A24, NAT_D:25 ; :: thesis: verum

end;

end;

end;

A28: for a, b, c being Element of holds (b + c) * a = (b * a) + (c * a)

proof

let a, b, c be Element of ; :: 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 ;
A29: aa < n by NAT_1:45;
A30: (((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 A29, Th10 ;
(bb + cc) mod n < n by Th9;
then A31: (b' + c') mod n is Element of Segm n by NAT_1:45;
(cc * aa) mod n < n by Th9;
then A32: (c' * a') mod n is Element of Segm n by NAT_1:45;
(bb * aa) mod n < n by Th9;
then A33: (b' * a') mod n is Element of Segm n by NAT_1:45;
A34: (b + c) * a = (multint n) . ((b' + c') mod n),a' by GR_CY_1:def 5
.= (((b' + c') mod n) * a') mod n by A31, Def11 ;
(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 A33, A32, GR_CY_1:def 5 ;
hence (b + c) * a = (b * a) + (c * a) by A34, A30; :: thesis: verum

end;

for a, b, c being Element of holds a * (b + c) = (a * b) + (a * c)

proof

let a, b, c be Element of ; :: 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 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 A24, A2, STRUCT_0:def 8;
hence ( not INT.Ring n is degenerated & INT.Ring n is commutative well-unital distributive Ring ) ; :: thesis: verum