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	|- B = ( Base ` G )
Assertion	prmsimpcyc	|- ( ( # ` B ) e. Prime -> ( G e. SimpGrp <-> G e. CycGrp ) )

Proof

Step	Hyp	Ref	Expression
1		prmsimpcyc.1	|- B = ( Base ` G )
2		simpggrp	|- ( G e. SimpGrp -> G e. Grp )
3		id	|- ( ( # ` B ) e. Prime -> ( # ` B ) e. Prime )
4	1	prmcyg	|- ( ( G e. Grp /\ ( # ` B ) e. Prime ) -> G e. CycGrp )
5	2 3 4	syl2anr	|- ( ( ( # ` B ) e. Prime /\ G e. SimpGrp ) -> G e. CycGrp )
6		cyggrp	|- ( G e. CycGrp -> G e. Grp )
7	6	adantl	|- ( ( ( # ` B ) e. Prime /\ G e. CycGrp ) -> G e. Grp )
8		simpl	|- ( ( ( # ` B ) e. Prime /\ G e. CycGrp ) -> ( # ` B ) e. Prime )
9	1 7 8	prmgrpsimpgd	|- ( ( ( # ` B ) e. Prime /\ G e. CycGrp ) -> G e. SimpGrp )
10	5 9	impbida	|- ( ( # ` B ) e. Prime -> ( G e. SimpGrp <-> G e. CycGrp ) )