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 19607

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 18715	. . . . . 6 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
3	2	adantr 482	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ≠ ∅)
4		6re 12177	. . . . . . . 8 ⊢ 6 ∈ ℝ
5		rexr 11135	. . . . . . . 8 ⊢ (6 ∈ ℝ → 6 ∈ ℝ^*)
6		pnfnlt 12979	. . . . . . . 8 ⊢ (6 ∈ ℝ^* → ¬ +∞ < 6)
7	4, 5, 6	mp2b 10	. . . . . . 7 ⊢ ¬ +∞ < 6
8	1	fvexi 6852	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
9	8	a1i 11	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → 𝐵 ∈ V)
10		hashinf 14164	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
11	9, 10	sylan 581	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
12	11	breq1d 5114	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 ↔ +∞ < 6))
13	12	biimpd 228	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 → +∞ < 6))
14	13	impancom 453	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (¬ 𝐵 ∈ Fin → +∞ < 6))
15	7, 14	mt3i 149	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ∈ Fin)
16		hashnncl 14195	. . . . . 6 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
17	15, 16	syl 17	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
18	3, 17	mpbird 257	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ ℕ)
19		nnuz 12736	. . . 4 ⊢ ℕ = (ℤ_≥‘1)
20	18, 19	eleqtrdi 2849	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (ℤ_≥‘1))
21		6nn 12176	. . . . 5 ⊢ 6 ∈ ℕ
22	21	nnzi 12461	. . . 4 ⊢ 6 ∈ ℤ
23	22	a1i 11	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 6 ∈ ℤ)
24		simpr 486	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) < 6)
25		elfzo2 13505	. . 3 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ ((♯‘𝐵) ∈ (ℤ_≥‘1) ∧ 6 ∈ ℤ ∧ (♯‘𝐵) < 6))
26	20, 23, 24, 25	syl3anbrc 1344	. 2 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (1..^6))
27		df-6 12154	. . . . . . 7 ⊢ 6 = (5 + 1)
28	27	oveq2i 7361	. . . . . 6 ⊢ (1..^6) = (1..^(5 + 1))
29	28	eleq2i 2830	. . . . 5 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ (♯‘𝐵) ∈ (1..^(5 + 1)))
30		5nn 12173	. . . . . . 7 ⊢ 5 ∈ ℕ
31	30, 19	eleqtri 2837	. . . . . 6 ⊢ 5 ∈ (ℤ_≥‘1)
32		fzosplitsni 13613	. . . . . 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 275	. . . 4 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ ((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5))
35		df-5 12153	. . . . . . . . 9 ⊢ 5 = (4 + 1)
36	35	oveq2i 7361	. . . . . . . 8 ⊢ (1..^5) = (1..^(4 + 1))
37	36	eleq2i 2830	. . . . . . 7 ⊢ ((♯‘𝐵) ∈ (1..^5) ↔ (♯‘𝐵) ∈ (1..^(4 + 1)))
38		4nn 12170	. . . . . . . . 9 ⊢ 4 ∈ ℕ
39	38, 19	eleqtri 2837	. . . . . . . 8 ⊢ 4 ∈ (ℤ_≥‘1)
40		fzosplitsni 13613	. . . . . . . 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 275	. . . . . 6 ⊢ ((♯‘𝐵) ∈ (1..^5) ↔ ((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4))
43		df-4 12152	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
44	43	oveq2i 7361	. . . . . . . . . 10 ⊢ (1..^4) = (1..^(3 + 1))
45	44	eleq2i 2830	. . . . . . . . 9 ⊢ ((♯‘𝐵) ∈ (1..^4) ↔ (♯‘𝐵) ∈ (1..^(3 + 1)))
46		3nn 12166	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
47	46, 19	eleqtri 2837	. . . . . . . . . 10 ⊢ 3 ∈ (ℤ_≥‘1)
48		fzosplitsni 13613	. . . . . . . . . 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 275	. . . . . . . 8 ⊢ ((♯‘𝐵) ∈ (1..^4) ↔ ((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3))
51		df-3 12151	. . . . . . . . . . . . 13 ⊢ 3 = (2 + 1)
52	51	oveq2i 7361	. . . . . . . . . . . 12 ⊢ (1..^3) = (1..^(2 + 1))
53	52	eleq2i 2830	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) ∈ (1..^3) ↔ (♯‘𝐵) ∈ (1..^(2 + 1)))
54		2eluzge1 12749	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ_≥‘1)
55		fzosplitsni 13613	. . . . . . . . . . . 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 275	. . . . . . . . . 10 ⊢ ((♯‘𝐵) ∈ (1..^3) ↔ ((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2))
58		elsni 4602	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝐵) ∈ {1} → (♯‘𝐵) = 1)
59		fzo12sn 13585	. . . . . . . . . . . . . . . . 17 ⊢ (1..^2) = {1}
60	58, 59	eleq2s 2857	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐵) ∈ (1..^2) → (♯‘𝐵) = 1)
61	60	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = 1)
62		hash1 14233	. . . . . . . . . . . . . . 15 ⊢ (♯‘1_o) = 1
63	61, 62	eqtr4di 2796	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = (♯‘1_o))
64		1nn0 12363	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ₀
65	61, 64	eqeltrdi 2847	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) ∈ ℕ₀)
66		hashclb 14187	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ₀))
67	8, 66	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ₀)
68	65, 67	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ∈ Fin)
69		1onn 8554	. . . . . . . . . . . . . . . 16 ⊢ 1_o ∈ ω
70		nnfi 9045	. . . . . . . . . . . . . . . 16 ⊢ (1_o ∈ ω → 1_o ∈ Fin)
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 1_o ∈ Fin
72		hashen 14176	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ 1_o ∈ Fin) → ((♯‘𝐵) = (♯‘1_o) ↔ 𝐵 ≈ 1_o))
73	68, 71, 72	sylancl 587	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → ((♯‘𝐵) = (♯‘1_o) ↔ 𝐵 ≈ 1_o))
74	63, 73	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ≈ 1_o)
75	1	0cyg 19605	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1_o) → 𝐺 ∈ CycGrp)
76		cygabl 19603	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel)
77	75, 76	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1_o) → 𝐺 ∈ Abel)
78	74, 77	syldan 592	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐺 ∈ Abel)
79	78	ex 414	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^2) → 𝐺 ∈ Abel))
80		id 22	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) = 2 → (♯‘𝐵) = 2)
81		2prm 16504	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℙ
82	80, 81	eqeltrdi 2847	. . . . . . . . . . . 12 ⊢ ((♯‘𝐵) = 2 → (♯‘𝐵) ∈ ℙ)
83	1	prmcyg 19606	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ CycGrp)
84	83, 76	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ Abel)
85	84	ex 414	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ ℙ → 𝐺 ∈ Abel))
86	82, 85	syl5 34	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 2 → 𝐺 ∈ Abel))
87	79, 86	jaod 858	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2) → 𝐺 ∈ Abel))
88	57, 87	biimtrid 241	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^3) → 𝐺 ∈ Abel))
89		id 22	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) = 3 → (♯‘𝐵) = 3)
90		3prm 16506	. . . . . . . . . . 11 ⊢ 3 ∈ ℙ
91	89, 90	eqeltrdi 2847	. . . . . . . . . 10 ⊢ ((♯‘𝐵) = 3 → (♯‘𝐵) ∈ ℙ)
92	91, 85	syl5 34	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 3 → 𝐺 ∈ Abel))
93	88, 92	jaod 858	. . . . . . . 8 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3) → 𝐺 ∈ Abel))
94	50, 93	biimtrid 241	. . . . . . 7 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^4) → 𝐺 ∈ Abel))
95		simpl 484	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Grp)
96		2z 12469	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
97		eqid 2738	. . . . . . . . . . . 12 ⊢ (gEx‘𝐺) = (gEx‘𝐺)
98		eqid 2738	. . . . . . . . . . . 12 ⊢ (od‘𝐺) = (od‘𝐺)
99	1, 97, 98	gexdvds2 19302	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 2 ∈ ℤ) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
100	95, 96, 99	sylancl 587	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
101	1, 97	gex2abl 19564	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (gEx‘𝐺) ∥ 2) → 𝐺 ∈ Abel)
102	101	ex 414	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
103	102	adantr 482	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
104	100, 103	sylbird 260	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
105		rexnal 3102	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 ↔ ¬ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2)
106	95	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Grp)
107		simprl 770	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝑥 ∈ 𝐵)
108	1, 98	odcl 19253	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐵 → ((od‘𝐺)‘𝑥) ∈ ℕ₀)
109	108	ad2antrl 727	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ₀)
110		4nn0 12366	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ₀
111	110	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∈ ℕ₀)
112		simpr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) = 4)
113	112, 110	eqeltrdi 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) ∈ ℕ₀)
114	113, 67	sylibr 233	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐵 ∈ Fin)
115	114	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐵 ∈ Fin)
116	1, 98	oddvds2 19283	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
117	106, 115, 107, 116	syl3anc 1372	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
118	112	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (♯‘𝐵) = 4)
119	117, 118	breqtrd 5130	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ 4)
120		sq2 14029	. . . . . . . . . . . . . . . . 17 ⊢ (2↑2) = 4
121		2nn0 12364	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ₀
122	96	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ∈ ℤ)
123	1, 98	odcl2 19282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ)
124	106, 115, 107, 123	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ)
125		pccl 16657	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀)
126	81, 124, 125	sylancr 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀)
127	126	nn0zd 12459	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ)
128		df-2 12150	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
129		simprr 772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ ((od‘𝐺)‘𝑥) ∥ 2)
130		dvdsexp 16146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀ ∧ 1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥)))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1))
131	130	3expia 1122	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
132	96, 126, 131	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
133		1z 12467	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℤ
134		eluz 12711	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 1 ∈ ℤ) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
135	127, 133, 134	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
136		oveq2 7358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 2 → (2↑𝑛) = (2↑2))
137	136, 120	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 2 → (2↑𝑛) = 4)
138	137	breq2d 5116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 2 → (((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) ∥ 4))
139	138	rspcev 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ₀ ∧ ((od‘𝐺)‘𝑥) ∥ 4) → ∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
140	121, 119, 139	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
141		pcprmpw2 16690	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))))
142	81, 124, 141	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))))
143	140, 142	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
144	143	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) = ((od‘𝐺)‘𝑥))
145		2cn 12162	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 ∈ ℂ
146		exp1 13903	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5117	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1) ↔ ((od‘𝐺)‘𝑥) ∥ 2))
150	132, 135, 149	3imtr3d 293	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1 → ((od‘𝐺)‘𝑥) ∥ 2))
151	129, 150	mtod 197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1)
152		1re 11089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ
153	126	nn0red 12408	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ)
154		ltnle 11168	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℝ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
155	152, 153, 154	sylancr 588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
156	151, 155	mpbird 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 1 < (2 pCnt ((od‘𝐺)‘𝑥)))
157		nn0ltp1le 12495	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℕ₀ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
158	64, 126, 157	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
159	156, 158	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥)))
160	128, 159	eqbrtrid 5139	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥)))
161		eluz2 12703	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
162	122, 127, 160, 161	syl3anbrc 1344	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ_≥‘2))
163		dvdsexp 16146	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℤ ∧ 2 ∈ ℕ₀ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ_≥‘2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
164	96, 121, 162, 163	mp3an12i 1466	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
165	120, 164	eqbrtrrid 5140	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
166	165, 143	breqtrrd 5132	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ ((od‘𝐺)‘𝑥))
167		dvdseq 16132	. . . . . . . . . . . . . . 15 ⊢ (((((od‘𝐺)‘𝑥) ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (((od‘𝐺)‘𝑥) ∥ 4 ∧ 4 ∥ ((od‘𝐺)‘𝑥))) → ((od‘𝐺)‘𝑥) = 4)
168	109, 111, 119, 166, 167	syl22anc 838	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = 4)
169	168, 118	eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (♯‘𝐵))
170	1, 98, 106, 107, 169	iscygodd 19600	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ CycGrp)
171	170, 76	syl 17	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Abel)
172	171	rexlimdvaa 3152	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∃𝑥 ∈ 𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
173	105, 172	biimtrrid 242	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (¬ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
174	104, 173	pm2.61d 179	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Abel)
175	174	ex 414	. . . . . . 7 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 4 → 𝐺 ∈ Abel))
176	94, 175	jaod 858	. . . . . 6 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4) → 𝐺 ∈ Abel))
177	42, 176	biimtrid 241	. . . . 5 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^5) → 𝐺 ∈ Abel))
178		id 22	. . . . . . 7 ⊢ ((♯‘𝐵) = 5 → (♯‘𝐵) = 5)
179		5prm 16917	. . . . . . 7 ⊢ 5 ∈ ℙ
180	178, 179	eqeltrdi 2847	. . . . . 6 ⊢ ((♯‘𝐵) = 5 → (♯‘𝐵) ∈ ℙ)
181	180, 85	syl5 34	. . . . 5 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 5 → 𝐺 ∈ Abel))
182	177, 181	jaod 858	. . . 4 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5) → 𝐺 ∈ Abel))
183	34, 182	biimtrid 241	. . 3 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^6) → 𝐺 ∈ Abel))
184	183	imp 408	. 2 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^6)) → 𝐺 ∈ Abel)
185	26, 184	syldan 592	1 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐺 ∈ Abel)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 = wceq 1542 ∈ wcel 2107 ≠ wne 2942 ∀wral 3063 ∃wrex 3072 Vcvv 3444 ∅c0 4281 {csn 4585 class class class wbr 5104 ‘cfv 6492 (class class class)co 7350 ωcom 7793 1_oc1o 8373 ≈ cen 8814 Fincfn 8817 ℂcc 10983 ℝcr 10984 1c1 10986 + caddc 10988 +∞cpnf 11120 ℝ^*cxr 11122 < clt 11123 ≤ cle 11124 ℕcn 12087 2c2 12142 3c3 12143 4c4 12144 5c5 12145 6c6 12146 ℕ₀cn0 12347 ℤcz 12433 ℤ_≥cuz 12697 ..^cfzo 13497 ↑cexp 13897 ♯chash 14159 ∥ cdvds 16072 ℙcprime 16483 pCnt cpc 16644 Basecbs 17019 Grpcgrp 18684 odcod 19241 gExcgex 19242 Abelcabl 19498 CycGrpccyg 19589

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-rep 5241 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7663 ax-inf2 9511 ax-cnex 11041 ax-resscn 11042 ax-1cn 11043 ax-icn 11044 ax-addcl 11045 ax-addrcl 11046 ax-mulcl 11047 ax-mulrcl 11048 ax-mulcom 11049 ax-addass 11050 ax-mulass 11051 ax-distr 11052 ax-i2m1 11053 ax-1ne0 11054 ax-1rid 11055 ax-rnegex 11056 ax-rrecex 11057 ax-cnre 11058 ax-pre-lttri 11059 ax-pre-lttrn 11060 ax-pre-ltadd 11061 ax-pre-mulgt0 11062 ax-pre-sup 11063

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-rmo 3352 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-pss 3928 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-int 4907 df-iun 4955 df-disj 5070 df-br 5105 df-opab 5167 df-mpt 5188 df-tr 5222 df-id 5529 df-eprel 5535 df-po 5543 df-so 5544 df-fr 5586 df-se 5587 df-we 5588 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6250 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6444 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7306 df-ov 7353 df-oprab 7354 df-mpo 7355 df-om 7794 df-1st 7912 df-2nd 7913 df-frecs 8180 df-wrecs 8211 df-recs 8285 df-rdg 8324 df-1o 8380 df-2o 8381 df-oadd 8384 df-omul 8385 df-er 8582 df-ec 8584 df-qs 8588 df-map 8701 df-en 8818 df-dom 8819 df-sdom 8820 df-fin 8821 df-sup 9312 df-inf 9313 df-oi 9380 df-dju 9771 df-card 9809 df-acn 9812 df-pnf 11125 df-mnf 11126 df-xr 11127 df-ltxr 11128 df-le 11129 df-sub 11321 df-neg 11322 df-div 11747 df-nn 12088 df-2 12150 df-3 12151 df-4 12152 df-5 12153 df-6 12154 df-7 12155 df-8 12156 df-9 12157 df-n0 12348 df-z 12434 df-dec 12553 df-uz 12698 df-q 12804 df-rp 12846 df-fz 13355 df-fzo 13498 df-fl 13627 df-mod 13705 df-seq 13837 df-exp 13898 df-hash 14160 df-cj 14919 df-re 14920 df-im 14921 df-sqrt 15055 df-abs 15056 df-clim 15306 df-sum 15507 df-dvds 16073 df-gcd 16311 df-prm 16484 df-pc 16645 df-sets 16972 df-slot 16990 df-ndx 17002 df-base 17020 df-ress 17049 df-plusg 17082 df-0g 17259 df-mgm 18433 df-sgrp 18482 df-mnd 18493 df-grp 18687 df-minusg 18688 df-sbg 18689 df-mulg 18808 df-subg 18860 df-eqg 18862 df-od 19245 df-gex 19246 df-cmn 19499 df-abl 19500 df-cyg 19590

This theorem is referenced by: pgrple2abl 46232

W3C validator