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 e. Grp /\ ( # ` B ) < 6 ) -> G e. Abel )

Proof

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