let n be Element of NAT ; :: thesis: for G being finite strict Group st G is cyclic & card G = n holds
for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
let G be finite strict Group; :: thesis: ( G is cyclic & card G = n implies for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) ) )
assume that
A1: G is cyclic and
A2: card G = n ; :: thesis: for p being Element of NAT st p divides n holds
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
let p be Element of NAT ; :: thesis: ( p divides n implies ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) ) )
assume A3: p divides n ; :: thesis: ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )
ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) )

proof

consider a being Element of G such that
A4: G = gr {a} by A1, GR_CY_1:def 9;
consider s being Nat such that
A5: n = p * s by A3, NAT_D:def 3;
A6: s in NAT by ORDINAL1:def 13;
then A7: ord (a |^ s) = p by A2, A4, A5, Th14;
then A8: card (gr {(a |^ s)}) = p by GR_CY_1:27;
A9: for G2 being strict Subgroup of G st card G2 = p holds
G2 = gr {(a |^ s)}

proof

let G2 be strict Subgroup of G; :: thesis: ( card G2 = p implies G2 = gr {(a |^ s)} )
assume A10: card G2 = p ; :: thesis: G2 = gr {(a |^ s)}
consider k being Element of NAT such that
A11: G2 = gr {(a |^ k)} by A4, Th13;
n divides k * p by A2, A4, A10, A11, Th17;
then consider m being Nat such that
A12: k * p = n * m by NAT_D:def 3;
s divides k

proof

ex l being Nat st k = s * l

proof

reconsider p1 = p as Integer ;
A13: p <> 0 by A2, A5, GROUP_1:90;
((1 / p1) * p1) * k = (1 / p1) * ((p1 * s) * m) by A5, A12, XCMPLX_1:4;
then 1 * k = ((p1 * (1 / p1)) * s) * m by A13, XCMPLX_1:107;
then A14: k = (1 * s) * m by A13, XCMPLX_1:107;
take m ; :: thesis: k = s * m
thus k = s * m by A14; :: thesis: verum

end;

hence s divides k by NAT_D:def 3; :: thesis: verum

end;

hence G2 = gr {(a |^ s)} by A6, A8, A10, A11, Th15, Th16; :: thesis: verum

end;

take gr {(a |^ s)} ; :: thesis: ( card (gr {(a |^ s)}) = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = gr {(a |^ s)} ) )
thus ( card (gr {(a |^ s)}) = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = gr {(a |^ s)} ) ) by A7, A9, GR_CY_1:27; :: thesis: verum

end;

hence ex G1 being strict Subgroup of G st
( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds
G2 = G1 ) ) ; :: thesis: verum