let n, k 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 )
A4: ( G = gr {(a |^ k)} implies k gcd n = 1 )

proof

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

proof

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

end;

k gcd n divides k by NAT_D:def 5;
then consider l being Nat such that
A10: k = (k gcd n) * l by NAT_D:def 3;
A11: not a |^ k is being_of_order_0 by GR_CY_1:6;
(a |^ k) |^ p = a |^ ((l * (k gcd n)) * p) by A10, GROUP_1:35
.= a |^ (n * l) by A7
.= (a |^ n) |^ l by GROUP_1:35
.= (1_ G) |^ l by A2, GR_CY_1:9
.= 1_ G by GROUP_1:31 ;
then A12: ord (a |^ k) <= p by A8, A11, GROUP_1:def 11;
p divides n by A7, NAT_D:def 3;
then p <= n by A2, NAT_D:7;
then p < n by A9, XXREAL_0:1;
hence contradiction by A2, A5, A12, 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
A13: (i * k) + (i1 * n) = 1 by A2, 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
A14: b = a |^ i0 by A1, GR_CY_1:5;
A15: i0 = ((k * i) + (n * i1)) * i0 by A13
.= ((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 A14, A15, 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 A4; :: thesis: verum