let p be prime Nat; :: thesis: for G being finite Group
for N being normal Subgroup of G st N is p -group & G ./. N is p -group holds
G is p -group
let G be finite Group; :: thesis: for N being normal Subgroup of G st N is p -group & G ./. N is p -group holds
G is p -group
let N be normal Subgroup of G; :: thesis: ( N is p -group & G ./. N is p -group implies G is p -group )
assume that
A1: N is p -group and
A2: G ./. N is p -group ; :: thesis: G is p -group
consider r1 being Nat such that
A3: card N = p |^ r1 by A1;
consider r2 being Nat such that
A4: card (G ./. N) = p |^ r2 by A2;
card (G ./. N) = index N by GROUP_6:27;
then card G = (p |^ r1) * (p |^ r2) by A3, A4, GROUP_2:147
.= p |^ (r1 + r2) by NEWTON:8 ;
hence G is p -group ; :: thesis: verum