Metamath Proof Explorer

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=BaseG
Assertion prmsimpcyc ⊢B∈ℙ→G∈SimpGrp↔G∈CycGrp

Proof

Step Hyp Ref Expression
1 prmsimpcyc.1 ⊢B=BaseG
2 simpggrp ⊢G∈SimpGrp→G∈Grp
3 id ⊢B∈ℙ→B∈ℙ
4 1 prmcyg ⊢G∈Grp∧B∈ℙ→G∈CycGrp
5 2 3 4 syl2anr ⊢B∈ℙ∧G∈SimpGrp→G∈CycGrp
6 cyggrp ⊢G∈CycGrp→G∈Grp
7 6 adantl ⊢B∈ℙ∧G∈CycGrp→G∈Grp
8 simpl ⊢B∈ℙ∧G∈CycGrp→B∈ℙ
9 1 7 8 prmgrpsimpgd ⊢B∈ℙ∧G∈CycGrp→G∈SimpGrp
10 5 9 impbida ⊢B∈ℙ→G∈SimpGrp↔G∈CycGrp