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=BaseG
Assertion prmcyg ⊢G∈Grp∧B∈ℙ→G∈CycGrp

Proof

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