let k, n, p be Element of NAT ; 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; 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; 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; ( 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)}
; 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
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
;
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;
verum
end;
hence
n divides k * p
by A5, NAT_D:def 3; verum