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 19965

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 19033	. . . . . 6 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
3	2	adantr 485	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ≠ ∅)
4		6re 12331	. . . . . . . 8 ⊢ 6 ∈ ℝ
5		rexr 11255	. . . . . . . 8 ⊢ (6 ∈ ℝ → 6 ∈ ℝ^*)
6		pnfnlt 13153	. . . . . . . 8 ⊢ (6 ∈ ℝ^* → ¬ +∞ < 6)
7	4, 5, 6	mp2b 10	. . . . . . 7 ⊢ ¬ +∞ < 6
8	1	fvexi 6896	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
9	8	a1i 11	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → 𝐵 ∈ V)
10		hashinf 14371	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
11	9, 10	sylan 591	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
12	11	breq1d 5123	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 ↔ +∞ < 6))
13	12	biimpd 232	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 → +∞ < 6))
14	13	impancom 456	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (¬ 𝐵 ∈ Fin → +∞ < 6))
15	7, 14	mt3i 150	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ∈ Fin)
16		hashnncl 14402	. . . . . 6 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
17	15, 16	syl 18	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
18	3, 17	mpbird 260	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ ℕ)
19		nnuz 12901	. . . 4 ⊢ ℕ = (ℤ_≥‘1)
20	18, 19	eleqtrdi 2879	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (ℤ_≥‘1))
21		6nn 12330	. . . . 5 ⊢ 6 ∈ ℕ
22	21	nnzi 12618	. . . 4 ⊢ 6 ∈ ℤ
23	22	a1i 11	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 6 ∈ ℤ)
24		simpr 489	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) < 6)
25		elfzo2 13690	. . 3 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ ((♯‘𝐵) ∈ (ℤ_≥‘1) ∧ 6 ∈ ℤ ∧ (♯‘𝐵) < 6))
26	20, 23, 24, 25	syl3anbrc 1360	. 2 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (1..^6))
27		df-6 12307	. . . . . . 7 ⊢ 6 = (5 + 1)
28	27	oveq2i 7422	. . . . . 6 ⊢ (1..^6) = (1..^(5 + 1))
29	28	eleq2i 2861	. . . . 5 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ (♯‘𝐵) ∈ (1..^(5 + 1)))
30		5nn 12327	. . . . . . 7 ⊢ 5 ∈ ℕ
31	30, 19	eleqtri 2867	. . . . . 6 ⊢ 5 ∈ (ℤ_≥‘1)
32		fzosplitsni 13808	. . . . . 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 12306	. . . . . . . . 9 ⊢ 5 = (4 + 1)
36	35	oveq2i 7422	. . . . . . . 8 ⊢ (1..^5) = (1..^(4 + 1))
37	36	eleq2i 2861	. . . . . . 7 ⊢ ((♯‘𝐵) ∈ (1..^5) ↔ (♯‘𝐵) ∈ (1..^(4 + 1)))
38		4nn 12324	. . . . . . . . 9 ⊢ 4 ∈ ℕ
39	38, 19	eleqtri 2867	. . . . . . . 8 ⊢ 4 ∈ (ℤ_≥‘1)
40		fzosplitsni 13808	. . . . . . . 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 12305	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
44	43	oveq2i 7422	. . . . . . . . . 10 ⊢ (1..^4) = (1..^(3 + 1))
45	44	eleq2i 2861	. . . . . . . . 9 ⊢ ((♯‘𝐵) ∈ (1..^4) ↔ (♯‘𝐵) ∈ (1..^(3 + 1)))
46		3nn 12320	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
47	46, 19	eleqtri 2867	. . . . . . . . . 10 ⊢ 3 ∈ (ℤ_≥‘1)
48		fzosplitsni 13808	. . . . . . . . . 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 12304	. . . . . . . . . . . . 13 ⊢ 3 = (2 + 1)
52	51	oveq2i 7422	. . . . . . . . . . . 12 ⊢ (1..^3) = (1..^(2 + 1))
53	52	eleq2i 2861	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) ∈ (1..^3) ↔ (♯‘𝐵) ∈ (1..^(2 + 1)))
54		2eluzge1 12906	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ_≥‘1)
55		fzosplitsni 13808	. . . . . . . . . . . 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 4611	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝐵) ∈ {1} → (♯‘𝐵) = 1)
59		fzo12sn 13777	. . . . . . . . . . . . . . . . 17 ⊢ (1..^2) = {1}
60	58, 59	eleq2s 2887	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐵) ∈ (1..^2) → (♯‘𝐵) = 1)
61	60	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = 1)
62		hash1 14440	. . . . . . . . . . . . . . 15 ⊢ (♯‘1_o) = 1
63	61, 62	eqtr4di 2822	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = (♯‘1_o))
64		1nn0 12520	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ₀
65	61, 64	eqeltrdi 2877	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) ∈ ℕ₀)
66		hashclb 14394	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ₀))
67	8, 66	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ₀)
68	65, 67	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ∈ Fin)
69		1onn 8626	. . . . . . . . . . . . . . . 16 ⊢ 1_o ∈ ω
70		nnfi 9152	. . . . . . . . . . . . . . . 16 ⊢ (1_o ∈ ω → 1_o ∈ Fin)
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 1_o ∈ Fin
72		hashen 14383	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ 1_o ∈ Fin) → ((♯‘𝐵) = (♯‘1_o) ↔ 𝐵 ≈ 1_o))
73	68, 71, 72	sylancl 597	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → ((♯‘𝐵) = (♯‘1_o) ↔ 𝐵 ≈ 1_o))
74	63, 73	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ≈ 1_o)
75	1	0cyg 19963	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1_o) → 𝐺 ∈ CycGrp)
76		cygabl 19961	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel)
77	75, 76	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1_o) → 𝐺 ∈ Abel)
78	74, 77	syldan 602	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐺 ∈ Abel)
79	78	ex 417	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^2) → 𝐺 ∈ Abel))
80		id 23	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) = 2 → (♯‘𝐵) = 2)
81		2prm 16750	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℙ
82	80, 81	eqeltrdi 2877	. . . . . . . . . . . 12 ⊢ ((♯‘𝐵) = 2 → (♯‘𝐵) ∈ ℙ)
83	1	prmcyg 19964	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ CycGrp)
84	83, 76	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ Abel)
85	84	ex 417	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ ℙ → 𝐺 ∈ Abel))
86	82, 85	syl5 35	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 2 → 𝐺 ∈ Abel))
87	79, 86	jaod 872	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2) → 𝐺 ∈ Abel))
88	57, 87	biimtrid 245	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^3) → 𝐺 ∈ Abel))
89		id 23	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) = 3 → (♯‘𝐵) = 3)
90		3prm 16752	. . . . . . . . . . 11 ⊢ 3 ∈ ℙ
91	89, 90	eqeltrdi 2877	. . . . . . . . . 10 ⊢ ((♯‘𝐵) = 3 → (♯‘𝐵) ∈ ℙ)
92	91, 85	syl5 35	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 3 → 𝐺 ∈ Abel))
93	88, 92	jaod 872	. . . . . . . 8 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3) → 𝐺 ∈ Abel))
94	50, 93	biimtrid 245	. . . . . . 7 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^4) → 𝐺 ∈ Abel))
95		simpl 487	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Grp)
96		2z 12626	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
97		eqid 2769	. . . . . . . . . . . 12 ⊢ (gEx‘𝐺) = (gEx‘𝐺)
98		eqid 2769	. . . . . . . . . . . 12 ⊢ (od‘𝐺) = (od‘𝐺)
99	1, 97, 98	gexdvds2 19655	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 2 ∈ ℤ) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
100	95, 96, 99	sylancl 597	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
101	1, 97	gex2abl 19921	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (gEx‘𝐺) ∥ 2) → 𝐺 ∈ Abel)
102	101	ex 417	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
103	102	adantr 485	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
104	100, 103	sylbird 263	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
105		rexnal 3123	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 ↔ ¬ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2)
106	95	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Grp)
107		simprl 782	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝑥 ∈ 𝐵)
108	1, 98	odcl 19606	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐵 → ((od‘𝐺)‘𝑥) ∈ ℕ₀)
109	108	ad2antrl 740	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ₀)
110		4nn0 12523	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ₀
111	110	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∈ ℕ₀)
112		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) = 4)
113	112, 110	eqeltrdi 2877	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) ∈ ℕ₀)
114	113, 67	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐵 ∈ Fin)
115	114	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐵 ∈ Fin)
116	1, 98	oddvds2 19636	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
117	106, 115, 107, 116	syl3anc 1396	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
118	112	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (♯‘𝐵) = 4)
119	117, 118	breqtrd 5141	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ 4)
120		sq2 14233	. . . . . . . . . . . . . . . . 17 ⊢ (2↑2) = 4
121		2nn0 12521	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ₀
122	96	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ∈ ℤ)
123	1, 98	odcl2 19635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ)
124	106, 115, 107, 123	syl3anc 1396	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ)
125		pccl 16909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀)
126	81, 124, 125	sylancr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀)
127	126	nn0zd 12616	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ)
128		df-2 12303	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
129		simprr 784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ ((od‘𝐺)‘𝑥) ∥ 2)
130		dvdsexp 16386	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀ ∧ 1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥)))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1))
131	130	3expia 1137	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
132	96, 126, 131	sylancr 598	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
133		1z 12624	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℤ
134		eluz 12876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 1 ∈ ℤ) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
135	127, 133, 134	sylancl 597	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ_≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
136		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 2 → (2↑𝑛) = (2↑2))
137	136, 120	eqtrdi 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 2 → (2↑𝑛) = 4)
138	137	breq2d 5125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 2 → (((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) ∥ 4))
139	138	rspcev 3590	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ₀ ∧ ((od‘𝐺)‘𝑥) ∥ 4) → ∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
140	121, 119, 139	sylancr 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
141		pcprmpw2 16942	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (∃𝑛 ∈ ℕ₀ ((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))))
142	81, 124, 141	sylancr 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) = ((od‘𝐺)‘𝑥))
145		2cn 12316	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 ∈ ℂ
146		exp1 14103	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5126	. . . . . . . . . . . . . . . . . . . . . . . 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 11208	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ
153	126	nn0red 12566	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ)
154		ltnle 11289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℝ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
155	152, 153, 154	sylancr 598	. . . . . . . . . . . . . . . . . . . . . 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 12654	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℕ₀ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ₀) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
158	64, 126, 157	sylancr 598	. . . . . . . . . . . . . . . . . . . . 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 5150	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥)))
161		eluz2 12868	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
162	122, 127, 160, 161	syl3anbrc 1360	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ_≥‘2))
163		dvdsexp 16386	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℤ ∧ 2 ∈ ℕ₀ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ_≥‘2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
164	96, 121, 162, 163	mp3an12i 1491	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
165	120, 164	eqbrtrrid 5151	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
166	165, 143	breqtrrd 5143	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ ((od‘𝐺)‘𝑥))
167		dvdseq 16372	. . . . . . . . . . . . . . 15 ⊢ (((((od‘𝐺)‘𝑥) ∈ ℕ₀ ∧ 4 ∈ ℕ₀) ∧ (((od‘𝐺)‘𝑥) ∥ 4 ∧ 4 ∥ ((od‘𝐺)‘𝑥))) → ((od‘𝐺)‘𝑥) = 4)
168	109, 111, 119, 166, 167	syl22anc 851	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = 4)
169	168, 118	eqtr4d 2807	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (♯‘𝐵))
170	1, 98, 106, 107, 169	iscygodd 19958	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ CycGrp)
171	170, 76	syl 18	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Abel)
172	171	rexlimdvaa 3173	. . . . . . . . . 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 417	. . . . . . 7 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 4 → 𝐺 ∈ Abel))
176	94, 175	jaod 872	. . . . . 6 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4) → 𝐺 ∈ Abel))
177	42, 176	biimtrid 245	. . . . 5 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^5) → 𝐺 ∈ Abel))
178		id 23	. . . . . . 7 ⊢ ((♯‘𝐵) = 5 → (♯‘𝐵) = 5)
179		5prm 17168	. . . . . . 7 ⊢ 5 ∈ ℙ
180	178, 179	eqeltrdi 2877	. . . . . 6 ⊢ ((♯‘𝐵) = 5 → (♯‘𝐵) ∈ ℙ)
181	180, 85	syl5 35	. . . . 5 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 5 → 𝐺 ∈ Abel))
182	177, 181	jaod 872	. . . 4 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5) → 𝐺 ∈ Abel))
183	34, 182	biimtrid 245	. . 3 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^6) → 𝐺 ∈ Abel))
184	183	imp 411	. 2 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^6)) → 𝐺 ∈ Abel)
185	26, 184	syldan 602	1 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐺 ∈ Abel)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 Vcvv 3463 ∅c0 4294 {csn 4594 class class class wbr 5113 ‘cfv 6537 (class class class)co 7411 ωcom 7862 1_oc1o 8446 ≈ cen 8940 Fincfn 8943 ℂcc 11098 ℝcr 11099 1c1 11101 + caddc 11103 +∞cpnf 11240 ℝ^*cxr 11242 < clt 11243 ≤ cle 11244 ℕcn 12233 2c2 12295 3c3 12296 4c4 12297 5c5 12298 6c6 12299 ℕ₀cn0 12504 ℤcz 12591 ℤ_≥cuz 12862 ..^cfzo 13682 ↑cexp 14097 ♯chash 14366 ∥ cdvds 16310 ℙcprime 16729 pCnt cpc 16896 Basecbs 17269 Grpcgrp 19000 odcod 19594 gExcgex 19595 Abelcabl 19851 CycGrpccyg 19947

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9610 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-pre-sup 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-disj 5081 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-2o 8454 df-oadd 8457 df-omul 8458 df-er 8694 df-ec 8696 df-qs 8700 df-map 8826 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-sup 9402 df-inf 9403 df-oi 9472 df-dju 9887 df-card 9925 df-acn 9928 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12505 df-z 12592 df-dec 12712 df-uz 12863 df-q 12973 df-rp 13017 df-fz 13536 df-fzo 13683 df-fl 13825 df-mod 13903 df-seq 14038 df-exp 14098 df-hash 14367 df-cj 15150 df-re 15151 df-im 15152 df-sqrt 15286 df-abs 15287 df-clim 15539 df-sum 15738 df-dvds 16311 df-gcd 16553 df-prm 16730 df-pc 16897 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-0g 17494 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-grp 19003 df-minusg 19004 df-sbg 19005 df-mulg 19134 df-subg 19189 df-eqg 19191 df-od 19598 df-gex 19599 df-cmn 19852 df-abl 19853 df-cyg 19948

This theorem is referenced by: pgrple2abl 49030

W3C validator