let k, n be Element of NAT ; :: thesis: for G being finite strict Group
for a being Element of G st G = gr {a} & card G = n holds
( G = gr {(a |^ k)} iff k gcd n = 1 )
let G be finite strict Group; :: thesis: for a being Element of G st G = gr {a} & card G = n holds
( G = gr {(a |^ k)} iff k gcd n = 1 )
let a be Element of G; :: thesis: ( G = gr {a} & card G = n implies ( G = gr {(a |^ k)} iff k gcd n = 1 ) )
assume that
A1: G = gr {a} and
A2: card G = n ; :: thesis: ( G = gr {(a |^ k)} iff k gcd n = 1 )
A3: ( G = gr {(a |^ k)} implies k gcd n = 1 )

proof

set d = k gcd n;
assume that
A4: G = gr {(a |^ k)} and
A5: k gcd n <> 1 ; :: thesis: contradiction
k gcd n divides n by NAT_D:def 5;
then consider p being Nat such that
A6: n = (k gcd n) * p by NAT_D:def 3;
A7: p <> 0 by A2, A6;
A8: p <> n

proof

assume p = n ; :: thesis: contradiction
then (k gcd n) * p = p * 1 by A6;
hence contradiction by A5, A2, A6, XCMPLX_1:5; :: thesis: verum

end;

k gcd n divides k by NAT_D:def 5;
then consider l being Nat such that
A9: k = (k gcd n) * l by NAT_D:def 3;
A10: not a |^ k is being_of_order_0 by GR_CY_1:6;
(a |^ k) |^ p = a |^ ((l * (k gcd n)) * p) by A9, GROUP_1:35
.= a |^ (n * l) by A6
.= (a |^ n) |^ l by GROUP_1:35
.= (1_ G) |^ l by A2, GR_CY_1:9
.= 1_ G by GROUP_1:31 ;
then A11: ord (a |^ k) <= p by A7, A10, GROUP_1:def 11;
p divides n by A6, NAT_D:def 3;
then p <= n by A2, NAT_D:7;
then p < n by A8, XXREAL_0:1;
hence contradiction by A2, A4, A11, GR_CY_1:7; :: thesis: verum

end;

( k gcd n = 1 implies G = gr {(a |^ k)} )

proof

assume k gcd n = 1 ; :: thesis: G = gr {(a |^ k)}
then consider i, i1 being Integer such that
A12: (i * k) + (i1 * n) = 1 by NEWTON:67;
for b being Element of G holds b in gr {(a |^ k)}

proof

let b be Element of G; :: thesis: b in gr {(a |^ k)}
b in G by STRUCT_0:def 5;
then consider i0 being Integer such that
A13: b = a |^ i0 by A1, GR_CY_1:5;
A14: i0 = ((k * i) + (n * i1)) * i0 by A12
.= ((k * i) * i0) + ((n * i1) * i0) ;
ex i2 being Integer st b = (a |^ k) |^ i2

proof

take i * i0 ; :: thesis: b = (a |^ k) |^ (i * i0)
b = (a |^ ((k * i) * i0)) * (a |^ (n * (i1 * i0))) by A13, A14, GROUP_1:33
.= (a |^ ((k * i) * i0)) * ((a |^ n) |^ (i1 * i0)) by GROUP_1:35
.= (a |^ ((k * i) * i0)) * ((1_ G) |^ (i1 * i0)) by A2, GR_CY_1:9
.= (a |^ ((k * i) * i0)) * (1_ G) by GROUP_1:31
.= a |^ (k * (i * i0)) by GROUP_1:def 4
.= (a |^ k) |^ (i * i0) by GROUP_1:35 ;
hence b = (a |^ k) |^ (i * i0) ; :: thesis: verum

end;

hence b in gr {(a |^ k)} by GR_CY_1:5; :: thesis: verum

end;

hence G = gr {(a |^ k)} by GROUP_2:62; :: thesis: verum

end;

hence ( G = gr {(a |^ k)} iff k gcd n = 1 ) by A3; :: thesis: verum