MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lt6abl Structured version   Visualization version   GIF version

Theorem lt6abl 19757
Description: A group with fewer than 6 elements is abelian. (Contributed by Mario Carneiro, 27-Apr-2016.)
Hypothesis
Ref Expression
cygctb.1 𝐵 = (Base‘𝐺)
Assertion
Ref Expression
lt6abl ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐺 ∈ Abel)

Proof of Theorem lt6abl
Dummy variables 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cygctb.1 . . . . . . 7 𝐵 = (Base‘𝐺)
21grpbn0 18847 . . . . . 6 (𝐺 ∈ Grp → 𝐵 ≠ ∅)
32adantr 481 . . . . 5 ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ≠ ∅)
4 6re 12298 . . . . . . . 8 6 ∈ ℝ
5 rexr 11256 . . . . . . . 8 (6 ∈ ℝ → 6 ∈ ℝ*)
6 pnfnlt 13104 . . . . . . . 8 (6 ∈ ℝ* → ¬ +∞ < 6)
74, 5, 6mp2b 10 . . . . . . 7 ¬ +∞ < 6
81fvexi 6902 . . . . . . . . . . . 12 𝐵 ∈ V
98a1i 11 . . . . . . . . . . 11 (𝐺 ∈ Grp → 𝐵 ∈ V)
10 hashinf 14291 . . . . . . . . . . 11 ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
119, 10sylan 580 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
1211breq1d 5157 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 ↔ +∞ < 6))
1312biimpd 228 . . . . . . . 8 ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 → +∞ < 6))
1413impancom 452 . . . . . . 7 ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (¬ 𝐵 ∈ Fin → +∞ < 6))
157, 14mt3i 149 . . . . . 6 ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ∈ Fin)
16 hashnncl 14322 . . . . . 6 (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
1715, 16syl 17 . . . . 5 ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
183, 17mpbird 256 . . . 4 ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ ℕ)
19 nnuz 12861 . . . 4 ℕ = (ℤ‘1)
2018, 19eleqtrdi 2843 . . 3 ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (ℤ‘1))
21 6nn 12297 . . . . 5 6 ∈ ℕ
2221nnzi 12582 . . . 4 6 ∈ ℤ
2322a1i 11 . . 3 ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 6 ∈ ℤ)
24 simpr 485 . . 3 ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) < 6)
25 elfzo2 13631 . . 3 ((♯‘𝐵) ∈ (1..^6) ↔ ((♯‘𝐵) ∈ (ℤ‘1) ∧ 6 ∈ ℤ ∧ (♯‘𝐵) < 6))
2620, 23, 24, 25syl3anbrc 1343 . 2 ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (1..^6))
27 df-6 12275 . . . . . . 7 6 = (5 + 1)
2827oveq2i 7416 . . . . . 6 (1..^6) = (1..^(5 + 1))
2928eleq2i 2825 . . . . 5 ((♯‘𝐵) ∈ (1..^6) ↔ (♯‘𝐵) ∈ (1..^(5 + 1)))
30 5nn 12294 . . . . . . 7 5 ∈ ℕ
3130, 19eleqtri 2831 . . . . . 6 5 ∈ (ℤ‘1)
32 fzosplitsni 13739 . . . . . 6 (5 ∈ (ℤ‘1) → ((♯‘𝐵) ∈ (1..^(5 + 1)) ↔ ((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5)))
3331, 32ax-mp 5 . . . . 5 ((♯‘𝐵) ∈ (1..^(5 + 1)) ↔ ((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5))
3429, 33bitri 274 . . . 4 ((♯‘𝐵) ∈ (1..^6) ↔ ((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5))
35 df-5 12274 . . . . . . . . 9 5 = (4 + 1)
3635oveq2i 7416 . . . . . . . 8 (1..^5) = (1..^(4 + 1))
3736eleq2i 2825 . . . . . . 7 ((♯‘𝐵) ∈ (1..^5) ↔ (♯‘𝐵) ∈ (1..^(4 + 1)))
38 4nn 12291 . . . . . . . . 9 4 ∈ ℕ
3938, 19eleqtri 2831 . . . . . . . 8 4 ∈ (ℤ‘1)
40 fzosplitsni 13739 . . . . . . . 8 (4 ∈ (ℤ‘1) → ((♯‘𝐵) ∈ (1..^(4 + 1)) ↔ ((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4)))
4139, 40ax-mp 5 . . . . . . 7 ((♯‘𝐵) ∈ (1..^(4 + 1)) ↔ ((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4))
4237, 41bitri 274 . . . . . 6 ((♯‘𝐵) ∈ (1..^5) ↔ ((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4))
43 df-4 12273 . . . . . . . . . . 11 4 = (3 + 1)
4443oveq2i 7416 . . . . . . . . . 10 (1..^4) = (1..^(3 + 1))
4544eleq2i 2825 . . . . . . . . 9 ((♯‘𝐵) ∈ (1..^4) ↔ (♯‘𝐵) ∈ (1..^(3 + 1)))
46 3nn 12287 . . . . . . . . . . 11 3 ∈ ℕ
4746, 19eleqtri 2831 . . . . . . . . . 10 3 ∈ (ℤ‘1)
48 fzosplitsni 13739 . . . . . . . . . 10 (3 ∈ (ℤ‘1) → ((♯‘𝐵) ∈ (1..^(3 + 1)) ↔ ((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3)))
4947, 48ax-mp 5 . . . . . . . . 9 ((♯‘𝐵) ∈ (1..^(3 + 1)) ↔ ((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3))
5045, 49bitri 274 . . . . . . . 8 ((♯‘𝐵) ∈ (1..^4) ↔ ((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3))
51 df-3 12272 . . . . . . . . . . . . 13 3 = (2 + 1)
5251oveq2i 7416 . . . . . . . . . . . 12 (1..^3) = (1..^(2 + 1))
5352eleq2i 2825 . . . . . . . . . . 11 ((♯‘𝐵) ∈ (1..^3) ↔ (♯‘𝐵) ∈ (1..^(2 + 1)))
54 2eluzge1 12874 . . . . . . . . . . . 12 2 ∈ (ℤ‘1)
55 fzosplitsni 13739 . . . . . . . . . . . 12 (2 ∈ (ℤ‘1) → ((♯‘𝐵) ∈ (1..^(2 + 1)) ↔ ((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2)))
5654, 55ax-mp 5 . . . . . . . . . . 11 ((♯‘𝐵) ∈ (1..^(2 + 1)) ↔ ((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2))
5753, 56bitri 274 . . . . . . . . . 10 ((♯‘𝐵) ∈ (1..^3) ↔ ((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2))
58 elsni 4644 . . . . . . . . . . . . . . . . 17 ((♯‘𝐵) ∈ {1} → (♯‘𝐵) = 1)
59 fzo12sn 13711 . . . . . . . . . . . . . . . . 17 (1..^2) = {1}
6058, 59eleq2s 2851 . . . . . . . . . . . . . . . 16 ((♯‘𝐵) ∈ (1..^2) → (♯‘𝐵) = 1)
6160adantl 482 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = 1)
62 hash1 14360 . . . . . . . . . . . . . . 15 (♯‘1o) = 1
6361, 62eqtr4di 2790 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = (♯‘1o))
64 1nn0 12484 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ0
6561, 64eqeltrdi 2841 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) ∈ ℕ0)
66 hashclb 14314 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0))
678, 66ax-mp 5 . . . . . . . . . . . . . . . 16 (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0)
6865, 67sylibr 233 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ∈ Fin)
69 1onn 8635 . . . . . . . . . . . . . . . 16 1o ∈ ω
70 nnfi 9163 . . . . . . . . . . . . . . . 16 (1o ∈ ω → 1o ∈ Fin)
7169, 70ax-mp 5 . . . . . . . . . . . . . . 15 1o ∈ Fin
72 hashen 14303 . . . . . . . . . . . . . . 15 ((𝐵 ∈ Fin ∧ 1o ∈ Fin) → ((♯‘𝐵) = (♯‘1o) ↔ 𝐵 ≈ 1o))
7368, 71, 72sylancl 586 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → ((♯‘𝐵) = (♯‘1o) ↔ 𝐵 ≈ 1o))
7463, 73mpbid 231 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ≈ 1o)
7510cyg 19755 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1o) → 𝐺 ∈ CycGrp)
76 cygabl 19753 . . . . . . . . . . . . . 14 (𝐺 ∈ CycGrp → 𝐺 ∈ Abel)
7775, 76syl 17 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1o) → 𝐺 ∈ Abel)
7874, 77syldan 591 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐺 ∈ Abel)
7978ex 413 . . . . . . . . . . 11 (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^2) → 𝐺 ∈ Abel))
80 id 22 . . . . . . . . . . . . 13 ((♯‘𝐵) = 2 → (♯‘𝐵) = 2)
81 2prm 16625 . . . . . . . . . . . . 13 2 ∈ ℙ
8280, 81eqeltrdi 2841 . . . . . . . . . . . 12 ((♯‘𝐵) = 2 → (♯‘𝐵) ∈ ℙ)
831prmcyg 19756 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ CycGrp)
8483, 76syl 17 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ Abel)
8584ex 413 . . . . . . . . . . . 12 (𝐺 ∈ Grp → ((♯‘𝐵) ∈ ℙ → 𝐺 ∈ Abel))
8682, 85syl5 34 . . . . . . . . . . 11 (𝐺 ∈ Grp → ((♯‘𝐵) = 2 → 𝐺 ∈ Abel))
8779, 86jaod 857 . . . . . . . . . 10 (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2) → 𝐺 ∈ Abel))
8857, 87biimtrid 241 . . . . . . . . 9 (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^3) → 𝐺 ∈ Abel))
89 id 22 . . . . . . . . . . 11 ((♯‘𝐵) = 3 → (♯‘𝐵) = 3)
90 3prm 16627 . . . . . . . . . . 11 3 ∈ ℙ
9189, 90eqeltrdi 2841 . . . . . . . . . 10 ((♯‘𝐵) = 3 → (♯‘𝐵) ∈ ℙ)
9291, 85syl5 34 . . . . . . . . 9 (𝐺 ∈ Grp → ((♯‘𝐵) = 3 → 𝐺 ∈ Abel))
9388, 92jaod 857 . . . . . . . 8 (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3) → 𝐺 ∈ Abel))
9450, 93biimtrid 241 . . . . . . 7 (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^4) → 𝐺 ∈ Abel))
95 simpl 483 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Grp)
96 2z 12590 . . . . . . . . . . 11 2 ∈ ℤ
97 eqid 2732 . . . . . . . . . . . 12 (gEx‘𝐺) = (gEx‘𝐺)
98 eqid 2732 . . . . . . . . . . . 12 (od‘𝐺) = (od‘𝐺)
991, 97, 98gexdvds2 19447 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 2 ∈ ℤ) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
10095, 96, 99sylancl 586 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
1011, 97gex2abl 19713 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ (gEx‘𝐺) ∥ 2) → 𝐺 ∈ Abel)
102101ex 413 . . . . . . . . . . 11 (𝐺 ∈ Grp → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
103102adantr 481 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
104100, 103sylbird 259 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∀𝑥𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
105 rexnal 3100 . . . . . . . . . 10 (∃𝑥𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 ↔ ¬ ∀𝑥𝐵 ((od‘𝐺)‘𝑥) ∥ 2)
10695adantr 481 . . . . . . . . . . . . 13 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Grp)
107 simprl 769 . . . . . . . . . . . . 13 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝑥𝐵)
1081, 98odcl 19398 . . . . . . . . . . . . . . . 16 (𝑥𝐵 → ((od‘𝐺)‘𝑥) ∈ ℕ0)
109108ad2antrl 726 . . . . . . . . . . . . . . 15 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
110 4nn0 12487 . . . . . . . . . . . . . . . 16 4 ∈ ℕ0
111110a1i 11 . . . . . . . . . . . . . . 15 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∈ ℕ0)
112 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) = 4)
113112, 110eqeltrdi 2841 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) ∈ ℕ0)
114113, 67sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐵 ∈ Fin)
115114adantr 481 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐵 ∈ Fin)
1161, 98oddvds2 19428 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
117106, 115, 107, 116syl3anc 1371 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
118112adantr 481 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (♯‘𝐵) = 4)
119117, 118breqtrd 5173 . . . . . . . . . . . . . . 15 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ 4)
120 sq2 14157 . . . . . . . . . . . . . . . . 17 (2↑2) = 4
121 2nn0 12485 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ0
12296a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ∈ ℤ)
1231, 98odcl2 19427 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ)
124106, 115, 107, 123syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ)
125 pccl 16778 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0)
12681, 124, 125sylancr 587 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0)
127126nn0zd 12580 . . . . . . . . . . . . . . . . . . 19 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ)
128 df-2 12271 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
129 simprr 771 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ ((od‘𝐺)‘𝑥) ∥ 2)
130 dvdsexp 16267 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0 ∧ 1 ∈ (ℤ‘(2 pCnt ((od‘𝐺)‘𝑥)))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1))
1311303expia 1121 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0) → (1 ∈ (ℤ‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
13296, 126, 131sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
133 1z 12588 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ ℤ
134 eluz 12832 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 1 ∈ ℤ) → (1 ∈ (ℤ‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
135127, 133, 134sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
136 oveq2 7413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑛 = 2 → (2↑𝑛) = (2↑2))
137136, 120eqtrdi 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑛 = 2 → (2↑𝑛) = 4)
138137breq2d 5159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 2 → (((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) ∥ 4))
139138rspcev 3612 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2 ∈ ℕ0 ∧ ((od‘𝐺)‘𝑥) ∥ 4) → ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
140121, 119, 139sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
141 pcprmpw2 16811 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))))
14281, 124, 141sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))))
143140, 142mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
144143eqcomd 2738 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) = ((od‘𝐺)‘𝑥))
145 2cn 12283 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 ∈ ℂ
146 exp1 14029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (2 ∈ ℂ → (2↑1) = 2)
147145, 146ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (2↑1) = 2
148147a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑1) = 2)
149144, 148breq12d 5160 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1) ↔ ((od‘𝐺)‘𝑥) ∥ 2))
150132, 135, 1493imtr3d 292 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1 → ((od‘𝐺)‘𝑥) ∥ 2))
151129, 150mtod 197 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1)
152 1re 11210 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℝ
153126nn0red 12529 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ)
154 ltnle 11289 . . . . . . . . . . . . . . . . . . . . . . 23 ((1 ∈ ℝ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
155152, 153, 154sylancr 587 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
156151, 155mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 1 < (2 pCnt ((od‘𝐺)‘𝑥)))
157 nn0ltp1le 12616 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℕ0 ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
15864, 126, 157sylancr 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
159156, 158mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥)))
160128, 159eqbrtrid 5182 . . . . . . . . . . . . . . . . . . 19 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥)))
161 eluz2 12824 . . . . . . . . . . . . . . . . . . 19 ((2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ‘2) ↔ (2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
162122, 127, 160, 161syl3anbrc 1343 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ‘2))
163 dvdsexp 16267 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℤ ∧ 2 ∈ ℕ0 ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ‘2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
16496, 121, 162, 163mp3an12i 1465 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
165120, 164eqbrtrrid 5183 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
166165, 143breqtrrd 5175 . . . . . . . . . . . . . . 15 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ ((od‘𝐺)‘𝑥))
167 dvdseq 16253 . . . . . . . . . . . . . . 15 (((((od‘𝐺)‘𝑥) ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (((od‘𝐺)‘𝑥) ∥ 4 ∧ 4 ∥ ((od‘𝐺)‘𝑥))) → ((od‘𝐺)‘𝑥) = 4)
168109, 111, 119, 166, 167syl22anc 837 . . . . . . . . . . . . . 14 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = 4)
169168, 118eqtr4d 2775 . . . . . . . . . . . . 13 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (♯‘𝐵))
1701, 98, 106, 107, 169iscygodd 19750 . . . . . . . . . . . 12 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ CycGrp)
171170, 76syl 17 . . . . . . . . . . 11 (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Abel)
172171rexlimdvaa 3156 . . . . . . . . . 10 ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∃𝑥𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
173105, 172biimtrrid 242 . . . . . . . . 9 ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (¬ ∀𝑥𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
174104, 173pm2.61d 179 . . . . . . . 8 ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Abel)
175174ex 413 . . . . . . 7 (𝐺 ∈ Grp → ((♯‘𝐵) = 4 → 𝐺 ∈ Abel))
17694, 175jaod 857 . . . . . 6 (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4) → 𝐺 ∈ Abel))
17742, 176biimtrid 241 . . . . 5 (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^5) → 𝐺 ∈ Abel))
178 id 22 . . . . . . 7 ((♯‘𝐵) = 5 → (♯‘𝐵) = 5)
179 5prm 17038 . . . . . . 7 5 ∈ ℙ
180178, 179eqeltrdi 2841 . . . . . 6 ((♯‘𝐵) = 5 → (♯‘𝐵) ∈ ℙ)
181180, 85syl5 34 . . . . 5 (𝐺 ∈ Grp → ((♯‘𝐵) = 5 → 𝐺 ∈ Abel))
182177, 181jaod 857 . . . 4 (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5) → 𝐺 ∈ Abel))
18334, 182biimtrid 241 . . 3 (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^6) → 𝐺 ∈ Abel))
184183imp 407 . 2 ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^6)) → 𝐺 ∈ Abel)
18526, 184syldan 591 1 ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐺 ∈ Abel)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2940  wral 3061  wrex 3070  Vcvv 3474  c0 4321  {csn 4627   class class class wbr 5147  cfv 6540  (class class class)co 7405  ωcom 7851  1oc1o 8455  cen 8932  Fincfn 8935  cc 11104  cr 11105  1c1 11107   + caddc 11109  +∞cpnf 11241  *cxr 11243   < clt 11244  cle 11245  cn 12208  2c2 12263  3c3 12264  4c4 12265  5c5 12266  6c6 12267  0cn0 12468  cz 12554  cuz 12818  ..^cfzo 13623  cexp 14023  chash 14286  cdvds 16193  cprime 16604   pCnt cpc 16765  Basecbs 17140  Grpcgrp 18815  odcod 19386  gExcgex 19387  Abelcabl 19643  CycGrpccyg 19739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-disj 5113  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-oadd 8466  df-omul 8467  df-er 8699  df-ec 8701  df-qs 8705  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-acn 9933  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-sum 15629  df-dvds 16194  df-gcd 16432  df-prm 16605  df-pc 16766  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-0g 17383  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-grp 18818  df-minusg 18819  df-sbg 18820  df-mulg 18945  df-subg 18997  df-eqg 18999  df-od 19390  df-gex 19391  df-cmn 19644  df-abl 19645  df-cyg 19740
This theorem is referenced by:  pgrple2abl  46994
  Copyright terms: Public domain W3C validator