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 syl6eqr G Grp B 1 ..^ 2 B = 1 𝑜
64 1nn0 1 0
65 61 64 syl6eqel 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 syl6eqel 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 syl5bi G Grp B 1 ..^ 3 G Abel
89 id B = 3 B = 3
90 3prm 3
91 89 90 syl6eqel 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 syl5bi 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 syl6eqel 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 syl6eq 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 syl5bir 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 syl5bi G Grp B 1 ..^ 5 G Abel
178 id B = 5 B = 5
179 5prm 5
180 178 179 syl6eqel 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 syl5bi 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