Theorem unitscyglem4 42854

Description: Lemma for unitscyg . (Contributed by metakunt, 14-Jul-2025.)

Hypotheses

Ref	Expression
unitscyglem1.1	⊢ 𝐵 = (Base‘𝐺)
unitscyglem1.2	⊢ ↑ = (.g‘𝐺)
unitscyglem1.3	⊢ (𝜑 → 𝐺 ∈ Grp)
unitscyglem1.4	⊢ (𝜑 → 𝐵 ∈ Fin)
unitscyglem1.5	⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)
unitscyglem4.1	⊢ (𝜑 → 𝐷 ∈ ℕ)
unitscyglem4.2	⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵))

Assertion

Ref	Expression
unitscyglem4	⊢ (𝜑 → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))

Distinct variable groups:   𝑥, ↑ ,𝑛   𝑥,𝐵,𝑛   𝑦,𝐵,𝑥   𝑥,𝐷,𝑦   𝑥,𝐺,𝑛   𝑦,𝐺   𝜑,𝑥,𝑛

Allowed substitution hints:   𝜑(𝑦)   𝐷(𝑛)   ↑ (𝑦)

Proof of Theorem unitscyglem4

Dummy variables 𝑙 𝑎 𝑘 𝑚 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfcv 2931	. . . . . 6 ⊢ Ⅎ𝑦𝐵
2		nfcv 2931	. . . . . 6 ⊢ Ⅎ𝑥𝐵
3		nfv 1941	. . . . . 6 ⊢ Ⅎ𝑥((od‘𝐺)‘𝑦) = 𝐷
4		nfv 1941	. . . . . 6 ⊢ Ⅎ𝑦((od‘𝐺)‘𝑥) = 𝐷
5		fveqeq2 6891	. . . . . 6 ⊢ (𝑦 = 𝑥 → (((od‘𝐺)‘𝑦) = 𝐷 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
6	1, 2, 3, 4, 5	cbvrabw 3458	. . . . 5 ⊢ {𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}
7	6	fveq2i 6885	. . . 4 ⊢ (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
8	7	a1i 11	. . 3 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))
9		unitscyglem4.2	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵))
10	9	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → 𝐷 ∥ (♯‘𝐵))
11	10	ex 417	. . . . . 6 ⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → 𝐷 ∥ (♯‘𝐵)))
12	11	ancrd 560	. . . . 5 ⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)))
13	12	imdistani 578	. . . 4 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (𝜑 ∧ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)))
14		breq1 5116	. . . . . . . 8 ⊢ (𝑚 = 𝐷 → (𝑚 ∥ (♯‘𝐵) ↔ 𝐷 ∥ (♯‘𝐵)))
15		eqeq2 2781	. . . . . . . . . 10 ⊢ (𝑚 = 𝐷 → (((od‘𝐺)‘𝑥) = 𝑚 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
16	15	rabbidv 3430	. . . . . . . . 9 ⊢ (𝑚 = 𝐷 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
17	16	neeq1d 3023	. . . . . . . 8 ⊢ (𝑚 = 𝐷 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))
18	14, 17	anbi12d 643	. . . . . . 7 ⊢ (𝑚 = 𝐷 → ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) ↔ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)))
19	16	fveq2d 6886	. . . . . . . 8 ⊢ (𝑚 = 𝐷 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))
20		fveq2 6882	. . . . . . . 8 ⊢ (𝑚 = 𝐷 → (ϕ‘𝑚) = (ϕ‘𝐷))
21	19, 20	eqeq12d 2785	. . . . . . 7 ⊢ (𝑚 = 𝐷 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)))
22	18, 21	imbi12d 347	. . . . . 6 ⊢ (𝑚 = 𝐷 → (((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)) ↔ ((𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))))
23		unitscyglem1.1	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
24		unitscyglem1.2	. . . . . . 7 ⊢ ↑ = (.g‘𝐺)
25		unitscyglem1.3	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ Grp)
26		unitscyglem1.4	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ Fin)
27		unitscyglem1.5	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0g‘𝐺)}) ≤ 𝑛)
28	23, 24, 25, 26, 27	unitscyglem3 42853	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)))
29		unitscyglem4.1	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ ℕ)
30	22, 28, 29	rspcdva 3591	. . . . 5 ⊢ (𝜑 → ((𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)))
31	30	imp 411	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))
32	13, 31	syl 18	. . 3 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))
33	8, 32	eqtrd 2804	. 2 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
34		id 23	. . . . 5 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
35	34	necon1bi 2992	. . . 4 ⊢ (¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅)
36	35	adantl 486	. . 3 ⊢ ((𝜑 ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅)
37	25	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 𝐺 ∈ Grp)
38	26	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 𝐵 ∈ Fin)
39	23, 37, 38	hashfingrpnn 19038	. . . . . . . . 9 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℕ)
40	23, 24, 37, 38, 39	grpods 42850	. . . . . . . 8 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)}))
41		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵))
42	41	eqcomd 2775	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → (♯‘𝐵) = (𝑙 · ((od‘𝐺)‘𝑥)))
43	42	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((♯‘𝐵) ↑ 𝑥) = ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥))
44	25	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐺 ∈ Grp)
45	44	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝐺 ∈ Grp)
46		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℤ)
47		eqid 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (od‘𝐺) = (od‘𝐺)
48		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
49	23, 47, 48	odcld 19621	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
50	49	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
51	50	nn0zd 12615	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((od‘𝐺)‘𝑥) ∈ ℤ)
52		simplr 780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝑥 ∈ 𝐵)
53	46, 51, 52	3jca 1144	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ∈ ℤ ∧ ((od‘𝐺)‘𝑥) ∈ ℤ ∧ 𝑥 ∈ 𝐵))
54	23, 24	mulgass 19176	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ (𝑙 ∈ ℤ ∧ ((od‘𝐺)‘𝑥) ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)))
55	45, 53, 54	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)))
56		eqid 2769	. . . . . . . . . . . . . . . . . . 19 ⊢ (0g‘𝐺) = (0g‘𝐺)
57	23, 47, 24, 56	odid 19607	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 → (((od‘𝐺)‘𝑥) ↑ 𝑥) = (0g‘𝐺))
58	52, 57	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (((od‘𝐺)‘𝑥) ↑ 𝑥) = (0g‘𝐺))
59	58	oveq2d 7427	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)) = (𝑙 ↑ (0g‘𝐺)))
60	23, 24, 56	mulgz 19167	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (0g‘𝐺)) = (0g‘𝐺))
61	44, 60	sylan 591	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (0g‘𝐺)) = (0g‘𝐺))
62	59, 61	eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)) = (0g‘𝐺))
63	55, 62	eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (0g‘𝐺))
64	63	adantr 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (0g‘𝐺))
65	43, 64	eqtrd 2804	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺))
66	26	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐵 ∈ Fin)
67	23, 47	oddvds2 19635	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
68	44, 66, 48, 67	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
69	49	nn0zd 12615	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℤ)
70		hashcl 14391	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
71	66, 70	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℕ0)
72	71	nn0zd 12615	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℤ)
73		divides 16311	. . . . . . . . . . . . . 14 ⊢ ((((od‘𝐺)‘𝑥) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → (((od‘𝐺)‘𝑥) ∥ (♯‘𝐵) ↔ ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)))
74	69, 72, 73	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((od‘𝐺)‘𝑥) ∥ (♯‘𝐵) ↔ ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)))
75	68, 74	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑙 ∈ ℤ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵))
76	65, 75	r19.29a 3179	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺))
77	76	rabeqcda 3434	. . . . . . . . . 10 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)} = 𝐵)
78	77	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)} = 𝐵)
79	78	fveq2d 6886	. . . . . . . 8 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)}) = (♯‘𝐵))
80	40, 79	eqtr2d 2805	. . . . . . 7 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) = Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
81		nfv 1941	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅)
82		nfcv 2931	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)})
83		fzfid 14008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (1...(♯‘𝐵)) ∈ Fin)
84		ssrab2 4042	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵))
85	84	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
86	83, 85	ssfid 9228	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin)
87	38	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝐵 ∈ Fin)
88		ssrab2 4042	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵
89	88	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
90	87, 89	ssfid 9228	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
91		hashcl 14391	. . . . . . . . . . . . 13 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
92	90, 91	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
93	92	nn0cnd 12566	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℂ)
94		breq1 5116	. . . . . . . . . . . 12 ⊢ (𝑎 = (♯‘𝐵) → (𝑎 ∥ (♯‘𝐵) ↔ (♯‘𝐵) ∥ (♯‘𝐵)))
95		1zzd 12624	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 1 ∈ ℤ)
96	39	nnzd 12616	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℤ)
97	39	nnge1d 12283	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 1 ≤ (♯‘𝐵))
98	39	nnred 12247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℝ)
99	98	leidd 11779	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ≤ (♯‘𝐵))
100	95, 96, 96, 97, 99	elfzd 13542	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ (1...(♯‘𝐵)))
101		iddvds 16326	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) ∈ ℤ → (♯‘𝐵) ∥ (♯‘𝐵))
102	96, 101	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∥ (♯‘𝐵))
103	94, 100, 102	elrabd 3661	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
104		eqeq2 2781	. . . . . . . . . . . . 13 ⊢ (𝑘 = (♯‘𝐵) → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = (♯‘𝐵)))
105	104	rabbidv 3430	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘𝐵) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)})
106	105	fveq2d 6886	. . . . . . . . . . 11 ⊢ (𝑘 = (♯‘𝐵) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}))
107	81, 82, 86, 93, 103, 106	fsumsplit1 15795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})))
108		ssrab2 4042	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ⊆ 𝐵
109	108	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ⊆ 𝐵)
110	38, 109	ssfid 9228	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ∈ Fin)
111		hashcl 14391	. . . . . . . . . . . . . 14 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℕ0)
112	110, 111	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℕ0)
113	112	nn0red 12565	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℝ)
114		diffi 9158	. . . . . . . . . . . . . . 15 ⊢ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ∈ Fin)
115	86, 114	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ∈ Fin)
116	38	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝐵 ∈ Fin)
117	88	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
118	116, 117	ssfid 9228	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
119	118, 91	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
120	115, 119	fsumnn0cl 15786	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
121	120	nn0red 12565	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ)
122	39	phicld 16830	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (ϕ‘(♯‘𝐵)) ∈ ℕ)
123	122	nnred 12247	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (ϕ‘(♯‘𝐵)) ∈ ℝ)
124		eldifi 4093	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
125		breq1 5116	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑘 → (𝑎 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
126	125	elrab 3659	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))
127	126	biimpi 219	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))
128		elfzelz 13551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(♯‘𝐵)) → 𝑘 ∈ ℤ)
129		elfzle1 13554	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(♯‘𝐵)) → 1 ≤ 𝑘)
130	128, 129	jca 520	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ (1...(♯‘𝐵)) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
131	130	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
132	127, 131	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
133	124, 132	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
134	133	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
135		elnnz1 12619	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
136	134, 135	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝑘 ∈ ℕ)
137		phicl 16827	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (ϕ‘𝑘) ∈ ℕ)
138	136, 137	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (ϕ‘𝑘) ∈ ℕ)
139	138	nnred 12247	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (ϕ‘𝑘) ∈ ℝ)
140	115, 139	fsumrecl 15784	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘) ∈ ℝ)
141		simplll 786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝜑)
142		simplr 780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝑧 ∈ 𝐵)
143	141, 142	jca 520	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝜑 ∧ 𝑧 ∈ 𝐵))
144		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = (♯‘𝐵))
145	143, 144	jca 520	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)))
146		fveqeq2 6891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = (((♯‘𝐵) / 𝐷) ↑ 𝑧) → (((od‘𝐺)‘𝑥) = 𝐷 ↔ ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) = 𝐷))
147	25	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐺 ∈ Grp)
148	9	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∥ (♯‘𝐵))
149	29	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℕ)
150	149	nnzd 12616	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℤ)
151	149	nnne0d 12285	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ≠ 0)
152	26	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐵 ∈ Fin)
153	152, 70	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
154	153	nn0zd 12615	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
155		dvdsval2 16312	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ∧ (♯‘𝐵) ∈ ℤ) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℤ))
156	150, 151, 154, 155	syl3anc 1396	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℤ))
157	148, 156	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℤ)
158		simplr 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝑧 ∈ 𝐵)
159	23, 24, 147, 157, 158	mulgcld 19161	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ 𝐵)
160	153	nn0cnd 12566	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ)
161	29	nncnd 12248	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐷 ∈ ℂ)
162	161	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℂ)
163	23, 147, 152	hashfingrpnn 19038	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ)
164	163	nnne0d 12285	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ≠ 0)
165	160, 160, 162, 164, 151	divdiv2d 12022	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)) = (((♯‘𝐵) · 𝐷) / (♯‘𝐵)))
166	162, 160, 164	divcan3d 11995	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) · 𝐷) / (♯‘𝐵)) = 𝐷)
167	165, 166	eqtr2d 2805	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 = ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)))
168		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = (♯‘𝐵))
169	168	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) = (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)))
170	26, 70	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ0)
171	170	nn0cnd 12566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (♯‘𝐵) ∈ ℂ)
172	29	nnne0d 12285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐷 ≠ 0)
173	171, 161, 172	divcan2d 11992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝐷 · ((♯‘𝐵) / 𝐷)) = (♯‘𝐵))
174	173	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
175	174	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
176	175	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
177	176	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)) = (((♯‘𝐵) / 𝐷) gcd (𝐷 · ((♯‘𝐵) / 𝐷))))
178		nndivdvds 16318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐵) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℕ))
179	163, 149, 178	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℕ))
180	148, 179	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℕ)
181	180	nnnn0d 12564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℕ0)
182	181, 150	gcdmultipled 16591	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (𝐷 · ((♯‘𝐵) / 𝐷))) = ((♯‘𝐵) / 𝐷))
183	177, 182	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)) = ((♯‘𝐵) / 𝐷))
184	169, 183	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) = ((♯‘𝐵) / 𝐷))
185	184	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) = (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)))
186	185	oveq2d 7427	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)) = ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))))
187	167, 186	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 = ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))))
188	168	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = ((od‘𝐺)‘𝑧))
189	23, 47, 24	odmulg 19625	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝐵 ∧ ((♯‘𝐵) / 𝐷) ∈ ℤ) → ((od‘𝐺)‘𝑧) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))))
190	147, 158, 157, 189	syl3anc 1396	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))))
191	188, 190	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))))
192	191	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))) = (♯‘𝐵))
193	157	zcnd 12700	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℂ)
194	184, 193	eqeltrd 2869	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℂ)
195	23, 47, 159	odcld 19621	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ∈ ℕ0)
196	195	nn0cnd 12566	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ∈ ℂ)
197	168, 154	eqeltrd 2869	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) ∈ ℤ)
198	168, 164	eqnetrd 3031	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) ≠ 0)
199	157, 197, 198	3jca 1144	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ≠ 0))
200		gcd2n0cl 16566	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((♯‘𝐵) / 𝐷) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ≠ 0) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℕ)
201	199, 200	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℕ)
202	201	nnne0d 12285	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ≠ 0)
203	160, 194, 196, 202	divmuld 12012	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) = ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ↔ ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))) = (♯‘𝐵)))
204	192, 203	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) = ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)))
205	187, 204	eqtr2d 2805	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) = 𝐷)
206	146, 159, 205	elrabd 3661	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
207		ne0i 4302	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
208	206, 207	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
209	145, 208	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
210		rabn0 4353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = (♯‘𝐵))
211		nfv 1941	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑧((od‘𝐺)‘𝑥) = (♯‘𝐵)
212		nfv 1941	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥((od‘𝐺)‘𝑧) = (♯‘𝐵)
213		fveqeq2 6891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑧 → (((od‘𝐺)‘𝑥) = (♯‘𝐵) ↔ ((od‘𝐺)‘𝑧) = (♯‘𝐵)))
214	211, 212, 213	cbvrexw 3314	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = (♯‘𝐵) ↔ ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
215	210, 214	bitri 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ ↔ ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
216	215	bilani 509	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) → ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
217	209, 216	r19.29a 3179	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
218	217	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))
219	218	necon4d 2988	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} = ∅))
220	219	imp 411	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} = ∅)
221	220	fveq2d 6886	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) = (♯‘∅))
222		hash0 14402	. . . . . . . . . . . . . . 15 ⊢ (♯‘∅) = 0
223	222	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘∅) = 0)
224	221, 223	eqtrd 2804	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) = 0)
225	122	nngt0d 12284	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 0 < (ϕ‘(♯‘𝐵)))
226	224, 225	eqbrtrd 5137	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) < (ϕ‘(♯‘𝐵)))
227		eldif 3923	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ↔ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}))
228	227	bilani 509	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}))
229		breq1 5116	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑧 → (𝑎 ∥ (♯‘𝐵) ↔ 𝑧 ∥ (♯‘𝐵)))
230	229	elrab 3659	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
231	230	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
232	231	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
233		velsn 4610	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ {(♯‘𝐵)} ↔ 𝑧 = (♯‘𝐵))
234	233	bicomi 227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = (♯‘𝐵) ↔ 𝑧 ∈ {(♯‘𝐵)})
235	234	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = (♯‘𝐵) → 𝑧 ∈ {(♯‘𝐵)})
236	235	necon3bi 2990	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑧 ∈ {(♯‘𝐵)} → 𝑧 ≠ (♯‘𝐵))
237	236	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ≠ (♯‘𝐵))
238	232, 237	jca 520	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)))
239	238	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)))
240		1zzd 12624	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 1 ∈ ℤ)
241	26	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝐵 ∈ Fin)
242	241, 70	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℕ0)
243	242	nn0zd 12615	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℤ)
244	243, 240	zsubcld 12704	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → ((♯‘𝐵) − 1) ∈ ℤ)
245		elfzelz 13551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (1...(♯‘𝐵)) → 𝑧 ∈ ℤ)
246	245	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ∈ ℤ)
247	246	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ ℤ)
248	247	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ ℤ)
249		elfzle1 13554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (1...(♯‘𝐵)) → 1 ≤ 𝑧)
250	249	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) → 1 ≤ 𝑧)
251	250	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 1 ≤ 𝑧)
252	251	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 1 ≤ 𝑧)
253		elfzle2 13555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ (1...(♯‘𝐵)) → 𝑧 ≤ (♯‘𝐵))
254	253	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ≤ (♯‘𝐵))
255	254	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ≤ (♯‘𝐵))
256	255	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≤ (♯‘𝐵))
257		simprr 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≠ (♯‘𝐵))
258	257	necomd 3019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ≠ 𝑧)
259	256, 258	jca 520	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 ≤ (♯‘𝐵) ∧ (♯‘𝐵) ≠ 𝑧))
260	248	zred 12699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ ℝ)
261	242	nn0red 12565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℝ)
262	260, 261	ltlend 11354	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 < (♯‘𝐵) ↔ (𝑧 ≤ (♯‘𝐵) ∧ (♯‘𝐵) ≠ 𝑧)))
263	259, 262	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 < (♯‘𝐵))
264	248, 243	zltlem1d 12647	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 < (♯‘𝐵) ↔ 𝑧 ≤ ((♯‘𝐵) − 1)))
265	263, 264	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≤ ((♯‘𝐵) − 1))
266	240, 244, 248, 252, 265	elfzd 13542	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ (1...((♯‘𝐵) − 1)))
267		simprlr 791	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∥ (♯‘𝐵))
268	229, 266, 267	elrabd 3661	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
269	268	ex 417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
270	269	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
271	239, 270	mpd 16	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
272	271	ex 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
273	272	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
274	228, 273	mpd 16	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
275	274	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
276	275	ssrdv 3951	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ⊆ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
277		1zzd 12624	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ∈ ℤ)
278	170	nn0zd 12615	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (♯‘𝐵) ∈ ℤ)
279	278	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → (♯‘𝐵) ∈ ℤ)
280		elfzelz 13551	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ∈ ℤ)
281	280	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ ℤ)
282		elfzle1 13554	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 1 ≤ 𝑧)
283	282	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ≤ 𝑧)
284	281	zred 12699	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ ℝ)
285	279	zred 12699	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → (♯‘𝐵) ∈ ℝ)
286		1red 11208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ∈ ℝ)
287	285, 286	resubcld 11641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → ((♯‘𝐵) − 1) ∈ ℝ)
288		elfzle2 13555	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ≤ ((♯‘𝐵) − 1))
289	288	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ≤ ((♯‘𝐵) − 1))
290	285	lem1d 12147	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → ((♯‘𝐵) − 1) ≤ (♯‘𝐵))
291	284, 287, 285, 289, 290	letrd 11366	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ≤ (♯‘𝐵))
292	277, 279, 281, 283, 291	elfzd 13542	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ (1...(♯‘𝐵)))
293	292	ex 417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ∈ (1...(♯‘𝐵))))
294	293	ssrdv 3951	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1...((♯‘𝐵) − 1)) ⊆ (1...(♯‘𝐵)))
295		rabss2 4039	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1...((♯‘𝐵) − 1)) ⊆ (1...(♯‘𝐵)) → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
296	294, 295	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
297	296	sseld 3944	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → 𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}))
298	297	imp 411	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
299	170	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
300	299	nn0red 12565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ∈ ℝ)
301	300	leidd 11779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ≤ (♯‘𝐵))
302		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 = (♯‘𝐵))
303	302	eqcomd 2775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) = 𝑧)
304	229	elrab 3659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)))
305	304	bilani 509	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)))
306	289	adantrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ (𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵))) → 𝑧 ≤ ((♯‘𝐵) − 1))
307	306	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → ((𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ≤ ((♯‘𝐵) − 1)))
308	307	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑧 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ≤ ((♯‘𝐵) − 1)))
309	305, 308	mpd 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ≤ ((♯‘𝐵) − 1))
310	298, 231, 246	3syl 19	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ ℤ)
311	278	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘𝐵) ∈ ℤ)
312	310, 311	zltlem1d 12647	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑧 < (♯‘𝐵) ↔ 𝑧 ≤ ((♯‘𝐵) − 1)))
313	309, 312	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 < (♯‘𝐵))
314	313	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 < (♯‘𝐵))
315	303, 314	eqbrtrd 5137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) < (♯‘𝐵))
316	300, 300	ltnled 11356	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → ((♯‘𝐵) < (♯‘𝐵) ↔ ¬ (♯‘𝐵) ≤ (♯‘𝐵)))
317	315, 316	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → ¬ (♯‘𝐵) ≤ (♯‘𝐵))
318	301, 317	pm2.21dd 198	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 ≠ (♯‘𝐵))
319		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ≠ (♯‘𝐵))
320	318, 319	pm2.61dane 3051	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ≠ (♯‘𝐵))
321	298, 320	eldifsnd 4759	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}))
322	321	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})))
323	322	ssrdv 3951	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}))
324	276, 323	eqssd 3962	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) = {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
325	324	sumeq1d 15750	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
326		fzfid 14008	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...((♯‘𝐵) − 1)) ∈ Fin)
327		ssrab2 4042	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...((♯‘𝐵) − 1))
328	327	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...((♯‘𝐵) − 1)))
329	326, 328	ssfid 9228	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin)
330	26	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝐵 ∈ Fin)
331	88	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
332	330, 331	ssfid 9228	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
333	332, 91	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
334	333	nn0red 12565	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ)
335	125	elrab 3659	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)))
336	335	bilani 509	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)))
337		elfzelz 13551	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (1...((♯‘𝐵) − 1)) → 𝑘 ∈ ℤ)
338		elfzle1 13554	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (1...((♯‘𝐵) − 1)) → 1 ≤ 𝑘)
339	337, 338	jca 520	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (1...((♯‘𝐵) − 1)) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
340	339	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
341	340	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
342	341, 135	sylibr 237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → 𝑘 ∈ ℕ)
343	342	ex 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → 𝑘 ∈ ℕ))
344	343	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → 𝑘 ∈ ℕ))
345	336, 344	mpd 16	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑘 ∈ ℕ)
346	345	phicld 16830	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℕ)
347	346	nnred 12247	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℝ)
348		simpll 778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝜑)
349	335	bilanri 511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
350	349	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
351	348, 350	jca 520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}))
352	351, 334	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ)
353		simpr 489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
354	351, 353	jca 520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
355	336	simprd 500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑘 ∥ (♯‘𝐵))
356	355	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∥ (♯‘𝐵))
357		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
358	356, 357	jca 520	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
359		breq1 5116	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑘 → (𝑚 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
360		eqeq2 2781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 = 𝑘 → (((od‘𝐺)‘𝑥) = 𝑚 ↔ ((od‘𝐺)‘𝑥) = 𝑘))
361	360	rabbidv 3430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 = 𝑘 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
362	361	neeq1d 3023	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑘 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
363	359, 362	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 = 𝑘 → ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) ↔ (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)))
364	361	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑘 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
365		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑘 → (ϕ‘𝑚) = (ϕ‘𝑘))
366	364, 365	eqeq12d 2785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 = 𝑘 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
367	363, 366	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑚 = 𝑘 → (((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)) ↔ ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))))
368	28	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ∀𝑚 ∈ ℕ ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)))
369	367, 368, 345	rspcdva 3591	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
370	369	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
371	358, 370	mpd 16	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))
372	354, 371	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))
373	352, 372	eqled 11312	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
374		id 23	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
375	374	necon1bi 2992	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = ∅)
376	375	adantl 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = ∅)
377	376	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘∅))
378	222	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘∅) = 0)
379	377, 378	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = 0)
380	342	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∈ ℕ)
381	380	phicld 16830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (ϕ‘𝑘) ∈ ℕ)
382	381	nnnn0d 12564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (ϕ‘𝑘) ∈ ℕ0)
383	382	nn0ge0d 12567	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 0 ≤ (ϕ‘𝑘))
384	379, 383	eqbrtrd 5137	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
385	373, 384	pm2.61dan 824	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
386	385	ex 417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘)))
387	386	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘)))
388	336, 387	mpd 16	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
389	329, 334, 347, 388	fsumle 15850	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
390	324	sumeq1d 15750	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
391	390	eqcomd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
392	389, 391	breqtrd 5141	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
393	325, 392	eqbrtrd 5137	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
394	393	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
395	113, 121, 123, 140, 226, 394	ltleaddd 11834	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) < ((ϕ‘(♯‘𝐵)) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)))
396		nfcv 2931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑘(ϕ‘(♯‘𝐵))
397		simpll 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝜑)
398	126	bilani 509	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))
399	397, 398	jca 520	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))))
400	131	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
401	400	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ (𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
402	401, 135	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ (𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))) → 𝑘 ∈ ℕ)
403	402	ex 417	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → ((𝜑 ∧ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵))) → 𝑘 ∈ ℕ))
404	399, 403	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑘 ∈ ℕ)
405	404	phicld 16830	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℕ)
406	405	nncnd 12248	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℂ)
407		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘𝐵) → (ϕ‘𝑘) = (ϕ‘(♯‘𝐵)))
408	81, 396, 86, 406, 103, 407	fsumsplit1 15795	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = ((ϕ‘(♯‘𝐵)) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)))
409	395, 408	breqtrrd 5143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) < Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
410	107, 409	eqbrtrd 5137	. . . . . . . . 9 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
411		elfzelz 13551	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (1...(♯‘𝐵)) → 𝑎 ∈ ℤ)
412		elfzle1 13554	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (1...(♯‘𝐵)) → 1 ≤ 𝑎)
413	411, 412	jca 520	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (1...(♯‘𝐵)) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
414	413	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵)) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
415	414	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵))) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
416		elnnz1 12619	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
417	415, 416	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ ℕ)
418	417	rabss3d 4043	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
419		simpl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝜑)
420		simprl 782	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ ℕ)
421	419, 420	jca 520	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → (𝜑 ∧ 𝑎 ∈ ℕ))
422		simprr 784	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∥ (♯‘𝐵))
423	421, 422	jca 520	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → ((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)))
424		1zzd 12624	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 1 ∈ ℤ)
425	278	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (♯‘𝐵) ∈ ℤ)
426	425	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
427	420	anassrs 472	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ ℕ)
428	427	nnzd 12616	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ ℤ)
429	427	nnge1d 12283	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 1 ≤ 𝑎)
430		nnz 12611	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℤ)
431	430	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → 𝑎 ∈ ℤ)
432	23, 25, 26	hashfingrpnn 19038	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
433	432	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (♯‘𝐵) ∈ ℕ)
434		dvdsle 16367	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑎 ∥ (♯‘𝐵) → 𝑎 ≤ (♯‘𝐵)))
435	431, 433, 434	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (𝑎 ∥ (♯‘𝐵) → 𝑎 ≤ (♯‘𝐵)))
436	435	imp 411	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ≤ (♯‘𝐵))
437	424, 426, 428, 429, 436	elfzd 13542	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ (1...(♯‘𝐵)))
438	423, 437	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ (1...(♯‘𝐵)))
439	438	rabss3d 4043	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
440	418, 439	eqssd 3962	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} = {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
441	440	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} = {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
442	441	sumeq1d 15750	. . . . . . . . 9 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
443	410, 442	breqtrd 5141	. . . . . . . 8 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
444		phisum 16849	. . . . . . . . 9 ⊢ ((♯‘𝐵) ∈ ℕ → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = (♯‘𝐵))
445	39, 444	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = (♯‘𝐵))
446	443, 445	breqtrd 5141	. . . . . . 7 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < (♯‘𝐵))
447	80, 446	eqbrtrd 5137	. . . . . 6 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) < (♯‘𝐵))
448	170	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℕ0)
449	448	nn0red 12565	. . . . . . 7 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℝ)
450	449	ltnrd 11343	. . . . . 6 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ¬ (♯‘𝐵) < (♯‘𝐵))
451	447, 450	pm2.21dd 198	. . . . 5 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
452	451	ex 417	. . . 4 ⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷)))
453	452	adantr 485	. . 3 ⊢ ((𝜑 ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷)))
454	36, 453	mpd 16	. 2 ⊢ ((𝜑 ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
455	33, 454	pm2.61dan 824	1 ⊢ (𝜑 → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095  {crab 3423   ∖ cdif 3910   ⊆ wss 3913  ∅c0 4294  {csn 4594   class class class wbr 5113  ‘cfv 6537  (class class class)co 7411  Fincfn 8942  ℂcc 11097  ℝcr 11098  0cc0 11099  1c1 11100   + caddc 11102   · cmul 11104   < clt 11242   ≤ cle 11243   − cmin 11440   / cdiv 11870  ℕcn 12232  ℕ₀cn0 12503  ℤcz 12590  ...cfz 13534  ♯chash 14365  Σcsu 15736   ∥ cdvds 16309   gcd cgcd 16551  ϕcphi 16822  Basecbs 17268  0_gc0g 17491  Grpcgrp 18999  ._gcmg 19132  odcod 19593

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 9609  ax-cnex 11155  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175  ax-pre-mulgt0 11176  ax-pre-sup 11177

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 7862  df-1st 7985  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8452  df-oadd 8456  df-omul 8457  df-er 8693  df-ec 8695  df-qs 8699  df-map 8825  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-sup 9401  df-inf 9402  df-oi 9471  df-card 9924  df-acn 9927  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248  df-sub 11442  df-neg 11443  df-div 11871  df-nn 12233  df-2 12302  df-3 12303  df-n0 12504  df-xnn0 12577  df-z 12591  df-uz 12862  df-rp 13016  df-ico 13377  df-fz 13535  df-fzo 13682  df-fl 13824  df-mod 13902  df-seq 14037  df-exp 14097  df-hash 14366  df-cj 15149  df-re 15150  df-im 15151  df-sqrt 15285  df-abs 15286  df-clim 15538  df-sum 15737  df-dvds 16310  df-gcd 16552  df-phi 16824  df-sets 17223  df-slot 17241  df-ndx 17253  df-base 17269  df-ress 17290  df-plusg 17322  df-0g 17493  df-mgm 18697  df-sgrp 18776  df-mnd 18792  df-grp 19002  df-minusg 19003  df-sbg 19004  df-mulg 19133  df-subg 19188  df-eqg 19190  df-od 19597

This theorem is referenced by:  unitscyglem5  42855