let n, p, s be Element of NAT ; for G being finite Group
for a being Element of G st G = gr {a} & card G = n & n = p * s holds
ord (a |^ p) = s
let G be finite Group; for a being Element of G st G = gr {a} & card G = n & n = p * s holds
ord (a |^ p) = s
let a be Element of G; ( G = gr {a} & card G = n & n = p * s implies ord (a |^ p) = s )
assume that
A1:
G = gr {a}
and
A2:
card G = n
and
A3:
n = p * s
; ord (a |^ p) = s
A4:
( not a |^ p is being_of_order_0 & s <> 0 )
by A2, A3, GR_CY_1:6;
A5:
p <> 0
by A2, A3;
A6:
for k being Nat st (a |^ p) |^ k = 1_ G & k <> 0 holds
s <= k
proof
let k be
Nat;
( (a |^ p) |^ k = 1_ G & k <> 0 implies s <= k )
assume that A7:
(a |^ p) |^ k = 1_ G
and A8:
(
k <> 0 &
s > k )
;
contradiction
A9:
a |^ (p * k) = 1_ G
by A7, GROUP_1:35;
A10:
(
ord a = n & not
a is
being_of_order_0 )
by A1, A2, GR_CY_1:6, GR_CY_1:7;
(
p * s > p * k &
p * k <> 0 )
by A5, A8, XCMPLX_1:6, XREAL_1:68;
hence
contradiction
by A3, A10, A9, GROUP_1:def 11;
verum
end;
(a |^ p) |^ s =
a |^ n
by A3, GROUP_1:35
.=
1_ G
by A2, GR_CY_1:9
;
hence
ord (a |^ p) = s
by A4, A6, GROUP_1:def 11; verum