Theorem lt6abl 19083

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 18199	. . . . . 6 ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
3	2	adantr 484	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ≠ ∅)
4		6re 11764	. . . . . . . 8 ⊢ 6 ∈ ℝ
5		rexr 10725	. . . . . . . 8 ⊢ (6 ∈ ℝ → 6 ∈ ℝ*)
6		pnfnlt 12564	. . . . . . . 8 ⊢ (6 ∈ ℝ* → ¬ +∞ < 6)
7	4, 5, 6	mp2b 10	. . . . . . 7 ⊢ ¬ +∞ < 6
8	1	fvexi 6672	. . . . . . . . . . . 12 ⊢ 𝐵 ∈ V
9	8	a1i 11	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → 𝐵 ∈ V)
10		hashinf 13745	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
11	9, 10	sylan 583	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐵) = +∞)
12	11	breq1d 5042	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 ↔ +∞ < 6))
13	12	biimpd 232	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ ¬ 𝐵 ∈ Fin) → ((♯‘𝐵) < 6 → +∞ < 6))
14	13	impancom 455	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (¬ 𝐵 ∈ Fin → +∞ < 6))
15	7, 14	mt3i 151	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐵 ∈ Fin)
16		hashnncl 13777	. . . . . 6 ⊢ (𝐵 ∈ Fin → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
17	15, 16	syl 17	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → ((♯‘𝐵) ∈ ℕ ↔ 𝐵 ≠ ∅))
18	3, 17	mpbird 260	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ ℕ)
19		nnuz 12321	. . . 4 ⊢ ℕ = (ℤ≥‘1)
20	18, 19	eleqtrdi 2862	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (ℤ≥‘1))
21		6nn 11763	. . . . 5 ⊢ 6 ∈ ℕ
22	21	nnzi 12045	. . . 4 ⊢ 6 ∈ ℤ
23	22	a1i 11	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 6 ∈ ℤ)
24		simpr 488	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) < 6)
25		elfzo2 13090	. . 3 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ ((♯‘𝐵) ∈ (ℤ≥‘1) ∧ 6 ∈ ℤ ∧ (♯‘𝐵) < 6))
26	20, 23, 24, 25	syl3anbrc 1340	. 2 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → (♯‘𝐵) ∈ (1..^6))
27		df-6 11741	. . . . . . 7 ⊢ 6 = (5 + 1)
28	27	oveq2i 7161	. . . . . 6 ⊢ (1..^6) = (1..^(5 + 1))
29	28	eleq2i 2843	. . . . 5 ⊢ ((♯‘𝐵) ∈ (1..^6) ↔ (♯‘𝐵) ∈ (1..^(5 + 1)))
30		5nn 11760	. . . . . . 7 ⊢ 5 ∈ ℕ
31	30, 19	eleqtri 2850	. . . . . 6 ⊢ 5 ∈ (ℤ≥‘1)
32		fzosplitsni 13197	. . . . . 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 11740	. . . . . . . . 9 ⊢ 5 = (4 + 1)
36	35	oveq2i 7161	. . . . . . . 8 ⊢ (1..^5) = (1..^(4 + 1))
37	36	eleq2i 2843	. . . . . . 7 ⊢ ((♯‘𝐵) ∈ (1..^5) ↔ (♯‘𝐵) ∈ (1..^(4 + 1)))
38		4nn 11757	. . . . . . . . 9 ⊢ 4 ∈ ℕ
39	38, 19	eleqtri 2850	. . . . . . . 8 ⊢ 4 ∈ (ℤ≥‘1)
40		fzosplitsni 13197	. . . . . . . 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 11739	. . . . . . . . . . 11 ⊢ 4 = (3 + 1)
44	43	oveq2i 7161	. . . . . . . . . 10 ⊢ (1..^4) = (1..^(3 + 1))
45	44	eleq2i 2843	. . . . . . . . 9 ⊢ ((♯‘𝐵) ∈ (1..^4) ↔ (♯‘𝐵) ∈ (1..^(3 + 1)))
46		3nn 11753	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ
47	46, 19	eleqtri 2850	. . . . . . . . . 10 ⊢ 3 ∈ (ℤ≥‘1)
48		fzosplitsni 13197	. . . . . . . . . 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 11738	. . . . . . . . . . . . 13 ⊢ 3 = (2 + 1)
52	51	oveq2i 7161	. . . . . . . . . . . 12 ⊢ (1..^3) = (1..^(2 + 1))
53	52	eleq2i 2843	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) ∈ (1..^3) ↔ (♯‘𝐵) ∈ (1..^(2 + 1)))
54		2eluzge1 12334	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ≥‘1)
55		fzosplitsni 13197	. . . . . . . . . . . 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 4539	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝐵) ∈ {1} → (♯‘𝐵) = 1)
59		fzo12sn 13169	. . . . . . . . . . . . . . . . 17 ⊢ (1..^2) = {1}
60	58, 59	eleq2s 2870	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝐵) ∈ (1..^2) → (♯‘𝐵) = 1)
61	60	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = 1)
62		hash1 13815	. . . . . . . . . . . . . . 15 ⊢ (♯‘1o) = 1
63	61, 62	eqtr4di 2811	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) = (♯‘1o))
64		1nn0 11950	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℕ0
65	61, 64	eqeltrdi 2860	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → (♯‘𝐵) ∈ ℕ0)
66		hashclb 13769	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ V → (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0))
67	8, 66	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin ↔ (♯‘𝐵) ∈ ℕ0)
68	65, 67	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ∈ Fin)
69		1onn 8275	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ ω
70		nnfi 8750	. . . . . . . . . . . . . . . 16 ⊢ (1o ∈ ω → 1o ∈ Fin)
71	69, 70	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ 1o ∈ Fin
72		hashen 13757	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 ∈ Fin ∧ 1o ∈ Fin) → ((♯‘𝐵) = (♯‘1o) ↔ 𝐵 ≈ 1o))
73	68, 71, 72	sylancl 589	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → ((♯‘𝐵) = (♯‘1o) ↔ 𝐵 ≈ 1o))
74	63, 73	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐵 ≈ 1o)
75	1	0cyg 19081	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1o) → 𝐺 ∈ CycGrp)
76		cygabl 19078	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel)
77	75, 76	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1o) → 𝐺 ∈ Abel)
78	74, 77	syldan 594	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^2)) → 𝐺 ∈ Abel)
79	78	ex 416	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^2) → 𝐺 ∈ Abel))
80		id 22	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) = 2 → (♯‘𝐵) = 2)
81		2prm 16088	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℙ
82	80, 81	eqeltrdi 2860	. . . . . . . . . . . 12 ⊢ ((♯‘𝐵) = 2 → (♯‘𝐵) ∈ ℙ)
83	1	prmcyg 19082	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ CycGrp)
84	83, 76	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ ℙ) → 𝐺 ∈ Abel)
85	84	ex 416	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ ℙ → 𝐺 ∈ Abel))
86	82, 85	syl5 34	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 2 → 𝐺 ∈ Abel))
87	79, 86	jaod 856	. . . . . . . . . 10 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^2) ∨ (♯‘𝐵) = 2) → 𝐺 ∈ Abel))
88	57, 87	syl5bi 245	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^3) → 𝐺 ∈ Abel))
89		id 22	. . . . . . . . . . 11 ⊢ ((♯‘𝐵) = 3 → (♯‘𝐵) = 3)
90		3prm 16090	. . . . . . . . . . 11 ⊢ 3 ∈ ℙ
91	89, 90	eqeltrdi 2860	. . . . . . . . . 10 ⊢ ((♯‘𝐵) = 3 → (♯‘𝐵) ∈ ℙ)
92	91, 85	syl5 34	. . . . . . . . 9 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 3 → 𝐺 ∈ Abel))
93	88, 92	jaod 856	. . . . . . . 8 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^3) ∨ (♯‘𝐵) = 3) → 𝐺 ∈ Abel))
94	50, 93	syl5bi 245	. . . . . . 7 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^4) → 𝐺 ∈ Abel))
95		simpl 486	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Grp)
96		2z 12053	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
97		eqid 2758	. . . . . . . . . . . 12 ⊢ (gEx‘𝐺) = (gEx‘𝐺)
98		eqid 2758	. . . . . . . . . . . 12 ⊢ (od‘𝐺) = (od‘𝐺)
99	1, 97, 98	gexdvds2 18777	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 2 ∈ ℤ) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
100	95, 96, 99	sylancl 589	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 ↔ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2))
101	1, 97	gex2abl 19039	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (gEx‘𝐺) ∥ 2) → 𝐺 ∈ Abel)
102	101	ex 416	. . . . . . . . . . 11 ⊢ (𝐺 ∈ Grp → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
103	102	adantr 484	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → ((gEx‘𝐺) ∥ 2 → 𝐺 ∈ Abel))
104	100, 103	sylbird 263	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
105		rexnal 3165	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 ↔ ¬ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2)
106	95	adantr 484	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Grp)
107		simprl 770	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝑥 ∈ 𝐵)
108	1, 98	odcl 18731	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐵 → ((od‘𝐺)‘𝑥) ∈ ℕ0)
109	108	ad2antrl 727	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
110		4nn0 11953	. . . . . . . . . . . . . . . 16 ⊢ 4 ∈ ℕ0
111	110	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∈ ℕ0)
112		simpr 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) = 4)
113	112, 110	eqeltrdi 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (♯‘𝐵) ∈ ℕ0)
114	113, 67	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐵 ∈ Fin)
115	114	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐵 ∈ Fin)
116	1, 98	oddvds2 18760	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
117	106, 115, 107, 116	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
118	112	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (♯‘𝐵) = 4)
119	117, 118	breqtrd 5058	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∥ 4)
120		sq2 13610	. . . . . . . . . . . . . . . . 17 ⊢ (2↑2) = 4
121		2nn0 11951	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ0
122	96	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ∈ ℤ)
123	1, 98	odcl2 18759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ)
124	106, 115, 107, 123	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) ∈ ℕ)
125		pccl 16241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0)
126	81, 124, 125	sylancr 590	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0)
127	126	nn0zd 12124	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ)
128		df-2 11737	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 = (1 + 1)
129		simprr 772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ¬ ((od‘𝐺)‘𝑥) ∥ 2)
130		dvdsexp 15729	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0 ∧ 1 ∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥)))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1))
131	130	3expia 1118	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0) → (1 ∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
132	96, 126, 131	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) ∥ (2↑1)))
133		1z 12051	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 1 ∈ ℤ
134		eluz 12296	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 1 ∈ ℤ) → (1 ∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
135	127, 133, 134	sylancl 589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (1 ∈ (ℤ≥‘(2 pCnt ((od‘𝐺)‘𝑥))) ↔ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
136		oveq2 7158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑛 = 2 → (2↑𝑛) = (2↑2))
137	136, 120	eqtrdi 2809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑛 = 2 → (2↑𝑛) = 4)
138	137	breq2d 5044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 2 → (((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) ∥ 4))
139	138	rspcev 3541	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℕ0 ∧ ((od‘𝐺)‘𝑥) ∥ 4) → ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
140	121, 119, 139	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛))
141		pcprmpw2 16273	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((2 ∈ ℙ ∧ ((od‘𝐺)‘𝑥) ∈ ℕ) → (∃𝑛 ∈ ℕ0 ((od‘𝐺)‘𝑥) ∥ (2↑𝑛) ↔ ((od‘𝐺)‘𝑥) = (2↑(2 pCnt ((od‘𝐺)‘𝑥)))))
142	81, 124, 141	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (∃𝑛 ∈ ℕ0 ((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 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑(2 pCnt ((od‘𝐺)‘𝑥))) = ((od‘𝐺)‘𝑥))
145		2cn 11749	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 ∈ ℂ
146		exp1 13485	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5045	. . . . . . . . . . . . . . . . . . . . . . . 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 10679	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℝ
153	126	nn0red 11995	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ)
154		ltnle 10758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℝ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℝ) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ ¬ (2 pCnt ((od‘𝐺)‘𝑥)) ≤ 1))
155	152, 153, 154	sylancr 590	. . . . . . . . . . . . . . . . . . . . . 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 12079	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℕ0 ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℕ0) → (1 < (2 pCnt ((od‘𝐺)‘𝑥)) ↔ (1 + 1) ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
158	64, 126, 157	sylancr 590	. . . . . . . . . . . . . . . . . . . . 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 5067	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥)))
161		eluz2 12288	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ ℤ ∧ 2 ≤ (2 pCnt ((od‘𝐺)‘𝑥))))
162	122, 127, 160, 161	syl3anbrc 1340	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ≥‘2))
163		dvdsexp 15729	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℤ ∧ 2 ∈ ℕ0 ∧ (2 pCnt ((od‘𝐺)‘𝑥)) ∈ (ℤ≥‘2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
164	96, 121, 162, 163	mp3an12i 1462	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → (2↑2) ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
165	120, 164	eqbrtrrid 5068	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ (2↑(2 pCnt ((od‘𝐺)‘𝑥))))
166	165, 143	breqtrrd 5060	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 4 ∥ ((od‘𝐺)‘𝑥))
167		dvdseq 15715	. . . . . . . . . . . . . . 15 ⊢ (((((od‘𝐺)‘𝑥) ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (((od‘𝐺)‘𝑥) ∥ 4 ∧ 4 ∥ ((od‘𝐺)‘𝑥))) → ((od‘𝐺)‘𝑥) = 4)
168	109, 111, 119, 166, 167	syl22anc 837	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = 4)
169	168, 118	eqtr4d 2796	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → ((od‘𝐺)‘𝑥) = (♯‘𝐵))
170	1, 98, 106, 107, 169	iscygodd 19075	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ CycGrp)
171	170, 76	syl 17	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) ∧ (𝑥 ∈ 𝐵 ∧ ¬ ((od‘𝐺)‘𝑥) ∥ 2)) → 𝐺 ∈ Abel)
172	171	rexlimdvaa 3209	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (∃𝑥 ∈ 𝐵 ¬ ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
173	105, 172	syl5bir 246	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → (¬ ∀𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) ∥ 2 → 𝐺 ∈ Abel))
174	104, 173	pm2.61d 182	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) = 4) → 𝐺 ∈ Abel)
175	174	ex 416	. . . . . . 7 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 4 → 𝐺 ∈ Abel))
176	94, 175	jaod 856	. . . . . 6 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^4) ∨ (♯‘𝐵) = 4) → 𝐺 ∈ Abel))
177	42, 176	syl5bi 245	. . . . 5 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^5) → 𝐺 ∈ Abel))
178		id 22	. . . . . . 7 ⊢ ((♯‘𝐵) = 5 → (♯‘𝐵) = 5)
179		5prm 16500	. . . . . . 7 ⊢ 5 ∈ ℙ
180	178, 179	eqeltrdi 2860	. . . . . 6 ⊢ ((♯‘𝐵) = 5 → (♯‘𝐵) ∈ ℙ)
181	180, 85	syl5 34	. . . . 5 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) = 5 → 𝐺 ∈ Abel))
182	177, 181	jaod 856	. . . 4 ⊢ (𝐺 ∈ Grp → (((♯‘𝐵) ∈ (1..^5) ∨ (♯‘𝐵) = 5) → 𝐺 ∈ Abel))
183	34, 182	syl5bi 245	. . 3 ⊢ (𝐺 ∈ Grp → ((♯‘𝐵) ∈ (1..^6) → 𝐺 ∈ Abel))
184	183	imp 410	. 2 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) ∈ (1..^6)) → 𝐺 ∈ Abel)
185	26, 184	syldan 594	1 ⊢ ((𝐺 ∈ Grp ∧ (♯‘𝐵) < 6) → 𝐺 ∈ Abel)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  Vcvv 3409  ∅c0 4225  {csn 4522   class class class wbr 5032  ‘cfv 6335  (class class class)co 7150  ωcom 7579  1_oc1o 8105   ≈ cen 8524  Fincfn 8527  ℂcc 10573  ℝcr 10574  1c1 10576   + caddc 10578  +∞cpnf 10710  ℝ^*cxr 10712   < clt 10713   ≤ cle 10714  ℕcn 11674  2c2 11729  3c3 11730  4c4 11731  5c5 11732  6c6 11733  ℕ₀cn0 11934  ℤcz 12020  ℤ_≥cuz 12282  ..^cfzo 13082  ↑cexp 13479  ♯chash 13740   ∥ cdvds 15655  ℙcprime 16067   pCnt cpc 16228  Basecbs 16541  Grpcgrp 18169  odcod 18719  gExcgex 18720  Abelcabl 18974  CycGrpccyg 19064

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-pre-sup 10653

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-disj 4998  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-se 5484  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-isom 6344  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-2o 8113  df-oadd 8116  df-omul 8117  df-er 8299  df-ec 8301  df-qs 8305  df-map 8418  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-sup 8939  df-inf 8940  df-oi 9007  df-dju 9363  df-card 9401  df-acn 9404  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-div 11336  df-nn 11675  df-2 11737  df-3 11738  df-4 11739  df-5 11740  df-6 11741  df-7 11742  df-8 11743  df-9 11744  df-n0 11935  df-z 12021  df-dec 12138  df-uz 12283  df-q 12389  df-rp 12431  df-fz 12940  df-fzo 13083  df-fl 13211  df-mod 13287  df-seq 13419  df-exp 13480  df-hash 13741  df-cj 14506  df-re 14507  df-im 14508  df-sqrt 14642  df-abs 14643  df-clim 14893  df-sum 15091  df-dvds 15656  df-gcd 15894  df-prm 16068  df-pc 16229  df-ndx 16544  df-slot 16545  df-base 16547  df-sets 16548  df-ress 16549  df-plusg 16636  df-0g 16773  df-mgm 17918  df-sgrp 17967  df-mnd 17978  df-grp 18172  df-minusg 18173  df-sbg 18174  df-mulg 18292  df-subg 18343  df-eqg 18345  df-od 18723  df-gex 18724  df-cmn 18975  df-abl 18976  df-cyg 19065

This theorem is referenced by:  pgrple2abl  45134