Theorem prmsimpcyc

Description: A group of prime order is cyclic if and only if it is simple. This is the first family of finite simple groups. (Contributed by Thierry Arnoux, 21-Sep-2023)

	Ref	Expression
Hypothesis	prmsimpcyc.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	prmsimpcyc	⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℙ → ( 𝐺 ∈ SimpGrp ↔ 𝐺 ∈ CycGrp ) )

Proof

Step	Hyp	Ref	Expression
1		prmsimpcyc.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		simpggrp	⊢ ( 𝐺 ∈ SimpGrp → 𝐺 ∈ Grp )
3		id	⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℙ → ( ♯ ‘ 𝐵 ) ∈ ℙ )
4	1	prmcyg	⊢ ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) ∈ ℙ ) → 𝐺 ∈ CycGrp )
5	2 3 4	syl2anr	⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℙ ∧ 𝐺 ∈ SimpGrp ) → 𝐺 ∈ CycGrp )
6		cyggrp	⊢ ( 𝐺 ∈ CycGrp → 𝐺 ∈ Grp )
7	6	adantl	⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℙ ∧ 𝐺 ∈ CycGrp ) → 𝐺 ∈ Grp )
8		simpl	⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℙ ∧ 𝐺 ∈ CycGrp ) → ( ♯ ‘ 𝐵 ) ∈ ℙ )
9	1 7 8	prmgrpsimpgd	⊢ ( ( ( ♯ ‘ 𝐵 ) ∈ ℙ ∧ 𝐺 ∈ CycGrp ) → 𝐺 ∈ SimpGrp )
10	5 9	impbida	⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℙ → ( 𝐺 ∈ SimpGrp ↔ 𝐺 ∈ CycGrp ) )