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 )
A3:
n > 0
by A2, GROUP_1:90;
A4:
( G = gr {(a |^ k)} implies k gcd n = 1 )
proof
assume that A5:
G = gr {(a |^ k)}
and A6:
k gcd n <> 1
;
:: thesis: contradiction
set d =
k gcd n;
A7:
k gcd n divides k
by NAT_D:def 5;
A8:
k gcd n divides n
by NAT_D:def 5;
consider l being
Nat such that A9:
k = (k gcd n) * l
by A7, NAT_D:def 3;
consider p being
Nat such that A10:
n = (k gcd n) * p
by A8, NAT_D:def 3;
A11:
p divides n
by A10, NAT_D:def 3;
A12:
(a |^ k) |^ p =
a |^ ((l * (k gcd n)) * p)
by A9, GROUP_1:67
.=
a |^ (n * l)
by A10
.=
(a |^ n) |^ l
by GROUP_1:67
.=
(1_ G) |^ l
by A2, GR_CY_1:29
.=
1_ G
by GROUP_1:61
;
A13:
p <> 0
by A2, A10, GROUP_1:90;
A14:
p < n
not
a |^ k is
being_of_order_0
by GR_CY_1:26;
then
ord (a |^ k) <= p
by A12, A13, GROUP_1:def 12;
hence
contradiction
by A2, A5, A14, GR_CY_1:27;
:: thesis: verum
end;
( k gcd n = 1 implies G = gr {(a |^ k)} )
hence
( G = gr {(a |^ k)} iff k gcd n = 1 )
by A4; :: thesis: verum