lt6abl - Metamath Proof Explorer

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

Theorem lt6abl 20011

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.

Step	Hyp	Ref	Expression
1		cygctb.1	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
2	1	grpbn0 19079	. . . . . 6 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
3	2	adantr 486	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ≠ ∅)
4		6re 12348	. . . . . . . 8 ⊢ 6 ∈ ℝ
5		rexr 11272	. . . . . . . 8 ⊢ (6 ∈ ℝ → 6 ∈ ℝ^*)
6		pnfnlt 13171	. . . . . . . 8 ⊢ (6 ∈ ℝ^* → ¬ +∞ < 6)
7	4, 5, 6	mp2b 10	. . . . . . 7 ⊢ ¬ +∞ < 6
8	1	fvexi 6899	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
9	8	a1i 11	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → 𝐵 ∈ V)
10		hashinf 14391	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
11	9, 10	sylan 592	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
12	11	breq1d 5121	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 ↔ +∞ < 6))
13	12	biimpd 232	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 → +∞ < 6))
14	13	impancom 457	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (¬ 𝐵 ∈ Fin → +∞ < 6))
15	7, 14	mt3i 150	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ∈ Fin)
16		hashnncl 14422	. . . . . 6 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
17	15, 16	syl 18	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
18	3, 17	mpbird 260	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ ℕ)
19		nnuz 12919	. . . 4 ⊢ ℕ = (ℤ_≥‘1)
20	18, 19	eleqtrdi 2875	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (ℤ_≥‘1))
21		6nn 12347	. . . . 5 ⊢ 6 ∈ ℕ
22	21	nnzi 12635	. . . 4 ⊢ 6 ∈ ℤ
23	22	a1i 11	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 6 ∈ ℤ)
24		simpr 490	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) < 6)
25		elfzo2 13709	. . 3 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ ((♯‘𝐵) ∈ (ℤ_≥‘1) ∧ 6 ∈ ℤ ∧ (♯‘𝐵) < 6))
26	20, 23, 24, 25	syl3anbrc 1362	. 2 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (1..^6))
27		df-6 12324	. . . . . . 7 ⊢ 6 = (5 + 1)
28	27	oveq2i 7430	. . . . . 6 ⊢ (1..^6) = (1..^(5 + 1))
29	28	eleq2i 2857	. . . . 5 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ (♯‘𝐵) ∈ (1..^(5 + 1)))
30		5nn 12344	. . . . . . 7 ⊢ 5 ∈ ℕ
31	30, 19	eleqtri 2863	. . . . . 6 ⊢ 5 ∈ (ℤ_≥‘1)
32		fzosplitsni 13827	. . . . . 6 ⊢ (5 ∈ (ℤ_≥‘1) → ((♯‘𝐵) ∈ (1..^(5 + 1)) ↔ ((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5)))
33	31, 32	ax-mp 5	. . . . 5 ⊢ ((♯‘𝐵) ∈ (1..^(5 + 1)) ↔ ((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5))
34	29, 33	bitri 278	. . . 4 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ ((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5))
35		df-5 12323	. . . . . . . . 9 ⊢ 5 = (4 + 1)
36	35	oveq2i 7430	. . . . . . . 8 ⊢ (1..^5) = (1..^(4 + 1))
37	36	eleq2i 2857	. . . . . . 7 ⊢ ((♯‘𝐵) ∈ (1..^5) ↔ (♯‘𝐵) ∈ (1..^(4 + 1)))
38		4nn 12341	. . . . . . . . 9 ⊢ 4 ∈ ℕ
39	38, 19	eleqtri 2863	. . . . . . . 8 ⊢ 4 ∈ (ℤ_≥‘1)
40		fzosplitsni 13827	. . . . . . . 8 ⊢ (4 ∈ (ℤ_≥‘1) → ((♯‘𝐵) ∈ (1..^(4 + 1)) ↔ ((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4)))
41	39, 40	ax-mp 5	. . . . . . 7 ⊢ ((♯‘𝐵) ∈ (1..^(4 + 1)) ↔ ((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4))
42	37, 41	bitri 278	. . . . . 6 ⊢ ((♯‘𝐵) ∈ (1..^5) ↔ ((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4))
43		df-4 12322	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
44	43	oveq2i 7430	. . . . . . . . . 10 ⊢ (1..^4) = (1..^(3 + 1))
45	44	eleq2i 2857	. . . . . . . . 9 ⊢ ((♯‘𝐵) ∈ (1..^4) ↔ (♯‘𝐵) ∈ (1..^(3 + 1)))
46		3nn 12337	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
47	46, 19	eleqtri 2863	. . . . . . . . . 10 ⊢ 3 ∈ (ℤ_≥‘1)
48		fzosplitsni 13827	. . . . . . . . . 10 ⊢ (3 ∈ (ℤ_≥‘1) → ((♯‘𝐵) ∈ (1..^(3 + 1)) ↔ ((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3)))
49	47, 48	ax-mp 5	. . . . . . . . 9 ⊢ ((♯‘𝐵) ∈ (1..^(3 + 1)) ↔ ((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3))
50	45, 49	bitri 278	. . . . . . . 8 ⊢ ((♯‘𝐵) ∈ (1..^4) ↔ ((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3))
51		df-3 12321	. . . . . . . . . . . . 13 ⊢ 3 = (2 + 1)
52	51	oveq2i 7430	. . . . . . . . . . . 12 ⊢ (1..^3) = (1..^(2 + 1))
53	52	eleq2i 2857	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) ∈ (1..^3) ↔ (♯‘𝐵) ∈ (1..^(2 + 1)))
54		2eluzge1 12924	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ_≥‘1)
55		fzosplitsni 13827	. . . . . . . . . . . 12 ⊢ (2 ∈ (ℤ_≥‘1) → ((♯‘𝐵) ∈ (1..^(2 + 1)) ↔ ((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2)))
56	54, 55	ax-mp 5	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) ∈ (1..^(2 + 1)) ↔ ((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2))
57	53, 56	bitri 278	. . . . . . . . . 10 ⊢ ((♯‘𝐵) ∈ (1..^3) ↔ ((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2))
58		elsni 4608	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝐵) ∈ {1} → (♯‘𝐵) = 1)
59		fzo12sn 13796	. . . . . . . . . . . . . . . . 17 ⊢ (1..^2) = {1}
60	58, 59	eleq2s 2883	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐵) ∈ (1..^2) → (♯‘𝐵) = 1)
61	60	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = 1)
62		hash1 14460	. . . . . . . . . . . . . . 15 ⊢ (♯‘1_o) = 1
63	61, 62	eqtr4di 2818	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = (♯‘1_o))
64		1nn0 12537	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ₀
65	61, 64	eqeltrdi 2873	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) ∈ ℕ₀)
66		hashclb 14414	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ₀))
67	8, 66	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ₀)
68	65, 67	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ∈ Fin)
69		1onn 8632	. . . . . . . . . . . . . . . 16 ⊢ 1_o ∈ ω
70		nnfi 9159	. . . . . . . . . . . . . . . 16 ⊢ (1_o ∈ ω → 1_o ∈ Fin)
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 1_o ∈ Fin
72		hashen 14403	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ 1_o ∈ Fin) → ((♯‘𝐵) = (♯‘1_o) ↔ 𝐵 ≈ 1_o))
73	68, 71, 72	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → ((♯‘𝐵) = (♯‘1_o) ↔ 𝐵 ≈ 1_o))
74	63, 73	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ≈ 1_o)
75	1	0cyg 20009	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1_o) → 𝐺 ∈ CycGrp)
76		cygabl 20007	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel)
77	75, 76	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1_o) → 𝐺 ∈ Abel)
78	74, 77	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐺 ∈ Abel)
79	78	ex 418	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^2) → 𝐺 ∈ Abel))
80		id 23	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) = 2 → (♯‘𝐵) = 2)
81		2prm 16774	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℙ
82	80, 81	eqeltrdi 2873	. . . . . . . . . . . 12 ⊢ ((♯‘𝐵) = 2 → (♯‘𝐵) ∈ ℙ)
83	1	prmcyg 20010	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ CycGrp)
84	83, 76	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ Abel)
85	84	ex 418	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ ℙ → 𝐺 ∈ Abel))
86	82, 85	syl5 35	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 2 → 𝐺 ∈ Abel))
87	79, 86	jaod 873	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2) → 𝐺 ∈ Abel))
88	57, 87	biimtrid 245	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^3) → 𝐺 ∈ Abel))
89		id 23	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) = 3 → (♯‘𝐵) = 3)
90		3prm 16776	. . . . . . . . . . 11 ⊢ 3 ∈ ℙ
91	89, 90	eqeltrdi 2873	. . . . . . . . . 10 ⊢ ((♯‘𝐵) = 3 → (♯‘𝐵) ∈ ℙ)
92	91, 85	syl5 35	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 3 → 𝐺 ∈ Abel))
93	88, 92	jaod 873	. . . . . . . 8 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3) → 𝐺 ∈ Abel))
94	50, 93	biimtrid 245	. . . . . . 7 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^4) → 𝐺 ∈ Abel))
95		simpl 488	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Grp)
96		2z 12643	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
97		eqid 2765	. . . . . . . . . . . 12 ⊢ (gEx‘𝐺) = (gEx‘𝐺)
98		eqid 2765	. . . . . . . . . . . 12 ⊢ (od‘𝐺) = (od‘𝐺)
99	1, 97, 98	gexdvds2 19701	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 2 ∈ ℤ) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
100	95, 96, 99	sylancl 598	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
101	1, 97	gex2abl 19967	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (gEx‘𝐺) ∥ 2) → 𝐺 ∈ Abel)
102	101	ex 418	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
103	102	adantr 486	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
104	100, 103	sylbird 263	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
105		rexnal 3119	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 ↔ ¬ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2)
106	95	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Grp)
107		simprl 783	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝑥 ∈ 𝐵)
108	1, 98	odcl 19652	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐵 → ((od‘𝐺)‘𝑥) ∈ ℕ₀)
109	108	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ₀)
110		4nn0 12540	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ₀
111	110	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∈ ℕ₀)
112		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) = 4)
113	112, 110	eqeltrdi 2873	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) ∈ ℕ₀)
114	113, 67	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐵 ∈ Fin)
115	114	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐵 ∈ Fin)
116	1, 98	oddvds2 19682	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
117	106, 115, 107, 116	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
118	112	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (♯‘𝐵) = 4)
119	117, 118	breqtrd 5139	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ 4)
120		sq2 14253	. . . . . . . . . . . . . . . . 17 ⊢ (2↑2) = 4
121		2nn0 12538	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ₀
122	96	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ∈ ℤ)
123	1, 98	odcl2 19681	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ)
124	106, 115, 107, 123	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ)
125		pccl 16933	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀)
126	81, 124, 125	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀)
127	126	nn0zd 12633	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ)
128		df-2 12320	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
129		simprr 785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ ((od‘𝐺)‘𝑥) ∥ 2)
130		dvdsexp 16410	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀ ∧ 1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥)))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1))
131	130	3expia 1139	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
132	96, 126, 131	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
133		1z 12641	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℤ
134		eluz 12894	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 1 ∈ ℤ) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
135	127, 133, 134	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
136		oveq2 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 2 → (2↑𝑛) = (2↑2))
137	136, 120	eqtrdi 2816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 2 → (2↑𝑛) = 4)
138	137	breq2d 5123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 2 → (((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) ∥ 4))
139	138	rspcev 3583	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ₀ ∧ ((od‘𝐺)‘𝑥) ∥ 4) → ∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
140	121, 119, 139	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
141		pcprmpw2 16966	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))))
142	81, 124, 141	sylancr 599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))))
143	140, 142	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
144	143	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) = ((od‘𝐺)‘𝑥))
145		2cn 12333	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 ∈ ℂ
146		exp1 14123	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2 ∈ ℂ → (2↑1) = 2)
147	145, 146	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (2↑1) = 2
148	147	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑1) = 2)
149	144, 148	breq12d 5124	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1) ↔ ((od‘𝐺)‘𝑥) ∥ 2))
150	132, 135, 149	3imtr3d 296	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1 → ((od‘𝐺)‘𝑥) ∥ 2))
151	129, 150	mtod 201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1)
152		1re 11225	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ
153	126	nn0red 12583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ)
154		ltnle 11306	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℝ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
155	152, 153, 154	sylancr 599	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
156	151, 155	mpbird 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 1 < (2 pCnt ((od‘𝐺)‘𝑥)))
157		nn0ltp1le 12672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℕ₀ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
158	64, 126, 157	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
159	156, 158	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥)))
160	128, 159	eqbrtrid 5148	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥)))
161		eluz2 12886	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
162	122, 127, 160, 161	syl3anbrc 1362	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ_≥‘2))
163		dvdsexp 16410	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℤ ∧ 2 ∈ ℕ₀ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ_≥‘2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
164	96, 121, 162, 163	mp3an12i 1494	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
165	120, 164	eqbrtrrid 5149	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
166	165, 143	breqtrrd 5141	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ ((od‘𝐺)‘𝑥))
167		dvdseq 16396	. . . . . . . . . . . . . . 15 ⊢ (((((od‘𝐺)‘𝑥) ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (((od‘𝐺)‘𝑥) ∥ 4 ∧ 4 ∥ ((od‘𝐺)‘𝑥))) → ((od‘𝐺)‘𝑥) = 4)
168	109, 111, 119, 166, 167	syl22anc 852	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = 4)
169	168, 118	eqtr4d 2803	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (♯‘𝐵))
170	1, 98, 106, 107, 169	iscygodd 20004	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ CycGrp)
171	170, 76	syl 18	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Abel)
172	171	rexlimdvaa 3169	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∃𝑥 ∈ 𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
173	105, 172	biimtrrid 246	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (¬ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
174	104, 173	pm2.61d 181	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Abel)
175	174	ex 418	. . . . . . 7 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 4 → 𝐺 ∈ Abel))
176	94, 175	jaod 873	. . . . . 6 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4) → 𝐺 ∈ Abel))
177	42, 176	biimtrid 245	. . . . 5 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^5) → 𝐺 ∈ Abel))
178		id 23	. . . . . . 7 ⊢ ((♯‘𝐵) = 5 → (♯‘𝐵) = 5)
179		5prm 17192	. . . . . . 7 ⊢ 5 ∈ ℙ
180	178, 179	eqeltrdi 2873	. . . . . 6 ⊢ ((♯‘𝐵) = 5 → (♯‘𝐵) ∈ ℙ)
181	180, 85	syl5 35	. . . . 5 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 5 → 𝐺 ∈ Abel))
182	177, 181	jaod 873	. . . 4 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5) → 𝐺 ∈ Abel))
183	34, 182	biimtrid 245	. . 3 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^6) → 𝐺 ∈ Abel))
184	183	imp 412	. 2 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^6)) → 𝐺 ∈ Abel)
185	26, 184	syldan 603	1 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐺 ∈ Abel)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 Vcvv 3457 ∅c0 4286 {csn 4591 class class class wbr 5111 ‘cfv 6540 (class class class)co 7419 ωcom 7868 1_oc1o 8452 ≈ cen 8946 Fincfn 8949 ℂcc 11115 ℝcr 11116 1c1 11118 + caddc 11120 +∞cpnf 11257 ℝ^*cxr 11259 < clt 11260 ≤ cle 11261 ℕcn 12250 2c2 12312 3c3 12313 4c4 12314 5c5 12315 6c6 12316 ℕ₀cn0 12521 ℤcz 12608 ℤ_≥cuz 12880 ..^cfzo 13701 ↑cexp 14117 ♯chash 14386 ∥ cdvds 16334 ℙcprime 16753 pCnt cpc 16920 Basecbs 17293 Grpcgrp 19046 odcod 19640 gExcgex 19641 Abelcabl 19897 CycGrpccyg 19993

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194 ax-pre-sup 11195

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-disj 5079 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 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 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-omul 8464 df-er 8700 df-ec 8702 df-qs 8706 df-map 8832 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-sup 9409 df-inf 9410 df-oi 9479 df-dju 9903 df-card 9941 df-acn 9944 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-div 11889 df-nn 12251 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-7 12325 df-8 12326 df-9 12327 df-n0 12522 df-z 12609 df-dec 12730 df-uz 12881 df-q 12991 df-rp 13035 df-fz 13554 df-fzo 13702 df-fl 13845 df-mod 13923 df-seq 14058 df-exp 14118 df-hash 14387 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-clim 15565 df-sum 15764 df-dvds 16335 df-gcd 16577 df-prm 16754 df-pc 16921 df-sets 17248 df-slot 17266 df-ndx 17278 df-base 17294 df-ress 17315 df-plusg 17347 df-0g 17518 df-mgm 18722 df-sgrp 18811 df-mnd 18827 df-grp 19049 df-minusg 19050 df-sbg 19051 df-mulg 19180 df-subg 19235 df-eqg 19237 df-od 19644 df-gex 19645 df-cmn 19898 df-abl 19899 df-cyg 19994

This theorem is used by: pgrple2abl 49204

W3C validator