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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion lt6abl ( ( 𝐺 ∈ Grp ∧ ( ♯ ‘ 𝐵 ) < 6 ) → 𝐺 ∈ Abel )

Proof

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