let G be finite Group; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ord h = p
thus ord h = p by A13, GROUP_8:5; :: thesis: verum