let k, n, p be Element of NAT ; :: thesis: for G being finite Group

for G1 being Subgroup of G

for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds

n divides k * p

let G be finite Group; :: thesis: for G1 being Subgroup of G

for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds

n divides k * p

let G1 be Subgroup of G; :: thesis: for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds

n divides k * p

let a be Element of G; :: thesis: ( card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} implies n divides k * p )

assume that

A1: card G = n and

A2: G = gr {a} and

A3: card G1 = p and

A4: G1 = gr {(a |^ k)} ; :: thesis: n divides k * p

set z = k * p;

consider m, l being Nat such that

A5: k * p = (n * m) + l and

A6: l < n by A1, NAT_1:17;

l = 0

for G1 being Subgroup of G

for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds

n divides k * p

let G be finite Group; :: thesis: for G1 being Subgroup of G

for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds

n divides k * p

let G1 be Subgroup of G; :: thesis: for a being Element of G st card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} holds

n divides k * p

let a be Element of G; :: thesis: ( card G = n & G = gr {a} & card G1 = p & G1 = gr {(a |^ k)} implies n divides k * p )

assume that

A1: card G = n and

A2: G = gr {a} and

A3: card G1 = p and

A4: G1 = gr {(a |^ k)} ; :: thesis: n divides k * p

set z = k * p;

consider m, l being Nat such that

A5: k * p = (n * m) + l and

A6: l < n by A1, NAT_1:17;

l = 0

proof

hence
n divides k * p
by A5, NAT_D:def 3; :: thesis: verum
a |^ k in gr {(a |^ k)}
by Th2;

then reconsider h = a |^ k as Element of G1 by A4, STRUCT_0:def 5;

assume A7: l <> 0 ; :: thesis: contradiction

a |^ (k * p) = (a |^ k) |^ p by GROUP_1:35

.= h |^ p by GROUP_4:1

.= 1_ G1 by A3, GR_CY_1:9

.= 1_ G by GROUP_2:44 ;

then A8: 1_ G = (a |^ (n * m)) * (a |^ l) by A5, GROUP_1:33

.= ((a |^ n) |^ m) * (a |^ l) by GROUP_1:35

.= ((1_ G) |^ m) * (a |^ l) by A1, GR_CY_1:9

.= (1_ G) * (a |^ l) by GROUP_1:31

.= a |^ l by GROUP_1:def 4 ;

( not a is being_of_order_0 & ord a = n ) by A1, A2, GR_CY_1:6, GR_CY_1:7;

hence contradiction by A6, A7, A8, GROUP_1:def 11; :: thesis: verum

end;then reconsider h = a |^ k as Element of G1 by A4, STRUCT_0:def 5;

assume A7: l <> 0 ; :: thesis: contradiction

a |^ (k * p) = (a |^ k) |^ p by GROUP_1:35

.= h |^ p by GROUP_4:1

.= 1_ G1 by A3, GR_CY_1:9

.= 1_ G by GROUP_2:44 ;

then A8: 1_ G = (a |^ (n * m)) * (a |^ l) by A5, GROUP_1:33

.= ((a |^ n) |^ m) * (a |^ l) by GROUP_1:35

.= ((1_ G) |^ m) * (a |^ l) by A1, GR_CY_1:9

.= (1_ G) * (a |^ l) by GROUP_1:31

.= a |^ l by GROUP_1:def 4 ;

( not a is being_of_order_0 & ord a = n ) by A1, A2, GR_CY_1:6, GR_CY_1:7;

hence contradiction by A6, A7, A8, GROUP_1:def 11; :: thesis: verum