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

Proof

Step Hyp Ref Expression
1 cygctb.1 ⊢B=BaseG
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∈Bod⁡G⁡x∥2
100 95 96 99 sylancl ⊢G∈Grp∧B=4→gEx⁡G∥2↔∀x∈Bod⁡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∈Bod⁡G⁡x∥2→G∈Abel
105 rexnal ⊢∃x∈B¬od⁡G⁡x∥2↔¬∀x∈Bod⁡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 ⊢22=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∈ℕ→2pCntod⁡G⁡x∈ℕ0
126 81 124 125 sylancr ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→2pCntod⁡G⁡x∈ℕ0
127 126 nn0zd ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→2pCntod⁡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∈ℤ∧2pCntod⁡G⁡x∈ℕ0∧1∈ℤ≥2pCntod⁡G⁡x→22pCntod⁡G⁡x∥21
131 130 3expia ⊢2∈ℤ∧2pCntod⁡G⁡x∈ℕ0→1∈ℤ≥2pCntod⁡G⁡x→22pCntod⁡G⁡x∥21
132 96 126 131 sylancr ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→1∈ℤ≥2pCntod⁡G⁡x→22pCntod⁡G⁡x∥21
133 1z ⊢1∈ℤ
134 eluz ⊢2pCntod⁡G⁡x∈ℤ∧1∈ℤ→1∈ℤ≥2pCntod⁡G⁡x↔2pCntod⁡G⁡x≤1
135 127 133 134 sylancl ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→1∈ℤ≥2pCntod⁡G⁡x↔2pCntod⁡G⁡x≤1
136 oveq2 ⊢n=2→2n=22
137 136 120 eqtrdi ⊢n=2→2n=4
138 137 breq2d ⊢n=2→od⁡G⁡x∥2n↔od⁡G⁡x∥4
139 138 rspcev ⊢2∈ℕ0∧od⁡G⁡x∥4→∃n∈ℕ0od⁡G⁡x∥2n
140 121 119 139 sylancr ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→∃n∈ℕ0od⁡G⁡x∥2n
141 pcprmpw2 ⊢2∈ℙ∧od⁡G⁡x∈ℕ→∃n∈ℕ0od⁡G⁡x∥2n↔od⁡G⁡x=22pCntod⁡G⁡x
142 81 124 141 sylancr ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→∃n∈ℕ0od⁡G⁡x∥2n↔od⁡G⁡x=22pCntod⁡G⁡x
143 140 142 mpbid ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→od⁡G⁡x=22pCntod⁡G⁡x
144 143 eqcomd ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→22pCntod⁡G⁡x=od⁡G⁡x
145 2cn ⊢2∈ℂ
146 exp1 ⊢2∈ℂ→21=2
147 145 146 ax-mp ⊢21=2
148 147 a1i ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→21=2
149 144 148 breq12d ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→22pCntod⁡G⁡x∥21↔od⁡G⁡x∥2
150 132 135 149 3imtr3d ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→2pCntod⁡G⁡x≤1→od⁡G⁡x∥2
151 129 150 mtod ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→¬2pCntod⁡G⁡x≤1
152 1re ⊢1∈ℝ
153 126 nn0red ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→2pCntod⁡G⁡x∈ℝ
154 ltnle ⊢1∈ℝ∧2pCntod⁡G⁡x∈ℝ→1<2pCntod⁡G⁡x↔¬2pCntod⁡G⁡x≤1
155 152 153 154 sylancr ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→1<2pCntod⁡G⁡x↔¬2pCntod⁡G⁡x≤1
156 151 155 mpbird ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→1<2pCntod⁡G⁡x
157 nn0ltp1le ⊢1∈ℕ0∧2pCntod⁡G⁡x∈ℕ0→1<2pCntod⁡G⁡x↔1+1≤2pCntod⁡G⁡x
158 64 126 157 sylancr ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→1<2pCntod⁡G⁡x↔1+1≤2pCntod⁡G⁡x
159 156 158 mpbid ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→1+1≤2pCntod⁡G⁡x
160 128 159 eqbrtrid ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→2≤2pCntod⁡G⁡x
161 eluz2 ⊢2pCntod⁡G⁡x∈ℤ≥2↔2∈ℤ∧2pCntod⁡G⁡x∈ℤ∧2≤2pCntod⁡G⁡x
162 122 127 160 161 syl3anbrc ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→2pCntod⁡G⁡x∈ℤ≥2
163 dvdsexp ⊢2∈ℤ∧2∈ℕ0∧2pCntod⁡G⁡x∈ℤ≥2→22∥22pCntod⁡G⁡x
164 96 121 162 163 mp3an12i ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→22∥22pCntod⁡G⁡x
165 120 164 eqbrtrrid ⊢G∈Grp∧B=4∧x∈B∧¬od⁡G⁡x∥2→4∥22pCntod⁡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∈Bod⁡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