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