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, Lm7;
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, Lm7; :: thesis: verum
end;
A6: INT.Ring n is well-unital by A3;
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) ) )
per cases ( a9 + b9 < n or a9 + b9 >= n ) ;
case A8: 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;
case A9: 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 Lm5;
(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 SUBSET_1:def 8;
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 ;
per cases ( a9 = 0 or a9 <> 0 ) ;
suppose a9 <> 0 ; :: thesis: a is right_complementable
then reconsider b = n - a9 as Element of Segm n by Lm6;
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;
hence ( not INT.Ring n is degenerated & INT.Ring n is commutative Ring ) ; :: thesis: verum