# Metamath Proof Explorer

## Theorem lt6abl

Description: A group with fewer than 6 elements is abelian. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypothesis cygctb.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
Assertion lt6abl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to {G}\in \mathrm{Abel}$

### Proof

Step Hyp Ref Expression
1 cygctb.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 1 grpbn0 ${⊢}{G}\in \mathrm{Grp}\to {B}\ne \varnothing$
3 2 adantr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to {B}\ne \varnothing$
4 6re ${⊢}6\in ℝ$
5 rexr ${⊢}6\in ℝ\to 6\in {ℝ}^{*}$
6 pnfnlt ${⊢}6\in {ℝ}^{*}\to ¬\mathrm{+\infty }<6$
7 4 5 6 mp2b ${⊢}¬\mathrm{+\infty }<6$
8 1 fvexi ${⊢}{B}\in \mathrm{V}$
9 8 a1i ${⊢}{G}\in \mathrm{Grp}\to {B}\in \mathrm{V}$
10 hashinf ${⊢}\left({B}\in \mathrm{V}\wedge ¬{B}\in \mathrm{Fin}\right)\to \left|{B}\right|=\mathrm{+\infty }$
11 9 10 sylan ${⊢}\left({G}\in \mathrm{Grp}\wedge ¬{B}\in \mathrm{Fin}\right)\to \left|{B}\right|=\mathrm{+\infty }$
12 11 breq1d ${⊢}\left({G}\in \mathrm{Grp}\wedge ¬{B}\in \mathrm{Fin}\right)\to \left(\left|{B}\right|<6↔\mathrm{+\infty }<6\right)$
13 12 biimpd ${⊢}\left({G}\in \mathrm{Grp}\wedge ¬{B}\in \mathrm{Fin}\right)\to \left(\left|{B}\right|<6\to \mathrm{+\infty }<6\right)$
14 13 impancom ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to \left(¬{B}\in \mathrm{Fin}\to \mathrm{+\infty }<6\right)$
15 7 14 mt3i ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to {B}\in \mathrm{Fin}$
16 hashnncl ${⊢}{B}\in \mathrm{Fin}\to \left(\left|{B}\right|\in ℕ↔{B}\ne \varnothing \right)$
17 15 16 syl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to \left(\left|{B}\right|\in ℕ↔{B}\ne \varnothing \right)$
18 3 17 mpbird ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to \left|{B}\right|\in ℕ$
19 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
20 18 19 eleqtrdi ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to \left|{B}\right|\in {ℤ}_{\ge 1}$
21 6nn ${⊢}6\in ℕ$
22 21 nnzi ${⊢}6\in ℤ$
23 22 a1i ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to 6\in ℤ$
24 simpr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to \left|{B}\right|<6$
25 elfzo2 ${⊢}\left|{B}\right|\in \left(1..^6\right)↔\left(\left|{B}\right|\in {ℤ}_{\ge 1}\wedge 6\in ℤ\wedge \left|{B}\right|<6\right)$
26 20 23 24 25 syl3anbrc ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to \left|{B}\right|\in \left(1..^6\right)$
27 df-6 ${⊢}6=5+1$
28 27 oveq2i ${⊢}\left(1..^6\right)=\left(1..^5+1\right)$
29 28 eleq2i ${⊢}\left|{B}\right|\in \left(1..^6\right)↔\left|{B}\right|\in \left(1..^5+1\right)$
30 5nn ${⊢}5\in ℕ$
31 30 19 eleqtri ${⊢}5\in {ℤ}_{\ge 1}$
32 fzosplitsni ${⊢}5\in {ℤ}_{\ge 1}\to \left(\left|{B}\right|\in \left(1..^5+1\right)↔\left(\left|{B}\right|\in \left(1..^5\right)\vee \left|{B}\right|=5\right)\right)$
33 31 32 ax-mp ${⊢}\left|{B}\right|\in \left(1..^5+1\right)↔\left(\left|{B}\right|\in \left(1..^5\right)\vee \left|{B}\right|=5\right)$
34 29 33 bitri ${⊢}\left|{B}\right|\in \left(1..^6\right)↔\left(\left|{B}\right|\in \left(1..^5\right)\vee \left|{B}\right|=5\right)$
35 df-5 ${⊢}5=4+1$
36 35 oveq2i ${⊢}\left(1..^5\right)=\left(1..^4+1\right)$
37 36 eleq2i ${⊢}\left|{B}\right|\in \left(1..^5\right)↔\left|{B}\right|\in \left(1..^4+1\right)$
38 4nn ${⊢}4\in ℕ$
39 38 19 eleqtri ${⊢}4\in {ℤ}_{\ge 1}$
40 fzosplitsni ${⊢}4\in {ℤ}_{\ge 1}\to \left(\left|{B}\right|\in \left(1..^4+1\right)↔\left(\left|{B}\right|\in \left(1..^4\right)\vee \left|{B}\right|=4\right)\right)$
41 39 40 ax-mp ${⊢}\left|{B}\right|\in \left(1..^4+1\right)↔\left(\left|{B}\right|\in \left(1..^4\right)\vee \left|{B}\right|=4\right)$
42 37 41 bitri ${⊢}\left|{B}\right|\in \left(1..^5\right)↔\left(\left|{B}\right|\in \left(1..^4\right)\vee \left|{B}\right|=4\right)$
43 df-4 ${⊢}4=3+1$
44 43 oveq2i ${⊢}\left(1..^4\right)=\left(1..^3+1\right)$
45 44 eleq2i ${⊢}\left|{B}\right|\in \left(1..^4\right)↔\left|{B}\right|\in \left(1..^3+1\right)$
46 3nn ${⊢}3\in ℕ$
47 46 19 eleqtri ${⊢}3\in {ℤ}_{\ge 1}$
48 fzosplitsni ${⊢}3\in {ℤ}_{\ge 1}\to \left(\left|{B}\right|\in \left(1..^3+1\right)↔\left(\left|{B}\right|\in \left(1..^3\right)\vee \left|{B}\right|=3\right)\right)$
49 47 48 ax-mp ${⊢}\left|{B}\right|\in \left(1..^3+1\right)↔\left(\left|{B}\right|\in \left(1..^3\right)\vee \left|{B}\right|=3\right)$
50 45 49 bitri ${⊢}\left|{B}\right|\in \left(1..^4\right)↔\left(\left|{B}\right|\in \left(1..^3\right)\vee \left|{B}\right|=3\right)$
51 df-3 ${⊢}3=2+1$
52 51 oveq2i ${⊢}\left(1..^3\right)=\left(1..^2+1\right)$
53 52 eleq2i ${⊢}\left|{B}\right|\in \left(1..^3\right)↔\left|{B}\right|\in \left(1..^2+1\right)$
54 2eluzge1 ${⊢}2\in {ℤ}_{\ge 1}$
55 fzosplitsni ${⊢}2\in {ℤ}_{\ge 1}\to \left(\left|{B}\right|\in \left(1..^2+1\right)↔\left(\left|{B}\right|\in \left(1..^2\right)\vee \left|{B}\right|=2\right)\right)$
56 54 55 ax-mp ${⊢}\left|{B}\right|\in \left(1..^2+1\right)↔\left(\left|{B}\right|\in \left(1..^2\right)\vee \left|{B}\right|=2\right)$
57 53 56 bitri ${⊢}\left|{B}\right|\in \left(1..^3\right)↔\left(\left|{B}\right|\in \left(1..^2\right)\vee \left|{B}\right|=2\right)$
58 elsni ${⊢}\left|{B}\right|\in \left\{1\right\}\to \left|{B}\right|=1$
59 fzo12sn ${⊢}\left(1..^2\right)=\left\{1\right\}$
60 58 59 eleq2s ${⊢}\left|{B}\right|\in \left(1..^2\right)\to \left|{B}\right|=1$
61 60 adantl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|\in \left(1..^2\right)\right)\to \left|{B}\right|=1$
62 hash1 ${⊢}\left|{1}_{𝑜}\right|=1$
63 61 62 syl6eqr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|\in \left(1..^2\right)\right)\to \left|{B}\right|=\left|{1}_{𝑜}\right|$
64 1nn0 ${⊢}1\in {ℕ}_{0}$
65 61 64 syl6eqel ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|\in \left(1..^2\right)\right)\to \left|{B}\right|\in {ℕ}_{0}$
66 hashclb ${⊢}{B}\in \mathrm{V}\to \left({B}\in \mathrm{Fin}↔\left|{B}\right|\in {ℕ}_{0}\right)$
67 8 66 ax-mp ${⊢}{B}\in \mathrm{Fin}↔\left|{B}\right|\in {ℕ}_{0}$
68 65 67 sylibr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|\in \left(1..^2\right)\right)\to {B}\in \mathrm{Fin}$
69 1onn ${⊢}{1}_{𝑜}\in \mathrm{\omega }$
70 nnfi ${⊢}{1}_{𝑜}\in \mathrm{\omega }\to {1}_{𝑜}\in \mathrm{Fin}$
71 69 70 ax-mp ${⊢}{1}_{𝑜}\in \mathrm{Fin}$
72 hashen ${⊢}\left({B}\in \mathrm{Fin}\wedge {1}_{𝑜}\in \mathrm{Fin}\right)\to \left(\left|{B}\right|=\left|{1}_{𝑜}\right|↔{B}\approx {1}_{𝑜}\right)$
73 68 71 72 sylancl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|\in \left(1..^2\right)\right)\to \left(\left|{B}\right|=\left|{1}_{𝑜}\right|↔{B}\approx {1}_{𝑜}\right)$
74 63 73 mpbid ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|\in \left(1..^2\right)\right)\to {B}\approx {1}_{𝑜}$
75 1 0cyg ${⊢}\left({G}\in \mathrm{Grp}\wedge {B}\approx {1}_{𝑜}\right)\to {G}\in \mathrm{CycGrp}$
76 cygabl ${⊢}{G}\in \mathrm{CycGrp}\to {G}\in \mathrm{Abel}$
77 75 76 syl ${⊢}\left({G}\in \mathrm{Grp}\wedge {B}\approx {1}_{𝑜}\right)\to {G}\in \mathrm{Abel}$
78 74 77 syldan ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|\in \left(1..^2\right)\right)\to {G}\in \mathrm{Abel}$
79 78 ex ${⊢}{G}\in \mathrm{Grp}\to \left(\left|{B}\right|\in \left(1..^2\right)\to {G}\in \mathrm{Abel}\right)$
80 id ${⊢}\left|{B}\right|=2\to \left|{B}\right|=2$
81 2prm ${⊢}2\in ℙ$
82 80 81 syl6eqel ${⊢}\left|{B}\right|=2\to \left|{B}\right|\in ℙ$
83 1 prmcyg ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|\in ℙ\right)\to {G}\in \mathrm{CycGrp}$
84 83 76 syl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|\in ℙ\right)\to {G}\in \mathrm{Abel}$
85 84 ex ${⊢}{G}\in \mathrm{Grp}\to \left(\left|{B}\right|\in ℙ\to {G}\in \mathrm{Abel}\right)$
86 82 85 syl5 ${⊢}{G}\in \mathrm{Grp}\to \left(\left|{B}\right|=2\to {G}\in \mathrm{Abel}\right)$
87 79 86 jaod ${⊢}{G}\in \mathrm{Grp}\to \left(\left(\left|{B}\right|\in \left(1..^2\right)\vee \left|{B}\right|=2\right)\to {G}\in \mathrm{Abel}\right)$
88 57 87 syl5bi ${⊢}{G}\in \mathrm{Grp}\to \left(\left|{B}\right|\in \left(1..^3\right)\to {G}\in \mathrm{Abel}\right)$
89 id ${⊢}\left|{B}\right|=3\to \left|{B}\right|=3$
90 3prm ${⊢}3\in ℙ$
91 89 90 syl6eqel ${⊢}\left|{B}\right|=3\to \left|{B}\right|\in ℙ$
92 91 85 syl5 ${⊢}{G}\in \mathrm{Grp}\to \left(\left|{B}\right|=3\to {G}\in \mathrm{Abel}\right)$
93 88 92 jaod ${⊢}{G}\in \mathrm{Grp}\to \left(\left(\left|{B}\right|\in \left(1..^3\right)\vee \left|{B}\right|=3\right)\to {G}\in \mathrm{Abel}\right)$
94 50 93 syl5bi ${⊢}{G}\in \mathrm{Grp}\to \left(\left|{B}\right|\in \left(1..^4\right)\to {G}\in \mathrm{Abel}\right)$
95 simpl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\to {G}\in \mathrm{Grp}$
96 2z ${⊢}2\in ℤ$
97 eqid ${⊢}\mathrm{gEx}\left({G}\right)=\mathrm{gEx}\left({G}\right)$
98 eqid ${⊢}\mathrm{od}\left({G}\right)=\mathrm{od}\left({G}\right)$
99 1 97 98 gexdvds2 ${⊢}\left({G}\in \mathrm{Grp}\wedge 2\in ℤ\right)\to \left(\mathrm{gEx}\left({G}\right)\parallel 2↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)$
100 95 96 99 sylancl ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\to \left(\mathrm{gEx}\left({G}\right)\parallel 2↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)$
101 1 97 gex2abl ${⊢}\left({G}\in \mathrm{Grp}\wedge \mathrm{gEx}\left({G}\right)\parallel 2\right)\to {G}\in \mathrm{Abel}$
102 101 ex ${⊢}{G}\in \mathrm{Grp}\to \left(\mathrm{gEx}\left({G}\right)\parallel 2\to {G}\in \mathrm{Abel}\right)$
103 102 adantr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\to \left(\mathrm{gEx}\left({G}\right)\parallel 2\to {G}\in \mathrm{Abel}\right)$
104 100 103 sylbird ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\to {G}\in \mathrm{Abel}\right)$
105 rexnal ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2↔¬\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2$
106 95 adantr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to {G}\in \mathrm{Grp}$
107 simprl ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to {x}\in {B}$
108 1 98 odcl ${⊢}{x}\in {B}\to \mathrm{od}\left({G}\right)\left({x}\right)\in {ℕ}_{0}$
109 108 ad2antrl ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\in {ℕ}_{0}$
110 4nn0 ${⊢}4\in {ℕ}_{0}$
111 110 a1i ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 4\in {ℕ}_{0}$
112 simpr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\to \left|{B}\right|=4$
113 112 110 syl6eqel ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\to \left|{B}\right|\in {ℕ}_{0}$
114 113 67 sylibr ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\to {B}\in \mathrm{Fin}$
115 114 adantr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to {B}\in \mathrm{Fin}$
116 1 98 oddvds2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {B}\in \mathrm{Fin}\wedge {x}\in {B}\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\parallel \left|{B}\right|$
117 106 115 107 116 syl3anc ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\parallel \left|{B}\right|$
118 112 adantr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \left|{B}\right|=4$
119 117 118 breqtrd ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\parallel 4$
120 sq2 ${⊢}{2}^{2}=4$
121 2nn0 ${⊢}2\in {ℕ}_{0}$
122 96 a1i ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 2\in ℤ$
123 1 98 odcl2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {B}\in \mathrm{Fin}\wedge {x}\in {B}\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\in ℕ$
124 106 115 107 123 syl3anc ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \mathrm{od}\left({G}\right)\left({x}\right)\in ℕ$
125 pccl ${⊢}\left(2\in ℙ\wedge \mathrm{od}\left({G}\right)\left({x}\right)\in ℕ\right)\to 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in {ℕ}_{0}$
126 81 124 125 sylancr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in {ℕ}_{0}$
127 126 nn0zd ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in ℤ$
128 df-2 ${⊢}2=1+1$
129 simprr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2$
130 dvdsexp ${⊢}\left(2\in ℤ\wedge 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in {ℕ}_{0}\wedge 1\in {ℤ}_{\ge \left(2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\right)}\right)\to {2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}\parallel {2}^{1}$
131 130 3expia ${⊢}\left(2\in ℤ\wedge 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in {ℕ}_{0}\right)\to \left(1\in {ℤ}_{\ge \left(2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\right)}\to {2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}\parallel {2}^{1}\right)$
132 96 126 131 sylancr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \left(1\in {ℤ}_{\ge \left(2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\right)}\to {2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}\parallel {2}^{1}\right)$
133 1z ${⊢}1\in ℤ$
134 eluz ${⊢}\left(2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in ℤ\wedge 1\in ℤ\right)\to \left(1\in {ℤ}_{\ge \left(2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\right)}↔2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\le 1\right)$
135 127 133 134 sylancl ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \left(1\in {ℤ}_{\ge \left(2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\right)}↔2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\le 1\right)$
136 oveq2 ${⊢}{n}=2\to {2}^{{n}}={2}^{2}$
137 136 120 syl6eq ${⊢}{n}=2\to {2}^{{n}}=4$
138 137 breq2d ${⊢}{n}=2\to \left(\mathrm{od}\left({G}\right)\left({x}\right)\parallel {2}^{{n}}↔\mathrm{od}\left({G}\right)\left({x}\right)\parallel 4\right)$
139 138 rspcev ${⊢}\left(2\in {ℕ}_{0}\wedge \mathrm{od}\left({G}\right)\left({x}\right)\parallel 4\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\parallel {2}^{{n}}$
140 121 119 139 sylancr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\parallel {2}^{{n}}$
141 pcprmpw2 ${⊢}\left(2\in ℙ\wedge \mathrm{od}\left({G}\right)\left({x}\right)\in ℕ\right)\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\parallel {2}^{{n}}↔\mathrm{od}\left({G}\right)\left({x}\right)={2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}\right)$
142 81 124 141 sylancr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\parallel {2}^{{n}}↔\mathrm{od}\left({G}\right)\left({x}\right)={2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}\right)$
143 140 142 mpbid ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \mathrm{od}\left({G}\right)\left({x}\right)={2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}$
144 143 eqcomd ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to {2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}=\mathrm{od}\left({G}\right)\left({x}\right)$
145 2cn ${⊢}2\in ℂ$
146 exp1 ${⊢}2\in ℂ\to {2}^{1}=2$
147 145 146 ax-mp ${⊢}{2}^{1}=2$
148 147 a1i ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to {2}^{1}=2$
149 144 148 breq12d ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \left({2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}\parallel {2}^{1}↔\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)$
150 132 135 149 3imtr3d ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \left(2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\le 1\to \mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)$
151 129 150 mtod ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to ¬2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\le 1$
152 1re ${⊢}1\in ℝ$
153 126 nn0red ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in ℝ$
154 ltnle ${⊢}\left(1\in ℝ\wedge 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in ℝ\right)\to \left(1<2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)↔¬2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\le 1\right)$
155 152 153 154 sylancr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \left(1<2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)↔¬2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\le 1\right)$
156 151 155 mpbird ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 1<2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)$
157 nn0ltp1le ${⊢}\left(1\in {ℕ}_{0}\wedge 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in {ℕ}_{0}\right)\to \left(1<2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)↔1+1\le 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\right)$
158 64 126 157 sylancr ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \left(1<2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)↔1+1\le 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\right)$
159 156 158 mpbid ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 1+1\le 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)$
160 128 159 eqbrtrid ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 2\le 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)$
161 eluz2 ${⊢}2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in {ℤ}_{\ge 2}↔\left(2\in ℤ\wedge 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in ℤ\wedge 2\le 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\right)$
162 122 127 160 161 syl3anbrc ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in {ℤ}_{\ge 2}$
163 dvdsexp ${⊢}\left(2\in ℤ\wedge 2\in {ℕ}_{0}\wedge 2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)\in {ℤ}_{\ge 2}\right)\to {2}^{2}\parallel {2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}$
164 96 121 162 163 mp3an12i ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to {2}^{2}\parallel {2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}$
165 120 164 eqbrtrrid ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 4\parallel {2}^{2\mathrm{pCnt}\mathrm{od}\left({G}\right)\left({x}\right)}$
166 165 143 breqtrrd ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to 4\parallel \mathrm{od}\left({G}\right)\left({x}\right)$
167 dvdseq ${⊢}\left(\left(\mathrm{od}\left({G}\right)\left({x}\right)\in {ℕ}_{0}\wedge 4\in {ℕ}_{0}\right)\wedge \left(\mathrm{od}\left({G}\right)\left({x}\right)\parallel 4\wedge 4\parallel \mathrm{od}\left({G}\right)\left({x}\right)\right)\right)\to \mathrm{od}\left({G}\right)\left({x}\right)=4$
168 109 111 119 166 167 syl22anc ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \mathrm{od}\left({G}\right)\left({x}\right)=4$
169 168 118 eqtr4d ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to \mathrm{od}\left({G}\right)\left({x}\right)=\left|{B}\right|$
170 1 98 106 107 169 iscygodd ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to {G}\in \mathrm{CycGrp}$
171 170 76 syl ${⊢}\left(\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\wedge \left({x}\in {B}\wedge ¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\right)\right)\to {G}\in \mathrm{Abel}$
172 171 rexlimdvaa ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}¬\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\to {G}\in \mathrm{Abel}\right)$
173 105 172 syl5bir ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\to \left(¬\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)\parallel 2\to {G}\in \mathrm{Abel}\right)$
174 104 173 pm2.61d ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|=4\right)\to {G}\in \mathrm{Abel}$
175 174 ex ${⊢}{G}\in \mathrm{Grp}\to \left(\left|{B}\right|=4\to {G}\in \mathrm{Abel}\right)$
176 94 175 jaod ${⊢}{G}\in \mathrm{Grp}\to \left(\left(\left|{B}\right|\in \left(1..^4\right)\vee \left|{B}\right|=4\right)\to {G}\in \mathrm{Abel}\right)$
177 42 176 syl5bi ${⊢}{G}\in \mathrm{Grp}\to \left(\left|{B}\right|\in \left(1..^5\right)\to {G}\in \mathrm{Abel}\right)$
178 id ${⊢}\left|{B}\right|=5\to \left|{B}\right|=5$
179 5prm ${⊢}5\in ℙ$
180 178 179 syl6eqel ${⊢}\left|{B}\right|=5\to \left|{B}\right|\in ℙ$
181 180 85 syl5 ${⊢}{G}\in \mathrm{Grp}\to \left(\left|{B}\right|=5\to {G}\in \mathrm{Abel}\right)$
182 177 181 jaod ${⊢}{G}\in \mathrm{Grp}\to \left(\left(\left|{B}\right|\in \left(1..^5\right)\vee \left|{B}\right|=5\right)\to {G}\in \mathrm{Abel}\right)$
183 34 182 syl5bi ${⊢}{G}\in \mathrm{Grp}\to \left(\left|{B}\right|\in \left(1..^6\right)\to {G}\in \mathrm{Abel}\right)$
184 183 imp ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|\in \left(1..^6\right)\right)\to {G}\in \mathrm{Abel}$
185 26 184 syldan ${⊢}\left({G}\in \mathrm{Grp}\wedge \left|{B}\right|<6\right)\to {G}\in \mathrm{Abel}$