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 )

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

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

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

k gcd n divides k
by NAT_D:def 5;
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;then (k gcd n) * p = p * 1 by A6;

hence contradiction by A5, A2, A6, XCMPLX_1:5; :: thesis: verum

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

proof

hence
( G = gr {(a |^ k)} iff k gcd n = 1 )
by A3; :: thesis: verum
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)}

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

hence
G = gr {(a |^ k)}
by GROUP_2:62; :: thesis: verum
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

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

hence
b in gr {(a |^ k)}
by GR_CY_1:5; :: thesis: verum
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;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