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 ) )

( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds

G2 = G1 ) ) ; :: thesis: verum

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

hence
ex G1 being strict Subgroup of G st
consider s being Nat such that

A4: n = p * s by A3, NAT_D:def 3;

consider a being Element of G such that

A5: G = gr {a} by A1;

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)} ) )

A6: s in NAT by ORDINAL1:def 12;

then A7: ord (a |^ s) = p by A2, A5, A4, Th8;

then A8: card (gr {(a |^ s)}) = p by GR_CY_1:7;

for G2 being strict Subgroup of G st card G2 = p holds

G2 = gr {(a |^ s)}

G2 = gr {(a |^ s)} ) ) by A7, GR_CY_1:7; :: thesis: verum

end;A4: n = p * s by A3, NAT_D:def 3;

consider a being Element of G such that

A5: G = gr {a} by A1;

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)} ) )

A6: s in NAT by ORDINAL1:def 12;

then A7: ord (a |^ s) = p by A2, A5, A4, Th8;

then A8: card (gr {(a |^ s)}) = p by GR_CY_1:7;

for G2 being strict Subgroup of G st card G2 = p holds

G2 = gr {(a |^ s)}

proof

hence
( card (gr {(a |^ s)}) = p & ( for G2 being strict Subgroup of G st card G2 = p holds
let G2 be strict Subgroup of G; :: thesis: ( card G2 = p implies G2 = gr {(a |^ s)} )

assume A9: card G2 = p ; :: thesis: G2 = gr {(a |^ s)}

consider k being Element of NAT such that

A10: G2 = gr {(a |^ k)} by A5, Th7;

n divides k * p by A2, A5, A9, A10, Th11;

then consider m being Nat such that

A11: k * p = n * m by NAT_D:def 3;

ex l being Nat st k = s * l

hence G2 = gr {(a |^ s)} by A6, A8, A9, A10, Th9, Th10; :: thesis: verum

end;assume A9: card G2 = p ; :: thesis: G2 = gr {(a |^ s)}

consider k being Element of NAT such that

A10: G2 = gr {(a |^ k)} by A5, Th7;

n divides k * p by A2, A5, A9, A10, Th11;

then consider m being Nat such that

A11: k * p = n * m by NAT_D:def 3;

ex l being Nat st k = s * l

proof

then
s divides k
by NAT_D:def 3;
take
m
; :: thesis: k = s * m

reconsider p1 = p as Integer ;

A12: p <> 0 by A2, A4;

((1 / p1) * p1) * k = (1 / p1) * ((p1 * s) * m) by A4, A11, XCMPLX_1:4;

then 1 * k = ((p1 * (1 / p1)) * s) * m by A12, XCMPLX_1:106;

then k = (1 * s) * m by A12, XCMPLX_1:106;

hence k = s * m ; :: thesis: verum

end;reconsider p1 = p as Integer ;

A12: p <> 0 by A2, A4;

((1 / p1) * p1) * k = (1 / p1) * ((p1 * s) * m) by A4, A11, XCMPLX_1:4;

then 1 * k = ((p1 * (1 / p1)) * s) * m by A12, XCMPLX_1:106;

then k = (1 * s) * m by A12, XCMPLX_1:106;

hence k = s * m ; :: thesis: verum

hence G2 = gr {(a |^ s)} by A6, A8, A9, A10, Th9, Th10; :: thesis: verum

G2 = gr {(a |^ s)} ) ) by A7, GR_CY_1:7; :: thesis: verum

( card G1 = p & ( for G2 being strict Subgroup of G st card G2 = p holds

G2 = G1 ) ) ; :: thesis: verum