let G be finite Group; for p being prime Nat st p divides card G holds
ex g being Element of G st ord g = p
let p be prime Nat; ( p divides card G implies ex g being Element of G st ord g = p )
reconsider p9 = p as prime Element of NAT by ORDINAL1:def 12;
A1:
1 < p9
by NAT_4:12;
consider P being strict Subgroup of G such that
A2:
P is_Sylow_p-subgroup_of_prime p
by Th10;
P is p -group
by A2;
then consider H being finite Group such that
A3:
P = H
and
A4:
H is p -group
;
consider r being Nat such that
A5:
card H = p |^ r
by A4;
assume A6:
p divides card G
; ex g being Element of G st ord g = p
then
0 + 1 < r + 1
by XREAL_1:6;
then
1 <= r
by NAT_1:13;
then
1 - 1 <= r - 1
by XREAL_1:9;
then reconsider r9 = r - 1 as Element of NAT by INT_1:3;
0 + 1 < (p9 |^ r9) + 1
by XREAL_1:6;
then
1 <= p |^ r9
by NAT_1:13;
then A7:
1 * p <= (p |^ r9) * p
by XREAL_1:64;
set H9 = (Omega). H;
A8:
card H = (card ((Omega). H)) * 1
;
p |^ r =
p |^ (r9 + 1)
.=
(p |^ r9) * p
by NEWTON:6
;
then
card ((Omega). H) > 1
by A5, A7, A1, XXREAL_0:2;
then consider g being Element of ((Omega). H) such that
A9:
g <> 1_ ((Omega). H)
by GR_CY_1:11;
reconsider H99 = gr {g} as strict Group ;
A10:
H99 is cyclic Group
by GR_CY_2:4;
reconsider H99 = H99 as finite strict Group ;
set n = card H99;
card H99 >= 1
by GROUP_1:45;
then
card H99 > 1
by A11, XXREAL_0:1;
then
p divides card H99
by A5, A8, Lm8, GROUP_2:148;
then consider H999 being strict Subgroup of H99 such that
A12:
card H999 = p9
and
for G2 being strict Subgroup of H99 st card G2 = p9 holds
G2 = H999
by A10, GR_CY_2:22;
consider h9 being Element of H999 such that
A13:
ord h9 = p
by A12, GROUP_8:1;
H99 is Subgroup of G
by A3, GROUP_2:56;
then reconsider H999 = H999 as strict Subgroup of G by GROUP_2:56;
reconsider h9 = h9 as Element of H999 ;
reconsider h = h9 as Element of G by GROUP_2:42;
take
h
; ord h = p
thus
ord h = p
by A13, GROUP_8:5; verum