let p be natural prime number ; :: thesis: for G being finite Group st ( for a being Element of G holds a is p -power ) holds
G is p -group
let G be finite Group; :: thesis: ( ( for a being Element of G holds a is p -power ) implies G is p -group )
assume A1: for a being Element of G holds a is p -power ; :: thesis: G is p -group
assume not G is p -group ; :: thesis: contradiction
then for r being natural number holds card G <> p |^ r by GROUP_10:def 17;
then consider s being Element of NAT such that
A2: ( s is prime & s divides card G ) and
A3: s <> p by Th1;
consider b being Element of G such that
A4: ord b = s by A2, GROUP_10:11;
b is p -power by A1;
then ex r1 being natural number st ord b = p |^ r1 by Def1;
hence contradiction by A2, A4, A3, NAT_3:6; :: thesis: verum