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 = Base G
Assertion lt6abl ⊢ G ∈ Grp ∧ B < 6 → G ∈ Abel

Proof

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