let G be strict Group; :: thesis: ( ex a being Element of G st a <> 1_ G implies ( ( for H being strict Subgroup of G holds

( H = G or H = (1). G ) ) iff ( G is cyclic & G is finite & ex p being Element of NAT st

( card G = p & p is prime ) ) ) )

assume A1: ex a being Element of G st a <> 1_ G ; :: thesis: ( ( for H being strict Subgroup of G holds

( H = G or H = (1). G ) ) iff ( G is cyclic & G is finite & ex p being Element of NAT st

( card G = p & p is prime ) ) )

thus ( ( for H being strict Subgroup of G holds

( H = G or H = (1). G ) ) implies ( G is cyclic & G is finite & ex p being Element of NAT st

( card G = p & p is prime ) ) ) :: thesis: ( G is cyclic & G is finite & ex p being Element of NAT st

( card G = p & p is prime ) implies for H being strict Subgroup of G holds

( H = G or H = (1). G ) )

G is cyclic and

A25: G is finite and

A26: ex p being Element of NAT st

( card G = p & p is prime ) ; :: thesis: for H being strict Subgroup of G holds

( H = G or H = (1). G )

let H be strict Subgroup of G; :: thesis: ( H = G or H = (1). G )

reconsider G = G as finite Group by A25;

reconsider H = H as Subgroup of G ;

card G = (card H) * (index H) by GROUP_2:147;

then A27: card H divides card G by NAT_D:def 3;

( H = G or H = (1). G ) ) iff ( G is cyclic & G is finite & ex p being Element of NAT st

( card G = p & p is prime ) ) ) )

assume A1: ex a being Element of G st a <> 1_ G ; :: thesis: ( ( for H being strict Subgroup of G holds

( H = G or H = (1). G ) ) iff ( G is cyclic & G is finite & ex p being Element of NAT st

( card G = p & p is prime ) ) )

thus ( ( for H being strict Subgroup of G holds

( H = G or H = (1). G ) ) implies ( G is cyclic & G is finite & ex p being Element of NAT st

( card G = p & p is prime ) ) ) :: thesis: ( G is cyclic & G is finite & ex p being Element of NAT st

( card G = p & p is prime ) implies for H being strict Subgroup of G holds

( H = G or H = (1). G ) )

proof

assume that
assume A2:
for H being strict Subgroup of G holds

( H = G or H = (1). G ) ; :: thesis: ( G is cyclic & G is finite & ex p being Element of NAT st

( card G = p & p is prime ) )

consider b being Element of G such that

A3: b <> 1_ G by A1;

A4: gr {b} = G by A2, A3, Th7;

A5: not b is being_of_order_0

A9: n = ord b and

not b is being_of_order_0 ;

A10: G is finite by A4, A5, Th11;

then A11: card G = n by A4, A9, GR_CY_1:7;

n is prime

( card G = p & p is prime ) ) by A4, A5, A11, Th11, GR_CY_2:4; :: thesis: verum

end;( H = G or H = (1). G ) ; :: thesis: ( G is cyclic & G is finite & ex p being Element of NAT st

( card G = p & p is prime ) )

consider b being Element of G such that

A3: b <> 1_ G by A1;

A4: gr {b} = G by A2, A3, Th7;

A5: not b is being_of_order_0

proof

then consider n being Element of NAT such that
assume A6:
b is being_of_order_0
; :: thesis: contradiction

then A7: b |^ 2 <> 1_ G by GROUP_1:def 10;

not b in gr {(b |^ 2)}

hence contradiction by A2, A7, Th7; :: thesis: verum

end;then A7: b |^ 2 <> 1_ G by GROUP_1:def 10;

not b in gr {(b |^ 2)}

proof

then
gr {(b |^ 2)} <> G
;
assume
b in gr {(b |^ 2)}
; :: thesis: contradiction

then consider j1 being Integer such that

A8: b = (b |^ 2) |^ j1 by GR_CY_1:5;

b = b |^ (2 * j1) by A8, GROUP_1:35;

then (b ") * (b |^ (2 * j1)) = 1_ G by GROUP_1:def 5;

then (b |^ (- 1)) * (b |^ (2 * j1)) = 1_ G by GROUP_1:32;

then b |^ ((- 1) + (2 * j1)) = 1_ G by GROUP_1:33;

then (- 1) + (2 * j1) = 0 by A6, Th13;

hence contradiction by INT_1:9; :: thesis: verum

end;then consider j1 being Integer such that

A8: b = (b |^ 2) |^ j1 by GR_CY_1:5;

b = b |^ (2 * j1) by A8, GROUP_1:35;

then (b ") * (b |^ (2 * j1)) = 1_ G by GROUP_1:def 5;

then (b |^ (- 1)) * (b |^ (2 * j1)) = 1_ G by GROUP_1:32;

then b |^ ((- 1) + (2 * j1)) = 1_ G by GROUP_1:33;

then (- 1) + (2 * j1) = 0 by A6, Th13;

hence contradiction by INT_1:9; :: thesis: verum

hence contradiction by A2, A7, Th7; :: thesis: verum

A9: n = ord b and

not b is being_of_order_0 ;

A10: G is finite by A4, A5, Th11;

then A11: card G = n by A4, A9, GR_CY_1:7;

n is prime

proof

hence
( G is cyclic & G is finite & ex p being Element of NAT st
assume A12:
not n is prime
; :: thesis: contradiction

ex u, v being Element of NAT st

( u > 1 & v > 1 & n = u * v )

A20: u > 1 and

A21: v > 1 and

A22: n = u * v ;

ord (b |^ v) = u by A4, A10, A11, A22, GR_CY_2:8;

then A23: card (gr {(b |^ v)}) = u by A10, GR_CY_1:7;

A24: u <> n by A20, A21, A22, XCMPLX_1:7;

gr {(b |^ v)} <> (1). G by A20, A23, GROUP_2:69;

hence contradiction by A2, A11, A23, A24; :: thesis: verum

end;ex u, v being Element of NAT st

( u > 1 & v > 1 & n = u * v )

proof

then consider u, v being Element of NAT such that
A13:
( not n > 1 or ex m being Nat st

( m divides n & not m = 1 & not m = n ) ) by A12, INT_2:def 4;

n >= 1 by A10, A11, GROUP_1:45;

then n > 1 by A3, A9, GROUP_1:43, XXREAL_0:1;

then consider m being Nat such that

A14: m <> 1 and

A15: m <> n and

A16: m divides n by A13;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

consider o being Nat such that

A17: n = m * o by A16, NAT_D:def 3;

reconsider o = o as Element of NAT by ORDINAL1:def 12;

take u = m; :: thesis: ex v being Element of NAT st

( u > 1 & v > 1 & n = u * v )

take v = o; :: thesis: ( u > 1 & v > 1 & n = u * v )

u <> 0

0 < v by A10, A11, A17;

then A19: 0 + 1 <= v by INT_1:7;

v <> 1 by A15, A17;

hence ( u > 1 & v > 1 & n = u * v ) by A14, A17, A18, A19, XXREAL_0:1; :: thesis: verum

end;( m divides n & not m = 1 & not m = n ) ) by A12, INT_2:def 4;

n >= 1 by A10, A11, GROUP_1:45;

then n > 1 by A3, A9, GROUP_1:43, XXREAL_0:1;

then consider m being Nat such that

A14: m <> 1 and

A15: m <> n and

A16: m divides n by A13;

reconsider m = m as Element of NAT by ORDINAL1:def 12;

consider o being Nat such that

A17: n = m * o by A16, NAT_D:def 3;

reconsider o = o as Element of NAT by ORDINAL1:def 12;

take u = m; :: thesis: ex v being Element of NAT st

( u > 1 & v > 1 & n = u * v )

take v = o; :: thesis: ( u > 1 & v > 1 & n = u * v )

u <> 0

proof

then A18:
0 + 1 <= u
by INT_1:7;
assume
u = 0
; :: thesis: contradiction

then n = 0 * (n div 0) by A16, NAT_D:3;

hence contradiction by A10, A11; :: thesis: verum

end;then n = 0 * (n div 0) by A16, NAT_D:3;

hence contradiction by A10, A11; :: thesis: verum

0 < v by A10, A11, A17;

then A19: 0 + 1 <= v by INT_1:7;

v <> 1 by A15, A17;

hence ( u > 1 & v > 1 & n = u * v ) by A14, A17, A18, A19, XXREAL_0:1; :: thesis: verum

A20: u > 1 and

A21: v > 1 and

A22: n = u * v ;

ord (b |^ v) = u by A4, A10, A11, A22, GR_CY_2:8;

then A23: card (gr {(b |^ v)}) = u by A10, GR_CY_1:7;

A24: u <> n by A20, A21, A22, XCMPLX_1:7;

gr {(b |^ v)} <> (1). G by A20, A23, GROUP_2:69;

hence contradiction by A2, A11, A23, A24; :: thesis: verum

( card G = p & p is prime ) ) by A4, A5, A11, Th11, GR_CY_2:4; :: thesis: verum

G is cyclic and

A25: G is finite and

A26: ex p being Element of NAT st

( card G = p & p is prime ) ; :: thesis: for H being strict Subgroup of G holds

( H = G or H = (1). G )

let H be strict Subgroup of G; :: thesis: ( H = G or H = (1). G )

reconsider G = G as finite Group by A25;

reconsider H = H as Subgroup of G ;

card G = (card H) * (index H) by GROUP_2:147;

then A27: card H divides card G by NAT_D:def 3;