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 )

A7: for a, b being Element of (INT.Ring n) holds a + b = b + a

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

not F is degenerated by A24, A2;

hence ( not INT.Ring n is degenerated & INT.Ring n is commutative Ring ) ; :: thesis: verum

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

A6:
INT.Ring n is well-unital
by A3;
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;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

A7: for a, b being Element of (INT.Ring n) holds a + b = b + a

proof

A10:
for a, b, c being Element of (INT.Ring n) holds (a * b) * c = a * (b * c)
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 ;

end;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) ) )

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

proof

A16:
for a, b being Element of (INT.Ring n) holds a * b = b * a
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;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

proof

A18:
for a, b, c being Element of (INT.Ring n) holds (a + b) + c = a + (b + c)
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;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

proof

0 in Segm n
by NAT_1:44;
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;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

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

A26:
INT.Ring n is right_complementable
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;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

proof

A28:
for a, b, c being Element of (INT.Ring n) holds (b + c) * a = (b * a) + (c * a)
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 ;

end;reconsider a9 = a as Element of Segm n ;

reconsider a9 = a9 as Element of NAT ;

per cases
( a9 = 0 or a9 <> 0 )
;

end;

suppose A27:
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;thus a + (0. (INT.Ring n)) = 0. (INT.Ring n) by A24, A25, A27; :: thesis: verum

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

proof

for a, b, c being Element of (INT.Ring n) holds a * (b + c) = (a * b) + (a * c)
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;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

proof

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

not F is degenerated by A24, A2;

hence ( not INT.Ring n is degenerated & INT.Ring n is commutative Ring ) ; :: thesis: verum