let n, p, s be Element of NAT ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

.= 1_ G by A2, GR_CY_1:9 ;

hence ord (a |^ p) = s by A4, A6, GROUP_1:def 11; :: thesis: verum

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

(a |^ p) |^ s =
a |^ n
by A3, GROUP_1:35
let k be Nat; :: thesis: ( (a |^ p) |^ k = 1_ G & k <> 0 implies s <= k )

assume that

A7: (a |^ p) |^ k = 1_ G and

A8: ( k <> 0 & s > k ) ; :: thesis: 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; :: thesis: verum

end;assume that

A7: (a |^ p) |^ k = 1_ G and

A8: ( k <> 0 & s > k ) ; :: thesis: 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; :: thesis: verum

.= 1_ G by A2, GR_CY_1:9 ;

hence ord (a |^ p) = s by A4, A6, GROUP_1:def 11; :: thesis: verum