Theorem lt6abl 19937

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 19006	. . . . . 6 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
3	2	adantr 480	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ≠ ∅)
4		6re 12383	. . . . . . . 8 ⊢ 6 ∈ ℝ
5		rexr 11336	. . . . . . . 8 ⊢ (6 ∈ ℝ → 6 ∈ ℝ*)
6		pnfnlt 13191	. . . . . . . 8 ⊢ (6 ∈ ℝ* → ¬ +∞ < 6)
7	4, 5, 6	mp2b 10	. . . . . . 7 ⊢ ¬ +∞ < 6
8	1	fvexi 6934	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
9	8	a1i 11	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → 𝐵 ∈ V)
10		hashinf 14384	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
11	9, 10	sylan 579	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
12	11	breq1d 5176	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 ↔ +∞ < 6))
13	12	biimpd 229	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 → +∞ < 6))
14	13	impancom 451	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (¬ 𝐵 ∈ Fin → +∞ < 6))
15	7, 14	mt3i 149	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ∈ Fin)
16		hashnncl 14415	. . . . . 6 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
17	15, 16	syl 17	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
18	3, 17	mpbird 257	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ ℕ)
19		nnuz 12946	. . . 4 ⊢ ℕ = (ℤ≥‘1)
20	18, 19	eleqtrdi 2854	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (ℤ≥‘1))
21		6nn 12382	. . . . 5 ⊢ 6 ∈ ℕ
22	21	nnzi 12667	. . . 4 ⊢ 6 ∈ ℤ
23	22	a1i 11	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 6 ∈ ℤ)
24		simpr 484	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) < 6)
25		elfzo2 13719	. . 3 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ ((♯‘𝐵) ∈ (ℤ≥‘1) ∧ 6 ∈ ℤ ∧ (♯‘𝐵) < 6))
26	20, 23, 24, 25	syl3anbrc 1343	. 2 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (1..^6))
27		df-6 12360	. . . . . . 7 ⊢ 6 = (5 + 1)
28	27	oveq2i 7459	. . . . . 6 ⊢ (1..^6) = (1..^(5 + 1))
29	28	eleq2i 2836	. . . . 5 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ (♯‘𝐵) ∈ (1..^(5 + 1)))
30		5nn 12379	. . . . . . 7 ⊢ 5 ∈ ℕ
31	30, 19	eleqtri 2842	. . . . . 6 ⊢ 5 ∈ (ℤ≥‘1)
32		fzosplitsni 13828	. . . . . 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 12359	. . . . . . . . 9 ⊢ 5 = (4 + 1)
36	35	oveq2i 7459	. . . . . . . 8 ⊢ (1..^5) = (1..^(4 + 1))
37	36	eleq2i 2836	. . . . . . 7 ⊢ ((♯‘𝐵) ∈ (1..^5) ↔ (♯‘𝐵) ∈ (1..^(4 + 1)))
38		4nn 12376	. . . . . . . . 9 ⊢ 4 ∈ ℕ
39	38, 19	eleqtri 2842	. . . . . . . 8 ⊢ 4 ∈ (ℤ≥‘1)
40		fzosplitsni 13828	. . . . . . . 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 12358	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
44	43	oveq2i 7459	. . . . . . . . . 10 ⊢ (1..^4) = (1..^(3 + 1))
45	44	eleq2i 2836	. . . . . . . . 9 ⊢ ((♯‘𝐵) ∈ (1..^4) ↔ (♯‘𝐵) ∈ (1..^(3 + 1)))
46		3nn 12372	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
47	46, 19	eleqtri 2842	. . . . . . . . . 10 ⊢ 3 ∈ (ℤ≥‘1)
48		fzosplitsni 13828	. . . . . . . . . 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 12357	. . . . . . . . . . . . 13 ⊢ 3 = (2 + 1)
52	51	oveq2i 7459	. . . . . . . . . . . 12 ⊢ (1..^3) = (1..^(2 + 1))
53	52	eleq2i 2836	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) ∈ (1..^3) ↔ (♯‘𝐵) ∈ (1..^(2 + 1)))
54		2eluzge1 12959	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ≥‘1)
55		fzosplitsni 13828	. . . . . . . . . . . 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 4665	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝐵) ∈ {1} → (♯‘𝐵) = 1)
59		fzo12sn 13799	. . . . . . . . . . . . . . . . 17 ⊢ (1..^2) = {1}
60	58, 59	eleq2s 2862	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐵) ∈ (1..^2) → (♯‘𝐵) = 1)
61	60	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = 1)
62		hash1 14453	. . . . . . . . . . . . . . 15 ⊢ (♯‘1o) = 1
63	61, 62	eqtr4di 2798	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = (♯‘1o))
64		1nn0 12569	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ0
65	61, 64	eqeltrdi 2852	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) ∈ ℕ0)
66		hashclb 14407	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0))
67	8, 66	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0)
68	65, 67	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ∈ Fin)
69		1onn 8696	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ ω
70		nnfi 9233	. . . . . . . . . . . . . . . 16 ⊢ (1o ∈ ω → 1o ∈ Fin)
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 1o ∈ Fin
72		hashen 14396	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ 1o ∈ Fin) → ((♯‘𝐵) = (♯‘1o) ↔ 𝐵 ≈ 1o))
73	68, 71, 72	sylancl 585	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → ((♯‘𝐵) = (♯‘1o) ↔ 𝐵 ≈ 1o))
74	63, 73	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ≈ 1o)
75	1	0cyg 19935	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1o) → 𝐺 ∈ CycGrp)
76		cygabl 19933	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel)
77	75, 76	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1o) → 𝐺 ∈ Abel)
78	74, 77	syldan 590	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐺 ∈ Abel)
79	78	ex 412	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^2) → 𝐺 ∈ Abel))
80		id 22	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) = 2 → (♯‘𝐵) = 2)
81		2prm 16739	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℙ
82	80, 81	eqeltrdi 2852	. . . . . . . . . . . 12 ⊢ ((♯‘𝐵) = 2 → (♯‘𝐵) ∈ ℙ)
83	1	prmcyg 19936	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ CycGrp)
84	83, 76	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ Abel)
85	84	ex 412	. . . . . . . . . . . 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 242	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^3) → 𝐺 ∈ Abel))
89		id 22	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) = 3 → (♯‘𝐵) = 3)
90		3prm 16741	. . . . . . . . . . 11 ⊢ 3 ∈ ℙ
91	89, 90	eqeltrdi 2852	. . . . . . . . . 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 242	. . . . . . 7 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^4) → 𝐺 ∈ Abel))
95		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Grp)
96		2z 12675	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
97		eqid 2740	. . . . . . . . . . . 12 ⊢ (gEx‘𝐺) = (gEx‘𝐺)
98		eqid 2740	. . . . . . . . . . . 12 ⊢ (od‘𝐺) = (od‘𝐺)
99	1, 97, 98	gexdvds2 19627	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 2 ∈ ℤ) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
100	95, 96, 99	sylancl 585	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
101	1, 97	gex2abl 19893	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (gEx‘𝐺) ∥ 2) → 𝐺 ∈ Abel)
102	101	ex 412	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
103	102	adantr 480	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
104	100, 103	sylbird 260	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
105		rexnal 3106	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 ↔ ¬ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2)
106	95	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Grp)
107		simprl 770	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝑥 ∈ 𝐵)
108	1, 98	odcl 19578	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐵 → ((od‘𝐺)‘𝑥) ∈ ℕ0)
109	108	ad2antrl 727	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
110		4nn0 12572	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ0
111	110	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∈ ℕ0)
112		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) = 4)
113	112, 110	eqeltrdi 2852	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) ∈ ℕ0)
114	113, 67	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐵 ∈ Fin)
115	114	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐵 ∈ Fin)
116	1, 98	oddvds2 19608	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
117	106, 115, 107, 116	syl3anc 1371	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
118	112	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (♯‘𝐵) = 4)
119	117, 118	breqtrd 5192	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ 4)
120		sq2 14246	. . . . . . . . . . . . . . . . 17 ⊢ (2↑2) = 4
121		2nn0 12570	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
122	96	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ∈ ℤ)
123	1, 98	odcl2 19607	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ)
124	106, 115, 107, 123	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ)
125		pccl 16896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0)
126	81, 124, 125	sylancr 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0)
127	126	nn0zd 12665	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ)
128		df-2 12356	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
129		simprr 772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ ((od‘𝐺)‘𝑥) ∥ 2)
130		dvdsexp 16376	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0 ∧ 1 ∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥)))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1))
131	130	3expia 1121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0) → (1 ∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
132	96, 126, 131	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
133		1z 12673	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℤ
134		eluz 12917	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 1 ∈ ℤ) → (1 ∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
135	127, 133, 134	sylancl 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
136		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 2 → (2↑𝑛) = (2↑2))
137	136, 120	eqtrdi 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 2 → (2↑𝑛) = 4)
138	137	breq2d 5178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 2 → (((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) ∥ 4))
139	138	rspcev 3635	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ0 ∧ ((od‘𝐺)‘𝑥) ∥ 4) → ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
140	121, 119, 139	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
141		pcprmpw2 16929	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))))
142	81, 124, 141	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))))
143	140, 142	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
144	143	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) = ((od‘𝐺)‘𝑥))
145		2cn 12368	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 ∈ ℂ
146		exp1 14118	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5179	. . . . . . . . . . . . . . . . . . . . . . . 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 198	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1)
152		1re 11290	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ
153	126	nn0red 12614	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ)
154		ltnle 11369	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℝ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
155	152, 153, 154	sylancr 586	. . . . . . . . . . . . . . . . . . . . . 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 12701	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℕ0 ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
158	64, 126, 157	sylancr 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
159	156, 158	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥)))
160	128, 159	eqbrtrid 5201	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥)))
161		eluz2 12909	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
162	122, 127, 160, 161	syl3anbrc 1343	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ≥‘2))
163		dvdsexp 16376	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℤ ∧ 2 ∈ ℕ0 ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ≥‘2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
164	96, 121, 162, 163	mp3an12i 1465	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
165	120, 164	eqbrtrrid 5202	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
166	165, 143	breqtrrd 5194	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ ((od‘𝐺)‘𝑥))
167		dvdseq 16362	. . . . . . . . . . . . . . 15 ⊢ (((((od‘𝐺)‘𝑥) ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (((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 2783	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (♯‘𝐵))
170	1, 98, 106, 107, 169	iscygodd 19930	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ CycGrp)
171	170, 76	syl 17	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Abel)
172	171	rexlimdvaa 3162	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∃𝑥 ∈ 𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
173	105, 172	biimtrrid 243	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (¬ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
174	104, 173	pm2.61d 179	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Abel)
175	174	ex 412	. . . . . . 7 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 4 → 𝐺 ∈ Abel))
176	94, 175	jaod 858	. . . . . 6 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4) → 𝐺 ∈ Abel))
177	42, 176	biimtrid 242	. . . . 5 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^5) → 𝐺 ∈ Abel))
178		id 22	. . . . . . 7 ⊢ ((♯‘𝐵) = 5 → (♯‘𝐵) = 5)
179		5prm 17156	. . . . . . 7 ⊢ 5 ∈ ℙ
180	178, 179	eqeltrdi 2852	. . . . . 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 242	. . 3 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^6) → 𝐺 ∈ Abel))
184	183	imp 406	. 2 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^6)) → 𝐺 ∈ Abel)
185	26, 184	syldan 590	1 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐺 ∈ Abel)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  Vcvv 3488  ∅c0 4352  {csn 4648   class class class wbr 5166  ‘cfv 6573  (class class class)co 7448  ωcom 7903  1_oc1o 8515   ≈ cen 9000  Fincfn 9003  ℂcc 11182  ℝcr 11183  1c1 11185   + caddc 11187  +∞cpnf 11321  ℝ^*cxr 11323   < clt 11324   ≤ cle 11325  ℕcn 12293  2c2 12348  3c3 12349  4c4 12350  5c5 12351  6c6 12352  ℕ₀cn0 12553  ℤcz 12639  ℤ_≥cuz 12903  ..^cfzo 13711  ↑cexp 14112  ♯chash 14379   ∥ cdvds 16302  ℙcprime 16718   pCnt cpc 16883  Basecbs 17258  Grpcgrp 18973  odcod 19566  gExcgex 19567  Abelcabl 19823  CycGrpccyg 19919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-disj 5134  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-isom 6582  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-oadd 8526  df-omul 8527  df-er 8763  df-ec 8765  df-qs 8769  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-sup 9511  df-inf 9512  df-oi 9579  df-dju 9970  df-card 10008  df-acn 10011  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361  df-8 12362  df-9 12363  df-n0 12554  df-z 12640  df-dec 12759  df-uz 12904  df-q 13014  df-rp 13058  df-fz 13568  df-fzo 13712  df-fl 13843  df-mod 13921  df-seq 14053  df-exp 14113  df-hash 14380  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285  df-clim 15534  df-sum 15735  df-dvds 16303  df-gcd 16541  df-prm 16719  df-pc 16884  df-sets 17211  df-slot 17229  df-ndx 17241  df-base 17259  df-ress 17288  df-plusg 17324  df-0g 17501  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-grp 18976  df-minusg 18977  df-sbg 18978  df-mulg 19108  df-subg 19163  df-eqg 19165  df-od 19570  df-gex 19571  df-cmn 19824  df-abl 19825  df-cyg 19920

This theorem is referenced by:  pgrple2abl  48090