Metamath Proof Explorer

Theorem prmcyg

Description: A group with prime order is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypothesis cygctb.1 ⊢ B = Base G
Assertion prmcyg ⊢ G ∈ Grp ∧ B ∈ ℙ → G ∈ CycGrp

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢ B = Base G
2 1nprm ⊢ ¬ 1 ∈ ℙ
3 simpr ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ B ⊆ 0 G → B ⊆ 0 G
4 eqid ⊢ 0 G = 0 G
5 1 4 grpidcl ⊢ G ∈ Grp → 0 G ∈ B
6 5 snssd ⊢ G ∈ Grp → 0 G ⊆ B
7 6 ad2antrr ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ B ⊆ 0 G → 0 G ⊆ B
8 3 7 eqssd ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ B ⊆ 0 G → B = 0 G
9 8 fveq2d ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ B ⊆ 0 G → B = 0 G
10 fvex ⊢ 0 G ∈ V
11 hashsng ⊢ 0 G ∈ V → 0 G = 1
12 10 11 ax-mp ⊢ 0 G = 1
13 9 12 eqtrdi ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ B ⊆ 0 G → B = 1
14 simplr ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ B ⊆ 0 G → B ∈ ℙ
15 13 14 eqeltrrd ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ B ⊆ 0 G → 1 ∈ ℙ
16 15 ex ⊢ G ∈ Grp ∧ B ∈ ℙ → B ⊆ 0 G → 1 ∈ ℙ
17 2 16 mtoi ⊢ G ∈ Grp ∧ B ∈ ℙ → ¬ B ⊆ 0 G
18 nss ⊢ ¬ B ⊆ 0 G ↔ ∃ x x ∈ B ∧ ¬ x ∈ 0 G
19 17 18 sylib ⊢ G ∈ Grp ∧ B ∈ ℙ → ∃ x x ∈ B ∧ ¬ x ∈ 0 G
20 eqid ⊢ od ⁡ G = od ⁡ G
21 simpll ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → G ∈ Grp
22 simprl ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → x ∈ B
23 simprr ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → ¬ x ∈ 0 G
24 20 4 1 odeq1 ⊢ G ∈ Grp ∧ x ∈ B → od ⁡ G ⁡ x = 1 ↔ x = 0 G
25 21 22 24 syl2anc ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → od ⁡ G ⁡ x = 1 ↔ x = 0 G
26 velsn ⊢ x ∈ 0 G ↔ x = 0 G
27 25 26 bitr4di ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → od ⁡ G ⁡ x = 1 ↔ x ∈ 0 G
28 23 27 mtbird ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → ¬ od ⁡ G ⁡ x = 1
29 prmnn ⊢ B ∈ ℙ → B ∈ ℕ
30 29 ad2antlr ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → B ∈ ℕ
31 30 nnnn0d ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → B ∈ ℕ 0
32 1 fvexi ⊢ B ∈ V
33 hashclb ⊢ B ∈ V → B ∈ Fin ↔ B ∈ ℕ 0
34 32 33 ax-mp ⊢ B ∈ Fin ↔ B ∈ ℕ 0
35 31 34 sylibr ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → B ∈ Fin
36 1 20 oddvds2 ⊢ G ∈ Grp ∧ B ∈ Fin ∧ x ∈ B → od ⁡ G ⁡ x ∥ B
37 21 35 22 36 syl3anc ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → od ⁡ G ⁡ x ∥ B
38 simplr ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → B ∈ ℙ
39 1 20 odcl2 ⊢ G ∈ Grp ∧ B ∈ Fin ∧ x ∈ B → od ⁡ G ⁡ x ∈ ℕ
40 21 35 22 39 syl3anc ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → od ⁡ G ⁡ x ∈ ℕ
41 dvdsprime ⊢ B ∈ ℙ ∧ od ⁡ G ⁡ x ∈ ℕ → od ⁡ G ⁡ x ∥ B ↔ od ⁡ G ⁡ x = B ∨ od ⁡ G ⁡ x = 1
42 38 40 41 syl2anc ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → od ⁡ G ⁡ x ∥ B ↔ od ⁡ G ⁡ x = B ∨ od ⁡ G ⁡ x = 1
43 37 42 mpbid ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → od ⁡ G ⁡ x = B ∨ od ⁡ G ⁡ x = 1
44 43 ord ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → ¬ od ⁡ G ⁡ x = B → od ⁡ G ⁡ x = 1
45 28 44 mt3d ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → od ⁡ G ⁡ x = B
46 1 20 21 22 45 iscygodd ⊢ G ∈ Grp ∧ B ∈ ℙ ∧ x ∈ B ∧ ¬ x ∈ 0 G → G ∈ CycGrp
47 19 46 exlimddv ⊢ G ∈ Grp ∧ B ∈ ℙ → G ∈ CycGrp