Step | Hyp | Ref
| Expression |
1 | | cygctb.1 |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
2 | 1 | grpbn0 17451 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅) |
3 | 2 | adantr 481 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → 𝐵 ≠ ∅) |
4 | | 6re 11101 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
5 | | rexr 10085 |
. . . . . . . 8
⊢ (6 ∈
ℝ → 6 ∈ ℝ*) |
6 | | pnfnlt 11962 |
. . . . . . . 8
⊢ (6 ∈
ℝ* → ¬ +∞ < 6) |
7 | 4, 5, 6 | mp2b 10 |
. . . . . . 7
⊢ ¬
+∞ < 6 |
8 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺)
∈ V |
9 | 1, 8 | eqeltri 2697 |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
10 | 9 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp → 𝐵 ∈ V) |
11 | | hashinf 13122 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin) →
(#‘𝐵) =
+∞) |
12 | 10, 11 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) →
(#‘𝐵) =
+∞) |
13 | 12 | breq1d 4663 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) →
((#‘𝐵) < 6 ↔
+∞ < 6)) |
14 | 13 | biimpd 219 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) →
((#‘𝐵) < 6 →
+∞ < 6)) |
15 | 14 | impancom 456 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → (¬ 𝐵 ∈ Fin → +∞ <
6)) |
16 | 7, 15 | mt3i 141 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → 𝐵 ∈ Fin) |
17 | | hashnncl 13157 |
. . . . . 6
⊢ (𝐵 ∈ Fin →
((#‘𝐵) ∈ ℕ
↔ 𝐵 ≠
∅)) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → ((#‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅)) |
19 | 3, 18 | mpbird 247 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → (#‘𝐵) ∈
ℕ) |
20 | | nnuz 11723 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
21 | 19, 20 | syl6eleq 2711 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → (#‘𝐵) ∈
(ℤ≥‘1)) |
22 | | 6nn 11189 |
. . . . 5
⊢ 6 ∈
ℕ |
23 | 22 | nnzi 11401 |
. . . 4
⊢ 6 ∈
ℤ |
24 | 23 | a1i 11 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → 6 ∈
ℤ) |
25 | | simpr 477 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → (#‘𝐵) < 6) |
26 | | elfzo2 12473 |
. . 3
⊢
((#‘𝐵) ∈
(1..^6) ↔ ((#‘𝐵)
∈ (ℤ≥‘1) ∧ 6 ∈ ℤ ∧
(#‘𝐵) <
6)) |
27 | 21, 24, 25, 26 | syl3anbrc 1246 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → (#‘𝐵) ∈
(1..^6)) |
28 | | df-6 11083 |
. . . . . . 7
⊢ 6 = (5 +
1) |
29 | 28 | oveq2i 6661 |
. . . . . 6
⊢ (1..^6) =
(1..^(5 + 1)) |
30 | 29 | eleq2i 2693 |
. . . . 5
⊢
((#‘𝐵) ∈
(1..^6) ↔ (#‘𝐵)
∈ (1..^(5 + 1))) |
31 | | 5nn 11188 |
. . . . . . 7
⊢ 5 ∈
ℕ |
32 | 31, 20 | eleqtri 2699 |
. . . . . 6
⊢ 5 ∈
(ℤ≥‘1) |
33 | | fzosplitsni 12579 |
. . . . . 6
⊢ (5 ∈
(ℤ≥‘1) → ((#‘𝐵) ∈ (1..^(5 + 1)) ↔
((#‘𝐵) ∈ (1..^5)
∨ (#‘𝐵) =
5))) |
34 | 32, 33 | ax-mp 5 |
. . . . 5
⊢
((#‘𝐵) ∈
(1..^(5 + 1)) ↔ ((#‘𝐵) ∈ (1..^5) ∨ (#‘𝐵) = 5)) |
35 | 30, 34 | bitri 264 |
. . . 4
⊢
((#‘𝐵) ∈
(1..^6) ↔ ((#‘𝐵)
∈ (1..^5) ∨ (#‘𝐵) = 5)) |
36 | | df-5 11082 |
. . . . . . . . 9
⊢ 5 = (4 +
1) |
37 | 36 | oveq2i 6661 |
. . . . . . . 8
⊢ (1..^5) =
(1..^(4 + 1)) |
38 | 37 | eleq2i 2693 |
. . . . . . 7
⊢
((#‘𝐵) ∈
(1..^5) ↔ (#‘𝐵)
∈ (1..^(4 + 1))) |
39 | | 4nn 11187 |
. . . . . . . . 9
⊢ 4 ∈
ℕ |
40 | 39, 20 | eleqtri 2699 |
. . . . . . . 8
⊢ 4 ∈
(ℤ≥‘1) |
41 | | fzosplitsni 12579 |
. . . . . . . 8
⊢ (4 ∈
(ℤ≥‘1) → ((#‘𝐵) ∈ (1..^(4 + 1)) ↔
((#‘𝐵) ∈ (1..^4)
∨ (#‘𝐵) =
4))) |
42 | 40, 41 | ax-mp 5 |
. . . . . . 7
⊢
((#‘𝐵) ∈
(1..^(4 + 1)) ↔ ((#‘𝐵) ∈ (1..^4) ∨ (#‘𝐵) = 4)) |
43 | 38, 42 | bitri 264 |
. . . . . 6
⊢
((#‘𝐵) ∈
(1..^5) ↔ ((#‘𝐵)
∈ (1..^4) ∨ (#‘𝐵) = 4)) |
44 | | df-4 11081 |
. . . . . . . . . . 11
⊢ 4 = (3 +
1) |
45 | 44 | oveq2i 6661 |
. . . . . . . . . 10
⊢ (1..^4) =
(1..^(3 + 1)) |
46 | 45 | eleq2i 2693 |
. . . . . . . . 9
⊢
((#‘𝐵) ∈
(1..^4) ↔ (#‘𝐵)
∈ (1..^(3 + 1))) |
47 | | 3nn 11186 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
48 | 47, 20 | eleqtri 2699 |
. . . . . . . . . 10
⊢ 3 ∈
(ℤ≥‘1) |
49 | | fzosplitsni 12579 |
. . . . . . . . . 10
⊢ (3 ∈
(ℤ≥‘1) → ((#‘𝐵) ∈ (1..^(3 + 1)) ↔
((#‘𝐵) ∈ (1..^3)
∨ (#‘𝐵) =
3))) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . 9
⊢
((#‘𝐵) ∈
(1..^(3 + 1)) ↔ ((#‘𝐵) ∈ (1..^3) ∨ (#‘𝐵) = 3)) |
51 | 46, 50 | bitri 264 |
. . . . . . . 8
⊢
((#‘𝐵) ∈
(1..^4) ↔ ((#‘𝐵)
∈ (1..^3) ∨ (#‘𝐵) = 3)) |
52 | | df-3 11080 |
. . . . . . . . . . . . 13
⊢ 3 = (2 +
1) |
53 | 52 | oveq2i 6661 |
. . . . . . . . . . . 12
⊢ (1..^3) =
(1..^(2 + 1)) |
54 | 53 | eleq2i 2693 |
. . . . . . . . . . 11
⊢
((#‘𝐵) ∈
(1..^3) ↔ (#‘𝐵)
∈ (1..^(2 + 1))) |
55 | | 2eluzge1 11734 |
. . . . . . . . . . . 12
⊢ 2 ∈
(ℤ≥‘1) |
56 | | fzosplitsni 12579 |
. . . . . . . . . . . 12
⊢ (2 ∈
(ℤ≥‘1) → ((#‘𝐵) ∈ (1..^(2 + 1)) ↔
((#‘𝐵) ∈ (1..^2)
∨ (#‘𝐵) =
2))) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((#‘𝐵) ∈
(1..^(2 + 1)) ↔ ((#‘𝐵) ∈ (1..^2) ∨ (#‘𝐵) = 2)) |
58 | 54, 57 | bitri 264 |
. . . . . . . . . 10
⊢
((#‘𝐵) ∈
(1..^3) ↔ ((#‘𝐵)
∈ (1..^2) ∨ (#‘𝐵) = 2)) |
59 | | elsni 4194 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐵) ∈
{1} → (#‘𝐵) =
1) |
60 | | fzo12sn 12551 |
. . . . . . . . . . . . . . . . 17
⊢ (1..^2) =
{1} |
61 | 59, 60 | eleq2s 2719 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐵) ∈
(1..^2) → (#‘𝐵)
= 1) |
62 | 61 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ (1..^2)) →
(#‘𝐵) =
1) |
63 | | hash1 13192 |
. . . . . . . . . . . . . . 15
⊢
(#‘1𝑜) = 1 |
64 | 62, 63 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ (1..^2)) →
(#‘𝐵) =
(#‘1𝑜)) |
65 | | 1nn0 11308 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℕ0 |
66 | 62, 65 | syl6eqel 2709 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ (1..^2)) →
(#‘𝐵) ∈
ℕ0) |
67 | | hashclb 13149 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔
(#‘𝐵) ∈
ℕ0)) |
68 | 9, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ Fin ↔
(#‘𝐵) ∈
ℕ0) |
69 | 66, 68 | sylibr 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ (1..^2)) → 𝐵 ∈ Fin) |
70 | | 1onn 7719 |
. . . . . . . . . . . . . . . 16
⊢
1𝑜 ∈ ω |
71 | | nnfi 8153 |
. . . . . . . . . . . . . . . 16
⊢
(1𝑜 ∈ ω → 1𝑜
∈ Fin) |
72 | 70, 71 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
1𝑜 ∈ Fin |
73 | | hashen 13135 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ Fin ∧
1𝑜 ∈ Fin) → ((#‘𝐵) = (#‘1𝑜) ↔
𝐵 ≈
1𝑜)) |
74 | 69, 72, 73 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ (1..^2)) →
((#‘𝐵) =
(#‘1𝑜) ↔ 𝐵 ≈
1𝑜)) |
75 | 64, 74 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ (1..^2)) → 𝐵 ≈
1𝑜) |
76 | 1 | 0cyg 18294 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1𝑜)
→ 𝐺 ∈
CycGrp) |
77 | | cygabl 18292 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1𝑜)
→ 𝐺 ∈
Abel) |
79 | 75, 78 | syldan 487 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ (1..^2)) → 𝐺 ∈ Abel) |
80 | 79 | ex 450 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp →
((#‘𝐵) ∈ (1..^2)
→ 𝐺 ∈
Abel)) |
81 | | id 22 |
. . . . . . . . . . . . 13
⊢
((#‘𝐵) = 2
→ (#‘𝐵) =
2) |
82 | | 2prm 15405 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℙ |
83 | 81, 82 | syl6eqel 2709 |
. . . . . . . . . . . 12
⊢
((#‘𝐵) = 2
→ (#‘𝐵) ∈
ℙ) |
84 | 1 | prmcyg 18295 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ ℙ) → 𝐺 ∈ CycGrp) |
85 | 84, 77 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ ℙ) → 𝐺 ∈ Abel) |
86 | 85 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ Grp →
((#‘𝐵) ∈ ℙ
→ 𝐺 ∈
Abel)) |
87 | 83, 86 | syl5 34 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp →
((#‘𝐵) = 2 →
𝐺 ∈
Abel)) |
88 | 80, 87 | jaod 395 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp →
(((#‘𝐵) ∈
(1..^2) ∨ (#‘𝐵) =
2) → 𝐺 ∈
Abel)) |
89 | 58, 88 | syl5bi 232 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp →
((#‘𝐵) ∈ (1..^3)
→ 𝐺 ∈
Abel)) |
90 | | id 22 |
. . . . . . . . . . 11
⊢
((#‘𝐵) = 3
→ (#‘𝐵) =
3) |
91 | | 3prm 15406 |
. . . . . . . . . . 11
⊢ 3 ∈
ℙ |
92 | 90, 91 | syl6eqel 2709 |
. . . . . . . . . 10
⊢
((#‘𝐵) = 3
→ (#‘𝐵) ∈
ℙ) |
93 | 92, 86 | syl5 34 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp →
((#‘𝐵) = 3 →
𝐺 ∈
Abel)) |
94 | 89, 93 | jaod 395 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp →
(((#‘𝐵) ∈
(1..^3) ∨ (#‘𝐵) =
3) → 𝐺 ∈
Abel)) |
95 | 51, 94 | syl5bi 232 |
. . . . . . 7
⊢ (𝐺 ∈ Grp →
((#‘𝐵) ∈ (1..^4)
→ 𝐺 ∈
Abel)) |
96 | | simpl 473 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) → 𝐺 ∈ Grp) |
97 | | 2z 11409 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
98 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(gEx‘𝐺) =
(gEx‘𝐺) |
99 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(od‘𝐺) =
(od‘𝐺) |
100 | 1, 98, 99 | gexdvds2 18000 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 2 ∈
ℤ) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2)) |
101 | 96, 97, 100 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2)) |
102 | 1, 98 | gex2abl 18254 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧
(gEx‘𝐺) ∥ 2)
→ 𝐺 ∈
Abel) |
103 | 102 | ex 450 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ Grp →
((gEx‘𝐺) ∥ 2
→ 𝐺 ∈
Abel)) |
104 | 103 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel)) |
105 | 101, 104 | sylbird 250 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) → (∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel)) |
106 | | rexnal 2995 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 ↔ ¬ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2) |
107 | 96 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Grp) |
108 | | simprl 794 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝑥 ∈ 𝐵) |
109 | 1, 99 | odcl 17955 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐵 → ((od‘𝐺)‘𝑥) ∈
ℕ0) |
110 | 109 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈
ℕ0) |
111 | | 4nn0 11311 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℕ0 |
112 | 111 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∈
ℕ0) |
113 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) → (#‘𝐵) = 4) |
114 | 113, 111 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) → (#‘𝐵) ∈
ℕ0) |
115 | 114, 68 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) → 𝐵 ∈ Fin) |
116 | 115 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐵 ∈ Fin) |
117 | 1, 99 | oddvds2 17983 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (#‘𝐵)) |
118 | 107, 116,
108, 117 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ (#‘𝐵)) |
119 | 113 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (#‘𝐵) = 4) |
120 | 118, 119 | breqtrd 4679 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ 4) |
121 | | sq2 12960 |
. . . . . . . . . . . . . . . . 17
⊢
(2↑2) = 4 |
122 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ∈
ℤ) |
123 | | 2nn0 11309 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℕ0 |
124 | 123 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ∈
ℕ0) |
125 | 1, 99 | odcl2 17982 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ) |
126 | 107, 116,
108, 125 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ) |
127 | | pccl 15554 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (2 pCnt
((od‘𝐺)‘𝑥)) ∈
ℕ0) |
128 | 82, 126, 127 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈
ℕ0) |
129 | 128 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ) |
130 | | df-2 11079 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 = (1 +
1) |
131 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ ((od‘𝐺)‘𝑥) ∥ 2) |
132 | | dvdsexp 15049 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((2
∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0 ∧ 1 ∈
(ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥)))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)) |
133 | 132 | 3expia 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((2
∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0) → (1
∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1))) |
134 | 97, 128, 133 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈
(ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1))) |
135 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℤ |
136 | | eluz 11701 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((2 pCnt
((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 1 ∈
ℤ) → (1 ∈ (ℤ≥‘(2 pCnt
((od‘𝐺)‘𝑥))) ↔ (2 pCnt
((od‘𝐺)‘𝑥)) ≤ 1)) |
137 | 129, 135,
136 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈
(ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1)) |
138 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑛 = 2 → (2↑𝑛) = (2↑2)) |
139 | 138, 121 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 = 2 → (2↑𝑛) = 4) |
140 | 139 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = 2 → (((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) ∥ 4)) |
141 | 140 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((2
∈ ℕ0 ∧ ((od‘𝐺)‘𝑥) ∥ 4) → ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛)) |
142 | 123, 120,
141 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ∃𝑛 ∈ ℕ0
((od‘𝐺)‘𝑥) ∥ (2↑𝑛)) |
143 | | pcprmpw2 15586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((2
∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (∃𝑛 ∈ ℕ0
((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥))))) |
144 | 82, 126, 143 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (∃𝑛 ∈ ℕ0
((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥))))) |
145 | 142, 144 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))) |
146 | 145 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑(2 pCnt
((od‘𝐺)‘𝑥))) = ((od‘𝐺)‘𝑥)) |
147 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℂ |
148 | | exp1 12866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (2 ∈
ℂ → (2↑1) = 2) |
149 | 147, 148 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(2↑1) = 2 |
150 | 149 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑1) =
2) |
151 | 146, 150 | breq12d 4666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((2↑(2 pCnt
((od‘𝐺)‘𝑥))) ∥ (2↑1) ↔
((od‘𝐺)‘𝑥) ∥ 2)) |
152 | 134, 137,
151 | 3imtr3d 282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((2 pCnt
((od‘𝐺)‘𝑥)) ≤ 1 →
((od‘𝐺)‘𝑥) ∥ 2)) |
153 | 131, 152 | mtod 189 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ (2 pCnt
((od‘𝐺)‘𝑥)) ≤ 1) |
154 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ |
155 | 128 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ) |
156 | | ltnle 10117 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℝ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ) → (1 < (2 pCnt
((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt
((od‘𝐺)‘𝑥)) ≤ 1)) |
157 | 154, 155,
156 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 < (2 pCnt
((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt
((od‘𝐺)‘𝑥)) ≤ 1)) |
158 | 153, 157 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 1 < (2 pCnt
((od‘𝐺)‘𝑥))) |
159 | | nn0ltp1le 11435 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℕ0 ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0) → (1 <
(2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt
((od‘𝐺)‘𝑥)))) |
160 | 65, 128, 159 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 < (2 pCnt
((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt
((od‘𝐺)‘𝑥)))) |
161 | 158, 160 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 + 1) ≤ (2 pCnt
((od‘𝐺)‘𝑥))) |
162 | 130, 161 | syl5eqbr 4688 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ≤ (2 pCnt
((od‘𝐺)‘𝑥))) |
163 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2 pCnt
((od‘𝐺)‘𝑥)) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (2 pCnt
((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 2 ≤
(2 pCnt ((od‘𝐺)‘𝑥)))) |
164 | 122, 129,
162, 163 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈
(ℤ≥‘2)) |
165 | | dvdsexp 15049 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℤ ∧ 2 ∈ ℕ0 ∧ (2 pCnt
((od‘𝐺)‘𝑥)) ∈
(ℤ≥‘2)) → (2↑2) ∥ (2↑(2 pCnt
((od‘𝐺)‘𝑥)))) |
166 | 122, 124,
164, 165 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑2) ∥
(2↑(2 pCnt ((od‘𝐺)‘𝑥)))) |
167 | 121, 166 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ (2↑(2
pCnt ((od‘𝐺)‘𝑥)))) |
168 | 167, 145 | breqtrrd 4681 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥
((od‘𝐺)‘𝑥)) |
169 | | dvdseq 15036 |
. . . . . . . . . . . . . . 15
⊢
(((((od‘𝐺)‘𝑥) ∈ ℕ0 ∧ 4 ∈
ℕ0) ∧ (((od‘𝐺)‘𝑥) ∥ 4 ∧ 4 ∥ ((od‘𝐺)‘𝑥))) → ((od‘𝐺)‘𝑥) = 4) |
170 | 110, 112,
120, 168, 169 | syl22anc 1327 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = 4) |
171 | 170, 119 | eqtr4d 2659 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (#‘𝐵)) |
172 | 1, 99, 107, 108, 171 | iscygodd 18290 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ CycGrp) |
173 | 172, 77 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Abel) |
174 | 173 | rexlimdvaa 3032 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) → (∃𝑥 ∈ 𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel)) |
175 | 106, 174 | syl5bir 233 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) → (¬
∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel)) |
176 | 105, 175 | pm2.61d 170 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) = 4) → 𝐺 ∈ Abel) |
177 | 176 | ex 450 |
. . . . . . 7
⊢ (𝐺 ∈ Grp →
((#‘𝐵) = 4 →
𝐺 ∈
Abel)) |
178 | 95, 177 | jaod 395 |
. . . . . 6
⊢ (𝐺 ∈ Grp →
(((#‘𝐵) ∈
(1..^4) ∨ (#‘𝐵) =
4) → 𝐺 ∈
Abel)) |
179 | 43, 178 | syl5bi 232 |
. . . . 5
⊢ (𝐺 ∈ Grp →
((#‘𝐵) ∈ (1..^5)
→ 𝐺 ∈
Abel)) |
180 | | id 22 |
. . . . . . 7
⊢
((#‘𝐵) = 5
→ (#‘𝐵) =
5) |
181 | | 5prm 15815 |
. . . . . . 7
⊢ 5 ∈
ℙ |
182 | 180, 181 | syl6eqel 2709 |
. . . . . 6
⊢
((#‘𝐵) = 5
→ (#‘𝐵) ∈
ℙ) |
183 | 182, 86 | syl5 34 |
. . . . 5
⊢ (𝐺 ∈ Grp →
((#‘𝐵) = 5 →
𝐺 ∈
Abel)) |
184 | 179, 183 | jaod 395 |
. . . 4
⊢ (𝐺 ∈ Grp →
(((#‘𝐵) ∈
(1..^5) ∨ (#‘𝐵) =
5) → 𝐺 ∈
Abel)) |
185 | 35, 184 | syl5bi 232 |
. . 3
⊢ (𝐺 ∈ Grp →
((#‘𝐵) ∈ (1..^6)
→ 𝐺 ∈
Abel)) |
186 | 185 | imp 445 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ (1..^6)) → 𝐺 ∈ Abel) |
187 | 27, 186 | syldan 487 |
1
⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → 𝐺 ∈ Abel) |