Theorem unitscyglem4 42946

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 2925	. . . . . 6 ⊢ Ⅎ𝑦𝐵
2		nfcv 2925	. . . . . 6 ⊢ Ⅎ𝑥𝐵
3		nfv 1944	. . . . . 6 ⊢ Ⅎ𝑥((od‘𝐺)‘𝑦) = 𝐷
4		nfv 1944	. . . . . 6 ⊢ Ⅎ𝑦((od‘𝐺)‘𝑥) = 𝐷
5		fveqeq2 6892	. . . . . 6 ⊢ (𝑦 = 𝑥 → (((od‘𝐺)‘𝑦) = 𝐷 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
6	1, 2, 3, 4, 5	cbvrabw 3451	. . . . 5 ⊢ {𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}
7	6	fveq2i 6886	. . . 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 5113	. . . . . . . 8 ⊢ (𝑚 = 𝐷 → (𝑚 ∥ (♯‘𝐵) ↔ 𝐷 ∥ (♯‘𝐵)))
15		eqeq2 2775	. . . . . . . . . 10 ⊢ (𝑚 = 𝐷 → (((od‘𝐺)‘𝑥) = 𝑚 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
16	15	rabbidv 3423	. . . . . . . . 9 ⊢ (𝑚 = 𝐷 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
17	16	neeq1d 3017	. . . . . . . 8 ⊢ (𝑚 = 𝐷 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))
18	14, 17	anbi12d 643	. . . . . . 7 ⊢ (𝑚 = 𝐷 → ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) ↔ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)))
19	16	fveq2d 6887	. . . . . . . 8 ⊢ (𝑚 = 𝐷 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))
20		fveq2 6883	. . . . . . . 8 ⊢ (𝑚 = 𝐷 → (ϕ‘𝑚) = (ϕ‘𝐷))
21	19, 20	eqeq12d 2779	. . . . . . 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 42945	. . . . . 6 ⊢ (𝜑 → ∀𝑚 ∈ ℕ ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (ϕ‘𝑚)))
29		unitscyglem4.1	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ ℕ)
30	22, 28, 29	rspcdva 3583	. . . . 5 ⊢ (𝜑 → ((𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)))
31	30	imp 411	. . . 4 ⊢ ((𝜑 ∧ (𝐷 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))
32	13, 31	syl 18	. . 3 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))
33	8, 32	eqtrd 2798	. 2 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅) → (♯‘{𝑦 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑦) = 𝐷}) = (ϕ‘𝐷))
34		id 23	. . . . 5 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
35	34	necon1bi 2986	. . . 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 19040	. . . . . . . . 9 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℕ)
40	23, 24, 37, 38, 39	grpods 42942	. . . . . . . 8 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)}))
41		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵))
42	41	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → (♯‘𝐵) = (𝑙 · ((od‘𝐺)‘𝑥)))
43	42	oveq1d 7427	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((♯‘𝐵) ↑ 𝑥) = ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥))
44	25	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐺 ∈ Grp)
45	44	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝐺 ∈ Grp)
46		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝑙 ∈ ℤ)
47		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (od‘𝐺) = (od‘𝐺)
48		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵)
49	23, 47, 48	odcld 19623	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
50	49	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((od‘𝐺)‘𝑥) ∈ ℕ0)
51	50	nn0zd 12617	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((od‘𝐺)‘𝑥) ∈ ℤ)
52		simplr 780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → 𝑥 ∈ 𝐵)
53	46, 51, 52	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ∈ ℤ ∧ ((od‘𝐺)‘𝑥) ∈ ℤ ∧ 𝑥 ∈ 𝐵))
54	23, 24	mulgass 19178	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ Grp ∧ (𝑙 ∈ ℤ ∧ ((od‘𝐺)‘𝑥) ∈ ℤ ∧ 𝑥 ∈ 𝐵)) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)))
55	45, 53, 54	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)))
56		eqid 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ (0g‘𝐺) = (0g‘𝐺)
57	23, 47, 24, 56	odid 19609	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝐵 → (((od‘𝐺)‘𝑥) ↑ 𝑥) = (0g‘𝐺))
58	52, 57	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (((od‘𝐺)‘𝑥) ↑ 𝑥) = (0g‘𝐺))
59	58	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)) = (𝑙 ↑ (0g‘𝐺)))
60	23, 24, 56	mulgz 19169	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ Grp ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (0g‘𝐺)) = (0g‘𝐺))
61	44, 60	sylan 591	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (0g‘𝐺)) = (0g‘𝐺))
62	59, 61	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → (𝑙 ↑ (((od‘𝐺)‘𝑥) ↑ 𝑥)) = (0g‘𝐺))
63	55, 62	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (0g‘𝐺))
64	63	adantr 485	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((𝑙 · ((od‘𝐺)‘𝑥)) ↑ 𝑥) = (0g‘𝐺))
65	43, 64	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑙 ∈ ℤ) ∧ (𝑙 · ((od‘𝐺)‘𝑥)) = (♯‘𝐵)) → ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺))
66	26	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐵 ∈ Fin)
67	23, 47	oddvds2 19637	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
68	44, 66, 48, 67	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∥ (♯‘𝐵))
69	49	nn0zd 12617	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((od‘𝐺)‘𝑥) ∈ ℤ)
70		hashcl 14394	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ0)
71	66, 70	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℕ0)
72	71	nn0zd 12617	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (♯‘𝐵) ∈ ℤ)
73		divides 16313	. . . . . . . . . . . . . 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 3173	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺))
77	76	rabeqcda 3427	. . . . . . . . . 10 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)} = 𝐵)
78	77	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)} = 𝐵)
79	78	fveq2d 6887	. . . . . . . 8 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((♯‘𝐵) ↑ 𝑥) = (0g‘𝐺)}) = (♯‘𝐵))
80	40, 79	eqtr2d 2799	. . . . . . 7 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) = Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
81		nfv 1944	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅)
82		nfcv 2925	. . . . . . . . . . 11 ⊢ Ⅎ𝑘(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)})
83		fzfid 14011	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (1...(♯‘𝐵)) ∈ Fin)
84		ssrab2 4035	. . . . . . . . . . . . 13 ⊢ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵))
85	84	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...(♯‘𝐵)))
86	83, 85	ssfid 9230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin)
87	38	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝐵 ∈ Fin)
88		ssrab2 4035	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵
89	88	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
90	87, 89	ssfid 9230	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
91		hashcl 14394	. . . . . . . . . . . . 13 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
92	90, 91	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
93	92	nn0cnd 12568	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℂ)
94		breq1 5113	. . . . . . . . . . . 12 ⊢ (𝑎 = (♯‘𝐵) → (𝑎 ∥ (♯‘𝐵) ↔ (♯‘𝐵) ∥ (♯‘𝐵)))
95		1zzd 12626	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 1 ∈ ℤ)
96	39	nnzd 12618	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℤ)
97	39	nnge1d 12285	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 1 ≤ (♯‘𝐵))
98	39	nnred 12249	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℝ)
99	98	leidd 11781	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ≤ (♯‘𝐵))
100	95, 96, 96, 97, 99	elfzd 13544	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ (1...(♯‘𝐵)))
101		iddvds 16328	. . . . . . . . . . . . 13 ⊢ ((♯‘𝐵) ∈ ℤ → (♯‘𝐵) ∥ (♯‘𝐵))
102	96, 101	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∥ (♯‘𝐵))
103	94, 100, 102	elrabd 3653	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
104		eqeq2 2775	. . . . . . . . . . . . 13 ⊢ (𝑘 = (♯‘𝐵) → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = (♯‘𝐵)))
105	104	rabbidv 3423	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘𝐵) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)})
106	105	fveq2d 6887	. . . . . . . . . . 11 ⊢ (𝑘 = (♯‘𝐵) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}))
107	81, 82, 86, 93, 103, 106	fsumsplit1 15798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})))
108		ssrab2 4035	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ⊆ 𝐵
109	108	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ⊆ 𝐵)
110	38, 109	ssfid 9230	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ∈ Fin)
111		hashcl 14394	. . . . . . . . . . . . . 14 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℕ0)
112	110, 111	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℕ0)
113	112	nn0red 12567	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) ∈ ℝ)
114		diffi 9160	. . . . . . . . . . . . . . 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 9230	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
119	118, 91	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
120	115, 119	fsumnn0cl 15789	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
121	120	nn0red 12567	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ)
122	39	phicld 16832	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (ϕ‘(♯‘𝐵)) ∈ ℕ)
123	122	nnred 12249	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (ϕ‘(♯‘𝐵)) ∈ ℝ)
124		eldifi 4086	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) → 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
125		breq1 5113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑘 → (𝑎 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
126	125	elrab 3651	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))
127	126	biimpi 219	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑘 ∈ (1...(♯‘𝐵)) ∧ 𝑘 ∥ (♯‘𝐵)))
128		elfzelz 13553	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ (1...(♯‘𝐵)) → 𝑘 ∈ ℤ)
129		elfzle1 13556	. . . . . . . . . . . . . . . . . . . . 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 12621	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
136	134, 135	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → 𝑘 ∈ ℕ)
137		phicl 16829	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → (ϕ‘𝑘) ∈ ℕ)
138	136, 137	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (ϕ‘𝑘) ∈ ℕ)
139	138	nnred 12249	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (ϕ‘𝑘) ∈ ℝ)
140	115, 139	fsumrecl 15787	. . . . . . . . . . . 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 6892	. . . . . . . . . . . . . . . . . . . . . 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 12618	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℤ)
151	149	nnne0d 12287	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ≠ 0)
152	26	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐵 ∈ Fin)
153	152, 70	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
154	153	nn0zd 12617	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
155		dvdsval2 16314	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐷 ∈ ℤ ∧ 𝐷 ≠ 0 ∧ (♯‘𝐵) ∈ ℤ) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℤ))
156	150, 151, 154, 155	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℤ))
157	148, 156	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℤ)
158		simplr 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝑧 ∈ 𝐵)
159	23, 24, 147, 157, 158	mulgcld 19163	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ 𝐵)
160	153	nn0cnd 12568	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℂ)
161	29	nncnd 12250	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐷 ∈ ℂ)
162	161	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 ∈ ℂ)
163	23, 147, 152	hashfingrpnn 19040	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ)
164	163	nnne0d 12287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) ≠ 0)
165	160, 160, 162, 164, 151	divdiv2d 12024	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)) = (((♯‘𝐵) · 𝐷) / (♯‘𝐵)))
166	162, 160, 164	divcan3d 11997	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) · 𝐷) / (♯‘𝐵)) = 𝐷)
167	165, 166	eqtr2d 2799	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 = ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)))
168		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = (♯‘𝐵))
169	168	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) = (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)))
170	26, 70	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ0)
171	170	nn0cnd 12568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → (♯‘𝐵) ∈ ℂ)
172	29	nnne0d 12287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐷 ≠ 0)
173	171, 161, 172	divcan2d 11994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝜑 → (𝐷 · ((♯‘𝐵) / 𝐷)) = (♯‘𝐵))
174	173	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
175	174	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
176	175	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = (𝐷 · ((♯‘𝐵) / 𝐷)))
177	176	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)) = (((♯‘𝐵) / 𝐷) gcd (𝐷 · ((♯‘𝐵) / 𝐷))))
178		nndivdvds 16320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((♯‘𝐵) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℕ))
179	163, 149, 178	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (𝐷 ∥ (♯‘𝐵) ↔ ((♯‘𝐵) / 𝐷) ∈ ℕ))
180	148, 179	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℕ)
181	180	nnnn0d 12566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℕ0)
182	181, 150	gcdmultipled 16593	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (𝐷 · ((♯‘𝐵) / 𝐷))) = ((♯‘𝐵) / 𝐷))
183	177, 182	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd (♯‘𝐵)) = ((♯‘𝐵) / 𝐷))
184	169, 183	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) = ((♯‘𝐵) / 𝐷))
185	184	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) = (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)))
186	185	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / ((♯‘𝐵) / 𝐷)) = ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))))
187	167, 186	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → 𝐷 = ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))))
188	168	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = ((od‘𝐺)‘𝑧))
189	23, 47, 24	odmulg 19627	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝐵 ∧ ((♯‘𝐵) / 𝐷) ∈ ℤ) → ((od‘𝐺)‘𝑧) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))))
190	147, 158, 157, 189	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))))
191	188, 190	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (♯‘𝐵) = ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))))
192	191	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))) = (♯‘𝐵))
193	157	zcnd 12702	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / 𝐷) ∈ ℂ)
194	184, 193	eqeltrd 2863	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℂ)
195	23, 47, 159	odcld 19623	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ∈ ℕ0)
196	195	nn0cnd 12568	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ∈ ℂ)
197	168, 154	eqeltrd 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) ∈ ℤ)
198	168, 164	eqnetrd 3025	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘𝑧) ≠ 0)
199	157, 197, 198	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ≠ 0))
200		gcd2n0cl 16568	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((♯‘𝐵) / 𝐷) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ∈ ℤ ∧ ((od‘𝐺)‘𝑧) ≠ 0) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℕ)
201	199, 200	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ∈ ℕ)
202	201	nnne0d 12287	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) ≠ 0)
203	160, 194, 196, 202	divmuld 12014	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) = ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) ↔ ((((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧)) · ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧))) = (♯‘𝐵)))
204	192, 203	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((♯‘𝐵) / (((♯‘𝐵) / 𝐷) gcd ((od‘𝐺)‘𝑧))) = ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)))
205	187, 204	eqtr2d 2799	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → ((od‘𝐺)‘(((♯‘𝐵) / 𝐷) ↑ 𝑧)) = 𝐷)
206	146, 159, 205	elrabd 3653	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → (((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
207		ne0i 4295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((♯‘𝐵) / 𝐷) ↑ 𝑧) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
208	206, 207	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
209	145, 208	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) ∧ 𝑧 ∈ 𝐵) ∧ ((od‘𝐺)‘𝑧) = (♯‘𝐵)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
210		rabn0 4347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = (♯‘𝐵))
211		nfv 1944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑧((od‘𝐺)‘𝑥) = (♯‘𝐵)
212		nfv 1944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑥((od‘𝐺)‘𝑧) = (♯‘𝐵)
213		fveqeq2 6892	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑧 → (((od‘𝐺)‘𝑥) = (♯‘𝐵) ↔ ((od‘𝐺)‘𝑧) = (♯‘𝐵)))
214	211, 212, 213	cbvrexw 3308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑥 ∈ 𝐵 ((od‘𝐺)‘𝑥) = (♯‘𝐵) ↔ ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
215	210, 214	bitri 278	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ ↔ ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
216	215	bilani 509	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) → ∃𝑧 ∈ 𝐵 ((od‘𝐺)‘𝑧) = (♯‘𝐵))
217	209, 216	r19.29a 3173	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅)
218	217	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ≠ ∅))
219	218	necon4d 2982	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} = ∅))
220	219	imp 411	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)} = ∅)
221	220	fveq2d 6887	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) = (♯‘∅))
222		hash0 14405	. . . . . . . . . . . . . . 15 ⊢ (♯‘∅) = 0
223	222	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘∅) = 0)
224	221, 223	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) = 0)
225	122	nngt0d 12286	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → 0 < (ϕ‘(♯‘𝐵)))
226	224, 225	eqbrtrd 5134	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) < (ϕ‘(♯‘𝐵)))
227		eldif 3916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ↔ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}))
228	227	bilani 509	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})) → (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}))
229		breq1 5113	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑧 → (𝑎 ∥ (♯‘𝐵) ↔ 𝑧 ∥ (♯‘𝐵)))
230	229	elrab 3651	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
231	230	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} → (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
232	231	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → (𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)))
233		velsn 4606	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ {(♯‘𝐵)} ↔ 𝑧 = (♯‘𝐵))
234	233	bicomi 227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 = (♯‘𝐵) ↔ 𝑧 ∈ {(♯‘𝐵)})
235	234	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 = (♯‘𝐵) → 𝑧 ∈ {(♯‘𝐵)})
236	235	necon3bi 2984	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑧 ∈ {(♯‘𝐵)} → 𝑧 ≠ (♯‘𝐵))
237	236	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → 𝑧 ≠ (♯‘𝐵))
238	232, 237	jca 520	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)}) → ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)))
239	238	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∧ ¬ 𝑧 ∈ {(♯‘𝐵)})) → ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)))
240		1zzd 12626	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 1 ∈ ℤ)
241	26	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝐵 ∈ Fin)
242	241, 70	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℕ0)
243	242	nn0zd 12617	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℤ)
244	243, 240	zsubcld 12706	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → ((♯‘𝐵) − 1) ∈ ℤ)
245		elfzelz 13553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑧 ∈ (1...(♯‘𝐵)) → 𝑧 ∈ ℤ)
246	245	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) → 𝑧 ∈ ℤ)
247	246	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵)) → 𝑧 ∈ ℤ)
248	247	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ ℤ)
249		elfzle1 13556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ≠ 𝑧)
259	256, 258	jca 520	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 ≤ (♯‘𝐵) ∧ (♯‘𝐵) ≠ 𝑧))
260	248	zred 12701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ ℝ)
261	242	nn0red 12567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (♯‘𝐵) ∈ ℝ)
262	260, 261	ltlend 11356	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 < (♯‘𝐵) ↔ (𝑧 ≤ (♯‘𝐵) ∧ (♯‘𝐵) ≠ 𝑧)))
263	259, 262	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 < (♯‘𝐵))
264	248, 243	zltlem1d 12649	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → (𝑧 < (♯‘𝐵) ↔ 𝑧 ≤ ((♯‘𝐵) − 1)))
265	263, 264	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ≤ ((♯‘𝐵) − 1))
266	240, 244, 248, 252, 265	elfzd 13544	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∈ (1...((♯‘𝐵) − 1)))
267		simprlr 791	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ ((𝑧 ∈ (1...(♯‘𝐵)) ∧ 𝑧 ∥ (♯‘𝐵)) ∧ 𝑧 ≠ (♯‘𝐵))) → 𝑧 ∥ (♯‘𝐵))
268	229, 266, 267	elrabd 3653	. . . . . . . . . . . . . . . . . . . . . . . 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 3944	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) ⊆ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
277		1zzd 12626	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ∈ ℤ)
278	170	nn0zd 12617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (♯‘𝐵) ∈ ℤ)
279	278	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → (♯‘𝐵) ∈ ℤ)
280		elfzelz 13553	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ∈ ℤ)
281	280	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ ℤ)
282		elfzle1 13556	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 1 ≤ 𝑧)
283	282	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ≤ 𝑧)
284	281	zred 12701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ ℝ)
285	279	zred 12701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → (♯‘𝐵) ∈ ℝ)
286		1red 11210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 1 ∈ ℝ)
287	285, 286	resubcld 11643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → ((♯‘𝐵) − 1) ∈ ℝ)
288		elfzle2 13557	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ≤ ((♯‘𝐵) − 1))
289	288	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ≤ ((♯‘𝐵) − 1))
290	285	lem1d 12149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → ((♯‘𝐵) − 1) ≤ (♯‘𝐵))
291	284, 287, 285, 289, 290	letrd 11368	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ≤ (♯‘𝐵))
292	277, 279, 281, 283, 291	elfzd 13544	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ (1...((♯‘𝐵) − 1))) → 𝑧 ∈ (1...(♯‘𝐵)))
293	292	ex 417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑧 ∈ (1...((♯‘𝐵) − 1)) → 𝑧 ∈ (1...(♯‘𝐵))))
294	293	ssrdv 3944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1...((♯‘𝐵) − 1)) ⊆ (1...(♯‘𝐵)))
295		rabss2 4032	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1...((♯‘𝐵) − 1)) ⊆ (1...(♯‘𝐵)) → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
296	294, 295	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
297	296	sseld 3937	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → 𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}))
298	297	imp 411	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
299	170	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ∈ ℕ0)
300	299	nn0red 12567	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ∈ ℝ)
301	300	leidd 11781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) ≤ (♯‘𝐵))
302		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 = (♯‘𝐵))
303	302	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) = 𝑧)
304	229	elrab 3651	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 12649	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑧 < (♯‘𝐵) ↔ 𝑧 ≤ ((♯‘𝐵) − 1)))
313	309, 312	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 < (♯‘𝐵))
314	313	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → 𝑧 < (♯‘𝐵))
315	303, 314	eqbrtrd 5134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) ∧ 𝑧 = (♯‘𝐵)) → (♯‘𝐵) < (♯‘𝐵))
316	300, 300	ltnled 11358	. . . . . . . . . . . . . . . . . . . . . 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 3045	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ≠ (♯‘𝐵))
321	298, 320	eldifsnd 4756	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}))
322	321	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑧 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} → 𝑧 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})))
323	322	ssrdv 3944	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}))
324	276, 323	eqssd 3955	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)}) = {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)})
325	324	sumeq1d 15753	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
326		fzfid 14011	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...((♯‘𝐵) − 1)) ∈ Fin)
327		ssrab2 4035	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...((♯‘𝐵) − 1))
328	327	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ (1...((♯‘𝐵) − 1)))
329	326, 328	ssfid 9230	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ∈ Fin)
330	26	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → 𝐵 ∈ Fin)
331	88	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
332	330, 331	ssfid 9230	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
333	332, 91	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ0)
334	333	nn0red 12567	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℝ)
335	125	elrab 3651	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} ↔ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)))
336	335	bilani 509	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵)))
337		elfzelz 13553	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ (1...((♯‘𝐵) − 1)) → 𝑘 ∈ ℤ)
338		elfzle1 13556	. . . . . . . . . . . . . . . . . . . . . . . . 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 16832	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℕ)
347	346	nnred 12249	. . . . . . . . . . . . . . . 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 5113	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑘 → (𝑚 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
360		eqeq2 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 = 𝑘 → (((od‘𝐺)‘𝑥) = 𝑚 ↔ ((od‘𝐺)‘𝑥) = 𝑘))
361	360	rabbidv 3423	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 = 𝑘 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
362	361	neeq1d 3017	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑘 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
363	359, 362	anbi12d 643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 = 𝑘 → ((𝑚 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚} ≠ ∅) ↔ (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)))
364	361	fveq2d 6887	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑘 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑚}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
365		fveq2 6883	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑘 → (ϕ‘𝑚) = (ϕ‘𝑘))
366	364, 365	eqeq12d 2779	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3583	. . . . . . . . . . . . . . . . . . . . . . . 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 11314	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ (ϕ‘𝑘))
374		id 23	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
375	374	necon1bi 2986	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅ → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = ∅)
376	375	adantl 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = ∅)
377	376	fveq2d 6887	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘∅))
378	222	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘∅) = 0)
379	377, 378	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = 0)
380	342	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 𝑘 ∈ ℕ)
381	380	phicld 16832	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (ϕ‘𝑘) ∈ ℕ)
382	381	nnnn0d 12566	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (ϕ‘𝑘) ∈ ℕ0)
383	382	nn0ge0d 12569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑘 ∈ (1...((♯‘𝐵) − 1)) ∧ 𝑘 ∥ (♯‘𝐵))) ∧ ¬ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → 0 ≤ (ϕ‘𝑘))
384	379, 383	eqbrtrd 5134	. . . . . . . . . . . . . . . . . . . 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 15853	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
390	324	sumeq1d 15753	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
391	390	eqcomd 2769	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
392	389, 391	breqtrd 5138	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...((♯‘𝐵) − 1)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
393	325, 392	eqbrtrd 5134	. . . . . . . . . . . . 13 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
394	393	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ≤ Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘))
395	113, 121, 123, 140, 226, 394	ltleaddd 11836	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) < ((ϕ‘(♯‘𝐵)) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)))
396		nfcv 2925	. . . . . . . . . . . 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 16832	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℕ)
406	405	nncnd 12250	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) ∧ 𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)}) → (ϕ‘𝑘) ∈ ℂ)
407		fveq2 6883	. . . . . . . . . . . 12 ⊢ (𝑘 = (♯‘𝐵) → (ϕ‘𝑘) = (ϕ‘(♯‘𝐵)))
408	81, 396, 86, 406, 103, 407	fsumsplit1 15798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = ((ϕ‘(♯‘𝐵)) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(ϕ‘𝑘)))
409	395, 408	breqtrrd 5140	. . . . . . . . . 10 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = (♯‘𝐵)}) + Σ𝑘 ∈ ({𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} ∖ {(♯‘𝐵)})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})) < Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
410	107, 409	eqbrtrd 5134	. . . . . . . . 9 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
411		elfzelz 13553	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (1...(♯‘𝐵)) → 𝑎 ∈ ℤ)
412		elfzle1 13556	. . . . . . . . . . . . . . . . 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 12621	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
417	415, 416	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(♯‘𝐵)) ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ ℕ)
418	417	rabss3d 4036	. . . . . . . . . . . 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 12626	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 1 ∈ ℤ)
425	278	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (♯‘𝐵) ∈ ℤ)
426	425	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → (♯‘𝐵) ∈ ℤ)
427	420	anassrs 472	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ ℕ)
428	427	nnzd 12618	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ ℤ)
429	427	nnge1d 12285	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 1 ≤ 𝑎)
430		nnz 12613	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ ℕ → 𝑎 ∈ ℤ)
431	430	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → 𝑎 ∈ ℤ)
432	23, 25, 26	hashfingrpnn 19040	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
433	432	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (♯‘𝐵) ∈ ℕ)
434		dvdsle 16369	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ) → (𝑎 ∥ (♯‘𝐵) → 𝑎 ≤ (♯‘𝐵)))
435	431, 433, 434	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑎 ∈ ℕ) → (𝑎 ∥ (♯‘𝐵) → 𝑎 ≤ (♯‘𝐵)))
436	435	imp 411	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ≤ (♯‘𝐵))
437	424, 426, 428, 429, 436	elfzd 13544	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑎 ∈ ℕ) ∧ 𝑎 ∥ (♯‘𝐵)) → 𝑎 ∈ (1...(♯‘𝐵)))
438	423, 437	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑎 ∥ (♯‘𝐵))) → 𝑎 ∈ (1...(♯‘𝐵)))
439	438	rabss3d 4036	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} ⊆ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)})
440	418, 439	eqssd 3955	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} = {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
441	440	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} = {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)})
442	441	sumeq1d 15753	. . . . . . . . 9 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
443	410, 442	breqtrd 5138	. . . . . . . 8 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘))
444		phisum 16851	. . . . . . . . 9 ⊢ ((♯‘𝐵) ∈ ℕ → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = (♯‘𝐵))
445	39, 444	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ (♯‘𝐵)} (ϕ‘𝑘) = (♯‘𝐵))
446	443, 445	breqtrd 5138	. . . . . . 7 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → Σ𝑘 ∈ {𝑎 ∈ (1...(♯‘𝐵)) ∣ 𝑎 ∥ (♯‘𝐵)} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) < (♯‘𝐵))
447	80, 446	eqbrtrd 5134	. . . . . 6 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) < (♯‘𝐵))
448	170	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℕ0)
449	448	nn0red 12567	. . . . . . 7 ⊢ ((𝜑 ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} = ∅) → (♯‘𝐵) ∈ ℝ)
450	449	ltnrd 11345	. . . . . 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 1103   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  {crab 3416   ∖ cdif 3903   ⊆ wss 3906  ∅c0 4287  {csn 4590   class class class wbr 5110  ‘cfv 6538  (class class class)co 7412  Fincfn 8944  ℂcc 11099  ℝcr 11100  0cc0 11101  1c1 11102   + caddc 11104   · cmul 11106   < clt 11244   ≤ cle 11245   − cmin 11442   / cdiv 11872  ℕcn 12234  ℕ₀cn0 12505  ℤcz 12592  ...cfz 13536  ♯chash 14368  Σcsu 15739   ∥ cdvds 16311   gcd cgcd 16553  ϕcphi 16824  Basecbs 17270  0_gc0g 17493  Grpcgrp 19001  ._gcmg 19134  odcod 19595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-inf2 9611  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178  ax-pre-sup 11179

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-int 4914  df-iun 4959  df-disj 5078  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-1o 8454  df-oadd 8458  df-omul 8459  df-er 8695  df-ec 8697  df-qs 8701  df-map 8827  df-en 8945  df-dom 8946  df-sdom 8947  df-fin 8948  df-sup 9403  df-inf 9404  df-oi 9473  df-card 9926  df-acn 9929  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-div 11873  df-nn 12235  df-2 12304  df-3 12305  df-n0 12506  df-xnn0 12579  df-z 12593  df-uz 12864  df-rp 13018  df-ico 13379  df-fz 13537  df-fzo 13685  df-fl 13827  df-mod 13905  df-seq 14040  df-exp 14100  df-hash 14369  df-cj 15152  df-re 15153  df-im 15154  df-sqrt 15288  df-abs 15289  df-clim 15541  df-sum 15740  df-dvds 16312  df-gcd 16554  df-phi 16826  df-sets 17225  df-slot 17243  df-ndx 17255  df-base 17271  df-ress 17292  df-plusg 17324  df-0g 17495  df-mgm 18699  df-sgrp 18778  df-mnd 18794  df-grp 19004  df-minusg 19005  df-sbg 19006  df-mulg 19135  df-subg 19190  df-eqg 19192  df-od 19599

This theorem is referenced by:  unitscyglem5  42947