set G = INT.Group n;
thus the carrier of (INT.Group n) is finite ; :: according to STRUCT_0:def 11 :: thesis: ( INT.Group n is associative & INT.Group n is Group-like )
reconsider e = 0 as Element of (INT.Group n) by NAT_1:44;
thus for h, g, f being Element of (INT.Group n) holds (h * g) * f = h * (g * f) :: according to GROUP_1:def 3 :: thesis: INT.Group n is Group-like
proof
let h, g, f be Element of (INT.Group n); :: thesis: (h * g) * f = h * (g * f)
reconsider A = h, B = g, C = f as Element of Segm n ;
A1: g * f = (B + C) mod n by Def4;
h * g = (A + B) mod n by Def4;
hence (h * g) * f = (((A + B) mod n) + C) mod n by Def4
.= ((A + B) + C) mod n by NAT_D:22
.= (A + (B + C)) mod n
.= (A + ((B + C) mod n)) mod n by NAT_D:22
.= h * (g * f) by A1, Def4 ;
:: thesis: verum
end;
take e ; :: according to GROUP_1:def 2 :: thesis: for b1 being Element of the carrier of (INT.Group n) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (INT.Group n) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of (INT.Group n); :: thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (INT.Group n) st
( h * b1 = e & b1 * h = e ) )
reconsider A = h as Element of Segm n ;
A2: A < n by NAT_1:44;
then consider p being Nat such that
A3: n = A + p by NAT_1:10;
thus h * e = (A + 0) mod n by Def4
.= h by A2, NAT_D:24 ; :: thesis: ( e * h = h & ex b1 being Element of the carrier of (INT.Group n) st
( h * b1 = e & b1 * h = e ) )
thus e * h = (0 + A) mod n by Def4
.= h by A2, NAT_D:24 ; :: thesis: ex b1 being Element of the carrier of (INT.Group n) st
( h * b1 = e & b1 * h = e )
p mod n < n by NAT_D:1;
then reconsider g = p mod n as Element of (INT.Group n) by NAT_1:44;
reconsider B = g as Element of Segm n ;
take g ; :: thesis: ( h * g = e & g * h = e )
A4: p <= n by A3, NAT_1:12;
thus h * g = e :: thesis: g * h = e
proof
per cases ( p = n or p < n ) by A4, XXREAL_0:1;
suppose A5: p = n ; :: thesis: h * g = e
h * g = (A + B) mod n by Def4
.= (0 * n) mod n by A3, A5, NAT_D:25
.= e by NAT_D:13 ;
hence h * g = e ; :: thesis: verum
end;
suppose A6: p < n ; :: thesis: h * g = e
h * g = (A + B) mod n by Def4
.= n mod n by A3, A6, NAT_D:24
.= e by NAT_D:25 ;
hence h * g = e ; :: thesis: verum
end;
end;
end;
thus g * h = e :: thesis: verum
proof
per cases ( p = n or p < n ) by A4, XXREAL_0:1;
suppose p = n ; :: thesis: g * h = e
then g * h = ((n mod n) + 0) mod n by A3, Def4
.= (0 * n) mod n by NAT_D:25
.= e by NAT_D:13 ;
hence g * h = e ; :: thesis: verum
end;
suppose A7: p < n ; :: thesis: g * h = e
g * h = (A + B) mod n by Def4
.= n mod n by A3, A7, NAT_D:24
.= e by NAT_D:25 ;
hence g * h = e ; :: thesis: verum
end;
end;
end;