unitscyglem2 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > unitscyglem2		Structured version Visualization version GIF version

Theorem unitscyglem2 43004

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

**Hypotheses**
Ref	Expression
unitscyglem1.1	⊢ 𝐵 = (Base‘𝐺)
unitscyglem1.2	⊢ ↑ = (._g‘𝐺)
unitscyglem1.3	⊢ (𝜑 → 𝐺 ∈ Grp)
unitscyglem1.4	⊢ (𝜑 → 𝐵 ∈ Fin)
unitscyglem1.5	⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0_g‘𝐺)}) ≤ 𝑛)
unitscyglem2.1	⊢ (𝜑 → 𝐷 ∈ ℕ)
unitscyglem2.2	⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵))
unitscyglem2.3	⊢ (𝜑 → 𝐴 ∈ 𝐵)
unitscyglem2.4	⊢ (𝜑 → ((od‘𝐺)‘𝐴) = 𝐷)
unitscyglem2.5	⊢ (𝜑 → ∀𝑐 ∈ ℕ (𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))

**Assertion**
Ref	Expression
unitscyglem2	⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))

Distinct variable groups: ↑ ,𝑛,𝑥 𝐴,𝑛,𝑥 𝐵,𝑐,𝑥 𝐵,𝑛 𝐷,𝑐,𝑥 𝐺,𝑐,𝑥 𝑛,𝐺 𝜑,𝑥 Allowed substitution hints: 𝜑(𝑛, 𝑐) 𝐴(𝑐) 𝐷(𝑛) ↑ (𝑐)

Proof of Theorem unitscyglem2 Dummy variables 𝑘 𝑙 𝑎 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 5117	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑘 → (𝑎 ∥ 𝐷 ↔ 𝑘 ∥ 𝐷))
2	1	elrab 3653	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ↔ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷))
3	2	bilani 510	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷))
4	3	simpld 500	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ (1...(𝐷 − 1)))
5	4	elfzelzd 13571	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℤ)
6		unitscyglem2.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ)
7	6	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℕ)
8	7	nnzd 12635	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℤ)
9		unitscyglem1.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ Fin)
10		hashcl 14412	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ₀)
11	9, 10	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ₀)
12	11	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘𝐵) ∈ ℕ₀)
13	12	nn0zd 12634	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘𝐵) ∈ ℤ)
14	3	simprd 501	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∥ 𝐷)
15		unitscyglem2.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵))
16	15	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∥ (♯‘𝐵))
17	5, 8, 13, 14, 16	dvdstrd 16378	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∥ (♯‘𝐵))
18		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → 𝜑)
19	2, 4	sylan2br 607	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → 𝑘 ∈ (1...(𝐷 − 1)))
20	18, 19	jca 521	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → (𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))))
21	2, 14	sylan2br 607	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → 𝑘 ∥ 𝐷)
22	20, 21	jca 521	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷))
23		fveqeq2 6897	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((𝐷 / 𝑘) ↑ 𝐴) → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘))
24		unitscyglem1.1	. . . . . . . . . . . . . . . 16 ⊢ 𝐵 = (Base‘𝐺)
25		unitscyglem1.2	. . . . . . . . . . . . . . . 16 ⊢ ↑ = (._g‘𝐺)
26		unitscyglem1.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ∈ Grp)
27	26	ad4antr 745	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐺 ∈ Grp)
28		simpr 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝑙 · 𝑘) = 𝐷)
29	28	eqcomd 2772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (𝑙 · 𝑘))
30	29	oveq1d 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) = ((𝑙 · 𝑘) / 𝑘))
31		simplr 781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑙 ∈ ℕ)
32	31	nncnd 12267	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑙 ∈ ℂ)
33		elfzelz 13570	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 𝑘 ∈ ℤ)
34	33	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 𝑘 ∈ ℤ)
35	34	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℤ)
36	35	zcnd 12719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℂ)
37		elfzle1 13573	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 1 ≤ 𝑘)
38	37	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 1 ≤ 𝑘)
39	34, 38	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
40		elnnz1 12638	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
41	39, 40	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 𝑘 ∈ ℕ)
42	41	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → 𝑘 ∈ ℕ)
43	42	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℕ)
44	43	nnne0d 12304	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ≠ 0)
45	32, 36, 44	divcan4d 12015	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝑙 · 𝑘) / 𝑘) = 𝑙)
46	30, 45	eqtrd 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) = 𝑙)
47	46, 31	eqeltrd 2866	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℕ)
48	47	nnnn0d 12583	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℕ₀)
49	48	nn0zd 12634	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℤ)
50		unitscyglem2.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
51	50	ad4antr 745	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐴 ∈ 𝐵)
52	24, 25, 27, 49, 51	mulgcld 19193	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) ↑ 𝐴) ∈ 𝐵)
53	6	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → 𝐷 ∈ ℕ)
54	53	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ∈ ℕ)
55	54	nncnd 12267	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ∈ ℂ)
56	55, 36, 44	divcan1d 12010	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) · 𝑘) = 𝐷)
57		unitscyglem2.4	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((od‘𝐺)‘𝐴) = 𝐷)
58	57	ad4antr 745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘𝐴) = 𝐷)
59	58	eqcomd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = ((od‘𝐺)‘𝐴))
60		eqid 2766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (od‘𝐺) = (od‘𝐺)
61	24, 60, 25	odmulg 19657	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ (𝐷 / 𝑘) ∈ ℤ) → ((od‘𝐺)‘𝐴) = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
62	27, 51, 49, 61	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘𝐴) = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
63	59, 62	eqtrd 2801	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
64	58	oveq2d 7439	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) = ((𝐷 / 𝑘) gcd 𝐷))
65	55, 36, 44	divcan2d 12011	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝑘 · (𝐷 / 𝑘)) = 𝐷)
66	65	eqcomd 2772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (𝑘 · (𝐷 / 𝑘)))
67	66	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd 𝐷) = ((𝐷 / 𝑘) gcd (𝑘 · (𝐷 / 𝑘))))
68	48, 35	gcdmultipled 16617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd (𝑘 · (𝐷 / 𝑘))) = (𝐷 / 𝑘))
69	67, 68	eqtrd 2801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd 𝐷) = (𝐷 / 𝑘))
70	64, 69	eqtrd 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) = (𝐷 / 𝑘))
71	70	oveq1d 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
72	63, 71	eqtrd 2801	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
73	56, 72	eqtr2d 2802	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · 𝑘))
74	24, 60, 52	odcld 19653	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) ∈ ℕ₀)
75	74	nn0cnd 12585	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) ∈ ℂ)
76	49	zcnd 12719	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℂ)
77	54	nnne0d 12304	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ≠ 0)
78	55, 36, 77, 44	divne0d 12025	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ≠ 0)
79	75, 36, 76, 78	mulcand 11865	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · 𝑘) ↔ ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘))
80	73, 79	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘)
81	23, 52, 80	elrabd 3655	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) ↑ 𝐴) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
82	81	ne0d 4298	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
83		nndivides 16345	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑘 ∥ 𝐷 ↔ ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷))
84	42, 53, 83	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → (𝑘 ∥ 𝐷 ↔ ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷))
85	84	biimpd 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → (𝑘 ∥ 𝐷 → ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷))
86	85	syldbl2 855	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷)
87	82, 86	r19.29a 3176	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
88	22, 87	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
89	88	ex 418	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
90	89	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ((𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
91	3, 90	mpd 16	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
92	17, 91	jca 521	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
93	4, 37	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 1 ≤ 𝑘)
94	5, 93	jca 521	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
95	94, 40	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℕ)
96	95	nnred 12266	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℝ)
97	7	nnred 12266	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℝ)
98		1red 11227	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 1 ∈ ℝ)
99	97, 98	resubcld 11660	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝐷 − 1) ∈ ℝ)
100		elfzle2 13574	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 𝑘 ≤ (𝐷 − 1))
101	4, 100	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ≤ (𝐷 − 1))
102	97	ltm1d 12165	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝐷 − 1) < 𝐷)
103	96, 99, 97, 101, 102	lelttrd 11386	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 < 𝐷)
104		breq1 5117	. . . . . . . . . 10 ⊢ (𝑐 = 𝑘 → (𝑐 < 𝐷 ↔ 𝑘 < 𝐷))
105		breq1 5117	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (𝑐 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
106		eqeq2 2778	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑘 → (((od‘𝐺)‘𝑥) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑘))
107	106	rabbidv 3426	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑘 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
108	107	neeq1d 3020	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
109	105, 108	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑘 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)))
110	107	fveq2d 6892	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
111		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (ϕ‘𝑐) = (ϕ‘𝑘))
112	110, 111	eqeq12d 2782	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑘 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
113	109, 112	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑐 = 𝑘 → (((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)) ↔ ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))))
114	104, 113	imbi12d 347	. . . . . . . . 9 ⊢ (𝑐 = 𝑘 → ((𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) ↔ (𝑘 < 𝐷 → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))))
115		unitscyglem2.5	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑐 ∈ ℕ (𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
116	115	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ∀𝑐 ∈ ℕ (𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
117	114, 116, 95	rspcdva 3585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 < 𝐷 → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))))
118	103, 117	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
119	92, 118	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))
120	119	sumeq2dv 15779	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
121	120	eqcomd 2772	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
122	121	oveq1d 7438	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})))
123		elun 4110	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) ↔ (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
124	123	bilani 510	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
125		1zzd 12643	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ∈ ℤ)
126	6	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℕ)
127	126	nnzd 12635	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℤ)
128		elfzelz 13570	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 𝑎 ∈ ℤ)
129	128	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 𝑎 ∈ ℤ)
130	129	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℤ)
131		elfzle1 13573	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 1 ≤ 𝑎)
132	131	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 1 ≤ 𝑎)
133	132	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ≤ 𝑎)
134	130	zred 12718	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℝ)
135	126	nnred 12266	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℝ)
136		1red 11227	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ∈ ℝ)
137	135, 136	resubcld 11660	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → (𝐷 − 1) ∈ ℝ)
138		elfzle2 13574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 𝑎 ≤ (𝐷 − 1))
139	138	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 𝑎 ≤ (𝐷 − 1))
140	139	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ≤ (𝐷 − 1))
141	135	ltm1d 12165	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → (𝐷 − 1) < 𝐷)
142	134, 137, 135, 140, 141	lelttrd 11386	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 < 𝐷)
143	134, 135, 142	ltled 11376	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ≤ 𝐷)
144	125, 127, 130, 133, 143	elfzd 13561	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ (1...𝐷))
145	144	rabss3d 4038	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
146	145	sseld 3939	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
147	146	imp 412	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
148		elsni 4611	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝐷} → 𝑦 = 𝐷)
149	148	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → 𝑦 = 𝐷)
150		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝑦 = 𝐷)
151		breq1 5117	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝐷 → (𝑎 ∥ 𝐷 ↔ 𝐷 ∥ 𝐷))
152		1zzd 12643	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℤ)
153	6	nnzd 12635	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℤ)
154	6	nnge1d 12302	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ 𝐷)
155	6	nnred 12266	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐷 ∈ ℝ)
156	155	leidd 11798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ≤ 𝐷)
157	152, 153, 153, 154, 156	elfzd 13561	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∈ (1...𝐷))
158		iddvds 16352	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ ℤ → 𝐷 ∥ 𝐷)
159	153, 158	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∥ 𝐷)
160	151, 157, 159	elrabd 3655	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
161	160	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝐷 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
162	150, 161	eqeltrd 2866	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
163	162	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑦 = 𝐷 → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
164	163	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → (𝑦 = 𝐷 → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
165	149, 164	mpd 16	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
166	147, 165	jaodan 972	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷})) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
167	166	ex 418	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
168	167	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) → ((𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
169	124, 168	mpd 16	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
170	169	ex 418	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
171		simpr 490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝑦 = 𝐷)
172		eqidd 2767	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 = 𝐷)
173	6	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 ∈ ℕ)
174		elsng 4608	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℕ → (𝐷 ∈ {𝐷} ↔ 𝐷 = 𝐷))
175	173, 174	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → (𝐷 ∈ {𝐷} ↔ 𝐷 = 𝐷))
176	172, 175	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 ∈ {𝐷})
177	171, 176	eqeltrd 2866	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝑦 ∈ {𝐷})
178	177	olcd 888	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
179		breq1 5117	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑦 → (𝑎 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷))
180	179	elrab 3653	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} ↔ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷))
181	180	bilani 510	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷))
182	181	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷))
183		1zzd 12643	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 1 ∈ ℤ)
184	153	ad3antrrr 743	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℤ)
185	184, 183	zsubcld 12723	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝐷 − 1) ∈ ℤ)
186		elfzelz 13570	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝐷) → 𝑦 ∈ ℤ)
187	186	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ∈ ℤ)
188	187	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ ℤ)
189		elfzle1 13573	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝐷) → 1 ≤ 𝑦)
190	189	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 1 ≤ 𝑦)
191	190	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 1 ≤ 𝑦)
192		elfzle2 13574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝐷) → 𝑦 ≤ 𝐷)
193	192	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ≤ 𝐷)
194	193	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ≤ 𝐷)
195		neqne 2969	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑦 = 𝐷 → 𝑦 ≠ 𝐷)
196	195	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝑦 ≠ 𝐷)
197	196	necomd 3016	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝐷 ≠ 𝑦)
198	197	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ≠ 𝑦)
199	194, 198	jca 521	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦))
200	188	zred 12718	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ ℝ)
201	155	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℝ)
202	200, 201	ltlend 11373	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 < 𝐷 ↔ (𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦)))
203	199, 202	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 < 𝐷)
204	6	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℕ)
205	204	nnzd 12635	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℤ)
206	188, 205	zltlem1d 12666	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 < 𝐷 ↔ 𝑦 ≤ (𝐷 − 1)))
207	203, 206	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ≤ (𝐷 − 1))
208	183, 185, 188, 191, 207	elfzd 13561	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ (1...(𝐷 − 1)))
209		simprr 785	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∥ 𝐷)
210	179, 208, 209	elrabd 3655	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})
211	210	ex 418	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}))
212	182, 211	mpd 16	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})
213	212	orcd 887	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
214	178, 213	pm2.61dan 825	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
215	214, 123	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}))
216	215	ex 418	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})))
217	170, 216	impbid 215	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) ↔ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
218	217	eqrdv 2764	. . . . . . 7 ⊢ (𝜑 → ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) = {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
219	218	sumeq1d 15777	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
220		phisum 16875	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = 𝐷)
221	6, 220	syl 18	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = 𝐷)
222		eqcom 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (((od‘𝐺)‘𝐴) = 𝐷 ↔ 𝐷 = ((od‘𝐺)‘𝐴))
223	222	imbi2i 339	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 → ((od‘𝐺)‘𝐴) = 𝐷) ↔ (𝜑 → 𝐷 = ((od‘𝐺)‘𝐴)))
224	57, 223	mpbi 233	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 = ((od‘𝐺)‘𝐴))
225	224	oveq1d 7438	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 ↑ 𝑥) = (((od‘𝐺)‘𝐴) ↑ 𝑥))
226	225	eqeq1d 2768	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 ↑ 𝑥) = (0_g‘𝐺) ↔ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)))
227	226	rabbidv 3426	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)} = {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)})
228	227	fveq2d 6892	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}) = (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)}))
229		unitscyglem1.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0_g‘𝐺)}) ≤ 𝑛)
230	24, 25, 26, 9, 229, 50	unitscyglem1 43003	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)}) = ((od‘𝐺)‘𝐴))
231	228, 230	eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}) = ((od‘𝐺)‘𝐴))
232	231, 57	eqtr2d 2802	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 = (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}))
233	24, 25, 26, 9, 6	grpods 43002	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}))
234	232, 233	eqtr4d 2804	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
235	218	eqcomd 2772	. . . . . . . . . 10 ⊢ (𝜑 → {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} = ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}))
236	235	sumeq1d 15777	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
237	234, 236	eqtrd 2801	. . . . . . . 8 ⊢ (𝜑 → 𝐷 = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
238	221, 237	eqtr2d 2802	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
239		1zzd 12643	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 1 ∈ ℤ)
240	153	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℤ)
241	179	elrab 3653	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} ↔ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
242	241	bilani 510	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
243	242	simpld 500	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ℕ)
244	243	nnzd 12635	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ℤ)
245	243	nnge1d 12302	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 1 ≤ 𝑦)
246	242	simprd 501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∥ 𝐷)
247	6	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℕ)
248		dvdsle 16393	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
249	244, 247, 248	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
250	246, 249	mpd 16	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ≤ 𝐷)
251	239, 240, 244, 245, 250	elfzd 13561	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ (1...𝐷))
252	179, 251, 246	elrabd 3655	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
253	252	ex 418	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
254		elfzelz 13570	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (1...𝐷) → 𝑎 ∈ ℤ)
255		elfzle1 13573	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (1...𝐷) → 1 ≤ 𝑎)
256	254, 255	jca 521	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (1...𝐷) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
257	256	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
258	257	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷)) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
259		elnnz1 12638	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
260	258, 259	sylibr 237	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℕ)
261	260	rabss3d 4038	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} ⊆ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷})
262	261	sseld 3939	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}))
263	253, 262	impbid 215	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} ↔ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
264	263	eqrdv 2764	. . . . . . . 8 ⊢ (𝜑 → {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} = {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
265	264	sumeq1d 15777	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
266	238, 265	eqtr2d 2802	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
267	219, 266	eqtrd 2801	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
268		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑘𝜑
269		nfcv 2928	. . . . . 6 ⊢ Ⅎ𝑘(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
270		fzfid 14029	. . . . . . 7 ⊢ (𝜑 → (1...(𝐷 − 1)) ∈ Fin)
271		ssrab2 4037	. . . . . . . 8 ⊢ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ (1...(𝐷 − 1))
272	271	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ (1...(𝐷 − 1)))
273	270, 272	ssfid 9239	. . . . . 6 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∈ Fin)
274	151	elrab 3653	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ↔ (𝐷 ∈ (1...(𝐷 − 1)) ∧ 𝐷 ∥ 𝐷))
275	274	biimpi 219	. . . . . . . . . . 11 ⊢ (𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → (𝐷 ∈ (1...(𝐷 − 1)) ∧ 𝐷 ∥ 𝐷))
276	275	simpld 500	. . . . . . . . . 10 ⊢ (𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → 𝐷 ∈ (1...(𝐷 − 1)))
277	276	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ (1...(𝐷 − 1)))
278		elfzle2 13574	. . . . . . . . 9 ⊢ (𝐷 ∈ (1...(𝐷 − 1)) → 𝐷 ≤ (𝐷 − 1))
279	277, 278	syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ≤ (𝐷 − 1))
280	155	ltm1d 12165	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 − 1) < 𝐷)
281		1red 11227	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℝ)
282	155, 281	resubcld 11660	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 − 1) ∈ ℝ)
283	282, 155	ltnled 11375	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷 − 1) < 𝐷 ↔ ¬ 𝐷 ≤ (𝐷 − 1)))
284	280, 283	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝐷 ≤ (𝐷 − 1))
285	284	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ¬ 𝐷 ≤ (𝐷 − 1))
286	279, 285	pm2.21dd 198	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})
287		simpr 490	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})
288	286, 287	pm2.61dan 825	. . . . . 6 ⊢ (𝜑 → ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})
289	9	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐵 ∈ Fin)
290		ssrab2 4037	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵
291	290	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
292	289, 291	ssfid 9239	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
293		hashcl 14412	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ₀)
294	292, 293	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ₀)
295	294	nn0cnd 12585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℂ)
296		eqeq2 2778	. . . . . . . 8 ⊢ (𝑘 = 𝐷 → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
297	296	rabbidv 3426	. . . . . . 7 ⊢ (𝑘 = 𝐷 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
298	297	fveq2d 6892	. . . . . 6 ⊢ (𝑘 = 𝐷 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))
299		ssrab2 4037	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ⊆ 𝐵
300	299	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ⊆ 𝐵)
301	9, 300	ssfid 9239	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ∈ Fin)
302		hashcl 14412	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℕ₀)
303	301, 302	syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℕ₀)
304	303	nn0cnd 12585	. . . . . 6 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℂ)
305	268, 269, 273, 6, 288, 295, 298, 304	fsumsplitsn 15821	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})))
306	267, 305	eqtr2d 2802	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘))
307		nfcv 2928	. . . . 5 ⊢ Ⅎ𝑘(ϕ‘𝐷)
308	119, 295	eqeltrrd 2867	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (ϕ‘𝑘) ∈ ℂ)
309		fveq2 6888	. . . . 5 ⊢ (𝑘 = 𝐷 → (ϕ‘𝑘) = (ϕ‘𝐷))
310	6	phicld 16856	. . . . . 6 ⊢ (𝜑 → (ϕ‘𝐷) ∈ ℕ)
311	310	nncnd 12267	. . . . 5 ⊢ (𝜑 → (ϕ‘𝐷) ∈ ℂ)
312	268, 307, 273, 6, 288, 308, 309, 311	fsumsplitsn 15821	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
313	306, 312	eqtrd 2801	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
314	122, 313	eqtrd 2801	. 2 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
315	273, 308	fsumcl 15810	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) ∈ ℂ)
316	315, 304, 311	addcand 11431	. 2 ⊢ (𝜑 → ((Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)))
317	314, 316	mpbid 235	1 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 ∀wral 3082 ∃wrex 3092 {crab 3419 ∪ cun 3906 ⊆ wss 3908 ∅c0 4289 {csn 4594 class class class wbr 5114 ‘cfv 6543 (class class class)co 7423 Fincfn 8952 ℂcc 11116 ℝcr 11117 1c1 11119 + caddc 11121 · cmul 11123 < clt 11261 ≤ cle 11262 − cmin 11459 / cdiv 11889 ℕcn 12251 ℕ₀cn0 12522 ℤcz 12609 ...cfz 13553 ♯chash 14386 Σcsu 15763 ∥ cdvds 16335 gcd cgcd 16577 ϕcphi 16848 Basecbs 17294 0_gc0g 17517 Grpcgrp 19031 ._gcmg 19164 odcod 19625

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-inf2 9620 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-disj 5082 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-se 5620 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-oadd 8466 df-omul 8467 df-er 8703 df-map 8835 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-sup 9412 df-inf 9413 df-oi 9482 df-card 9944 df-acn 9947 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-n0 12523 df-xnn0 12596 df-z 12610 df-uz 12881 df-rp 13035 df-fz 13554 df-fzo 13702 df-fl 13845 df-mod 13923 df-seq 14058 df-exp 14118 df-hash 14387 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-clim 15565 df-sum 15764 df-dvds 16336 df-gcd 16578 df-phi 16850 df-0g 17519 df-mgm 18723 df-sgrp 18806 df-mnd 18822 df-grp 19034 df-minusg 19035 df-sbg 19036 df-mulg 19165 df-od 19629

This theorem is used by: unitscyglem3 43005

W3C validator