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 42310

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 5096	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑘 → (𝑎 ∥ 𝐷 ↔ 𝑘 ∥ 𝐷))
2	1	elrab 3643	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ↔ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷))
3	2	biimpi 216	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷))
4	3	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷))
5	4	simpld 494	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ (1...(𝐷 − 1)))
6	5	elfzelzd 13427	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℤ)
7		unitscyglem2.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ)
8	7	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℕ)
9	8	nnzd 12501	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℤ)
10		unitscyglem1.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ Fin)
11		hashcl 14265	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ₀)
12	10, 11	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ₀)
13	12	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘𝐵) ∈ ℕ₀)
14	13	nn0zd 12500	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘𝐵) ∈ ℤ)
15	4	simprd 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∥ 𝐷)
16		unitscyglem2.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∥ (♯‘𝐵))
17	16	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∥ (♯‘𝐵))
18	6, 9, 14, 15, 17	dvdstrd 16208	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∥ (♯‘𝐵))
19		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → 𝜑)
20	2, 5	sylan2br 595	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → 𝑘 ∈ (1...(𝐷 − 1)))
21	19, 20	jca 511	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → (𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))))
22	2, 15	sylan2br 595	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → 𝑘 ∥ 𝐷)
23	21, 22	jca 511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷))
24		fveqeq2 6837	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ((𝐷 / 𝑘) ↑ 𝐴) → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘))
25		unitscyglem1.1	. . . . . . . . . . . . . . . 16 ⊢ 𝐵 = (Base‘𝐺)
26		unitscyglem1.2	. . . . . . . . . . . . . . . 16 ⊢ ↑ = (._g‘𝐺)
27		unitscyglem1.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐺 ∈ Grp)
28	27	ad4antr 732	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐺 ∈ Grp)
29		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝑙 · 𝑘) = 𝐷)
30	29	eqcomd 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (𝑙 · 𝑘))
31	30	oveq1d 7367	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) = ((𝑙 · 𝑘) / 𝑘))
32		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑙 ∈ ℕ)
33	32	nncnd 12148	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑙 ∈ ℂ)
34		elfzelz 13426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 𝑘 ∈ ℤ)
35	34	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 𝑘 ∈ ℤ)
36	35	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℤ)
37	36	zcnd 12584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℂ)
38		elfzle1 13429	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 1 ≤ 𝑘)
39	38	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 1 ≤ 𝑘)
40	35, 39	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
41		elnnz1 12504	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
42	40, 41	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 𝑘 ∈ ℕ)
43	42	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → 𝑘 ∈ ℕ)
44	43	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℕ)
45	44	nnne0d 12182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ≠ 0)
46	33, 37, 45	divcan4d 11910	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝑙 · 𝑘) / 𝑘) = 𝑙)
47	31, 46	eqtrd 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) = 𝑙)
48	47, 32	eqeltrd 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℕ)
49	48	nnnn0d 12449	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℕ₀)
50	49	nn0zd 12500	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℤ)
51		unitscyglem2.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
52	51	ad4antr 732	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐴 ∈ 𝐵)
53	25, 26, 28, 50, 52	mulgcld 19011	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) ↑ 𝐴) ∈ 𝐵)
54	7	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → 𝐷 ∈ ℕ)
55	54	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ∈ ℕ)
56	55	nncnd 12148	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ∈ ℂ)
57	56, 37, 45	divcan1d 11905	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) · 𝑘) = 𝐷)
58		unitscyglem2.4	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((od‘𝐺)‘𝐴) = 𝐷)
59	58	ad4antr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘𝐴) = 𝐷)
60	59	eqcomd 2739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = ((od‘𝐺)‘𝐴))
61		eqid 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (od‘𝐺) = (od‘𝐺)
62	25, 61, 26	odmulg 19470	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ (𝐷 / 𝑘) ∈ ℤ) → ((od‘𝐺)‘𝐴) = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
63	28, 52, 50, 62	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘𝐴) = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
64	60, 63	eqtrd 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
65	59	oveq2d 7368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) = ((𝐷 / 𝑘) gcd 𝐷))
66	56, 37, 45	divcan2d 11906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝑘 · (𝐷 / 𝑘)) = 𝐷)
67	66	eqcomd 2739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (𝑘 · (𝐷 / 𝑘)))
68	67	oveq2d 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd 𝐷) = ((𝐷 / 𝑘) gcd (𝑘 · (𝐷 / 𝑘))))
69	49, 36	gcdmultipled 16447	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd (𝑘 · (𝐷 / 𝑘))) = (𝐷 / 𝑘))
70	68, 69	eqtrd 2768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd 𝐷) = (𝐷 / 𝑘))
71	65, 70	eqtrd 2768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) = (𝐷 / 𝑘))
72	71	oveq1d 7367	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
73	64, 72	eqtrd 2768	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
74	57, 73	eqtr2d 2769	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · 𝑘))
75	25, 61, 53	odcld 19466	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) ∈ ℕ₀)
76	75	nn0cnd 12451	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) ∈ ℂ)
77	50	zcnd 12584	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℂ)
78	55	nnne0d 12182	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ≠ 0)
79	56, 37, 78, 45	divne0d 11920	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ≠ 0)
80	76, 37, 77, 79	mulcand 11757	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · 𝑘) ↔ ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘))
81	74, 80	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘)
82	24, 53, 81	elrabd 3645	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) ↑ 𝐴) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
83	82	ne0d 4291	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
84		nndivides 16175	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑘 ∥ 𝐷 ↔ ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷))
85	43, 54, 84	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → (𝑘 ∥ 𝐷 ↔ ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷))
86	85	biimpd 229	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → (𝑘 ∥ 𝐷 → ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷))
87	86	syldbl2 841	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → ∃𝑙 ∈ ℕ (𝑙 · 𝑘) = 𝐷)
88	83, 87	r19.29a 3141	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
89	23, 88	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷)) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
90	89	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
91	90	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ((𝑘 ∈ (1...(𝐷 − 1)) ∧ 𝑘 ∥ 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
92	4, 91	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
93	18, 92	jca 511	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
94	5, 38	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 1 ≤ 𝑘)
95	6, 94	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
96	95, 41	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℕ)
97	96	nnred 12147	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℝ)
98	8	nnred 12147	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℝ)
99		1red 11120	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 1 ∈ ℝ)
100	98, 99	resubcld 11552	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝐷 − 1) ∈ ℝ)
101		elfzle2 13430	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 𝑘 ≤ (𝐷 − 1))
102	5, 101	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ≤ (𝐷 − 1))
103	98	ltm1d 12061	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝐷 − 1) < 𝐷)
104	97, 100, 98, 102, 103	lelttrd 11278	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 < 𝐷)
105		breq1 5096	. . . . . . . . . 10 ⊢ (𝑐 = 𝑘 → (𝑐 < 𝐷 ↔ 𝑘 < 𝐷))
106		breq1 5096	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (𝑐 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
107		eqeq2 2745	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑘 → (((od‘𝐺)‘𝑥) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑘))
108	107	rabbidv 3403	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑘 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
109	108	neeq1d 2988	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
110	106, 109	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑘 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)))
111	108	fveq2d 6832	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
112		fveq2 6828	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (ϕ‘𝑐) = (ϕ‘𝑘))
113	111, 112	eqeq12d 2749	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑘 → ((♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
114	110, 113	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑐 = 𝑘 → (((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐)) ↔ ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))))
115	105, 114	imbi12d 344	. . . . . . . . 9 ⊢ (𝑐 = 𝑘 → ((𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))) ↔ (𝑘 < 𝐷 → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))))
116		unitscyglem2.5	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑐 ∈ ℕ (𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
117	116	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ∀𝑐 ∈ ℕ (𝑐 < 𝐷 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (ϕ‘𝑐))))
118	115, 117, 96	rspcdva 3574	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝑘 < 𝐷 → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))))
119	104, 118	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ((𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘)))
120	93, 119	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (ϕ‘𝑘))
121	120	sumeq2dv 15611	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
122	121	eqcomd 2739	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
123	122	oveq1d 7367	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})))
124		elun 4102	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) ↔ (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
125	124	biimpi 216	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
126	125	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
127		1zzd 12509	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ∈ ℤ)
128	7	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℕ)
129	128	nnzd 12501	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℤ)
130		elfzelz 13426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 𝑎 ∈ ℤ)
131	130	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 𝑎 ∈ ℤ)
132	131	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℤ)
133		elfzle1 13429	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 1 ≤ 𝑎)
134	133	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 1 ≤ 𝑎)
135	134	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ≤ 𝑎)
136	132	zred 12583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℝ)
137	128	nnred 12147	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℝ)
138		1red 11120	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ∈ ℝ)
139	137, 138	resubcld 11552	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → (𝐷 − 1) ∈ ℝ)
140		elfzle2 13430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 𝑎 ≤ (𝐷 − 1))
141	140	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 𝑎 ≤ (𝐷 − 1))
142	141	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ≤ (𝐷 − 1))
143	137	ltm1d 12061	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → (𝐷 − 1) < 𝐷)
144	136, 139, 137, 142, 143	lelttrd 11278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 < 𝐷)
145	136, 137, 144	ltled 11268	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ≤ 𝐷)
146	127, 129, 132, 135, 145	elfzd 13417	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ (1...𝐷))
147	146	rabss3d 4030	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
148	147	sseld 3929	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
149	148	imp 406	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
150		elsni 4592	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝐷} → 𝑦 = 𝐷)
151	150	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → 𝑦 = 𝐷)
152		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝑦 = 𝐷)
153		breq1 5096	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝐷 → (𝑎 ∥ 𝐷 ↔ 𝐷 ∥ 𝐷))
154		1zzd 12509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℤ)
155	7	nnzd 12501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℤ)
156	7	nnge1d 12180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ 𝐷)
157	7	nnred 12147	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐷 ∈ ℝ)
158	157	leidd 11690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ≤ 𝐷)
159	154, 155, 155, 156, 158	elfzd 13417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∈ (1...𝐷))
160		iddvds 16182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ ℤ → 𝐷 ∥ 𝐷)
161	155, 160	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∥ 𝐷)
162	153, 159, 161	elrabd 3645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
163	162	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝐷 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
164	152, 163	eqeltrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
165	164	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑦 = 𝐷 → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
166	165	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → (𝑦 = 𝐷 → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
167	151, 166	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
168	149, 167	jaodan 959	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷})) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
169	168	ex 412	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
170	169	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) → ((𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
171	126, 170	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
172	171	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
173		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝑦 = 𝐷)
174		eqidd 2734	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 = 𝐷)
175	7	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 ∈ ℕ)
176		elsng 4589	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℕ → (𝐷 ∈ {𝐷} ↔ 𝐷 = 𝐷))
177	175, 176	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → (𝐷 ∈ {𝐷} ↔ 𝐷 = 𝐷))
178	174, 177	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 ∈ {𝐷})
179	173, 178	eqeltrd 2833	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝑦 ∈ {𝐷})
180	179	olcd 874	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
181		breq1 5096	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑦 → (𝑎 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷))
182	181	elrab 3643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} ↔ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷))
183	182	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} → (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷))
184	183	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷))
185	184	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷))
186		1zzd 12509	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 1 ∈ ℤ)
187	155	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℤ)
188	187, 186	zsubcld 12588	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝐷 − 1) ∈ ℤ)
189		elfzelz 13426	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝐷) → 𝑦 ∈ ℤ)
190	189	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ∈ ℤ)
191	190	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ ℤ)
192		elfzle1 13429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝐷) → 1 ≤ 𝑦)
193	192	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 1 ≤ 𝑦)
194	193	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 1 ≤ 𝑦)
195		elfzle2 13430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝐷) → 𝑦 ≤ 𝐷)
196	195	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ≤ 𝐷)
197	196	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ≤ 𝐷)
198		neqne 2937	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑦 = 𝐷 → 𝑦 ≠ 𝐷)
199	198	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝑦 ≠ 𝐷)
200	199	necomd 2984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝐷 ≠ 𝑦)
201	200	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ≠ 𝑦)
202	197, 201	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦))
203	191	zred 12583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ ℝ)
204	157	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℝ)
205	203, 204	ltlend 11265	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 < 𝐷 ↔ (𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦)))
206	202, 205	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 < 𝐷)
207	7	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℕ)
208	207	nnzd 12501	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℤ)
209	191, 208	zltlem1d 12532	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 < 𝐷 ↔ 𝑦 ≤ (𝐷 − 1)))
210	206, 209	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ≤ (𝐷 − 1))
211	186, 188, 191, 194, 210	elfzd 13417	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ (1...(𝐷 − 1)))
212		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∥ 𝐷)
213	181, 211, 212	elrabd 3645	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})
214	213	ex 412	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}))
215	185, 214	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})
216	215	orcd 873	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
217	180, 216	pm2.61dan 812	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
218	217, 124	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}))
219	218	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})))
220	172, 219	impbid 212	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) ↔ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
221	220	eqrdv 2731	. . . . . . 7 ⊢ (𝜑 → ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) = {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
222	221	sumeq1d 15609	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
223		phisum 16704	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = 𝐷)
224	7, 223	syl 17	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = 𝐷)
225		eqcom 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (((od‘𝐺)‘𝐴) = 𝐷 ↔ 𝐷 = ((od‘𝐺)‘𝐴))
226	225	imbi2i 336	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 → ((od‘𝐺)‘𝐴) = 𝐷) ↔ (𝜑 → 𝐷 = ((od‘𝐺)‘𝐴)))
227	58, 226	mpbi 230	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 = ((od‘𝐺)‘𝐴))
228	227	oveq1d 7367	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 ↑ 𝑥) = (((od‘𝐺)‘𝐴) ↑ 𝑥))
229	228	eqeq1d 2735	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 ↑ 𝑥) = (0_g‘𝐺) ↔ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)))
230	229	rabbidv 3403	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)} = {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)})
231	230	fveq2d 6832	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}) = (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)}))
232		unitscyglem1.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0_g‘𝐺)}) ≤ 𝑛)
233	25, 26, 27, 10, 232, 51	unitscyglem1 42309	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)}) = ((od‘𝐺)‘𝐴))
234	231, 233	eqtrd 2768	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}) = ((od‘𝐺)‘𝐴))
235	234, 58	eqtr2d 2769	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 = (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}))
236	25, 26, 27, 10, 7	grpods 42308	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}))
237	235, 236	eqtr4d 2771	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
238	221	eqcomd 2739	. . . . . . . . . 10 ⊢ (𝜑 → {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} = ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}))
239	238	sumeq1d 15609	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
240	237, 239	eqtrd 2768	. . . . . . . 8 ⊢ (𝜑 → 𝐷 = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
241	224, 240	eqtr2d 2769	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
242		1zzd 12509	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 1 ∈ ℤ)
243	155	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℤ)
244	181	elrab 3643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} ↔ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
245	244	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} → (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
246	245	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
247	246	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ℕ)
248	247	nnzd 12501	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ℤ)
249	247	nnge1d 12180	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 1 ≤ 𝑦)
250	246	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∥ 𝐷)
251	7	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℕ)
252		dvdsle 16223	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
253	248, 251, 252	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
254	250, 253	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ≤ 𝐷)
255	242, 243, 248, 249, 254	elfzd 13417	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ (1...𝐷))
256	181, 255, 250	elrabd 3645	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
257	256	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
258		elfzelz 13426	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (1...𝐷) → 𝑎 ∈ ℤ)
259		elfzle1 13429	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (1...𝐷) → 1 ≤ 𝑎)
260	258, 259	jca 511	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (1...𝐷) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
261	260	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
262	261	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷)) → (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
263		elnnz1 12504	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
264	262, 263	sylibr 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℕ)
265	264	rabss3d 4030	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} ⊆ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷})
266	265	sseld 3929	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}))
267	257, 266	impbid 212	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} ↔ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
268	267	eqrdv 2731	. . . . . . . 8 ⊢ (𝜑 → {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} = {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
269	268	sumeq1d 15609	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
270	241, 269	eqtr2d 2769	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
271	222, 270	eqtrd 2768	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
272		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑘𝜑
273		nfcv 2895	. . . . . 6 ⊢ Ⅎ𝑘(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
274		fzfid 13882	. . . . . . 7 ⊢ (𝜑 → (1...(𝐷 − 1)) ∈ Fin)
275		ssrab2 4029	. . . . . . . 8 ⊢ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ (1...(𝐷 − 1))
276	275	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ (1...(𝐷 − 1)))
277	274, 276	ssfid 9160	. . . . . 6 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∈ Fin)
278	153	elrab 3643	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ↔ (𝐷 ∈ (1...(𝐷 − 1)) ∧ 𝐷 ∥ 𝐷))
279	278	biimpi 216	. . . . . . . . . . 11 ⊢ (𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → (𝐷 ∈ (1...(𝐷 − 1)) ∧ 𝐷 ∥ 𝐷))
280	279	simpld 494	. . . . . . . . . 10 ⊢ (𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → 𝐷 ∈ (1...(𝐷 − 1)))
281	280	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ (1...(𝐷 − 1)))
282		elfzle2 13430	. . . . . . . . 9 ⊢ (𝐷 ∈ (1...(𝐷 − 1)) → 𝐷 ≤ (𝐷 − 1))
283	281, 282	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ≤ (𝐷 − 1))
284	157	ltm1d 12061	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 − 1) < 𝐷)
285		1red 11120	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℝ)
286	157, 285	resubcld 11552	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 − 1) ∈ ℝ)
287	286, 157	ltnled 11267	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷 − 1) < 𝐷 ↔ ¬ 𝐷 ≤ (𝐷 − 1)))
288	284, 287	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝐷 ≤ (𝐷 − 1))
289	288	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ¬ 𝐷 ≤ (𝐷 − 1))
290	283, 289	pm2.21dd 195	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})
291		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})
292	290, 291	pm2.61dan 812	. . . . . 6 ⊢ (𝜑 → ¬ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷})
293	10	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐵 ∈ Fin)
294		ssrab2 4029	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵
295	294	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
296	293, 295	ssfid 9160	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
297		hashcl 14265	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ₀)
298	296, 297	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ₀)
299	298	nn0cnd 12451	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℂ)
300		eqeq2 2745	. . . . . . . 8 ⊢ (𝑘 = 𝐷 → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
301	300	rabbidv 3403	. . . . . . 7 ⊢ (𝑘 = 𝐷 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
302	301	fveq2d 6832	. . . . . 6 ⊢ (𝑘 = 𝐷 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))
303		ssrab2 4029	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ⊆ 𝐵
304	303	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ⊆ 𝐵)
305	10, 304	ssfid 9160	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ∈ Fin)
306		hashcl 14265	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℕ₀)
307	305, 306	syl 17	. . . . . . 7 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℕ₀)
308	307	nn0cnd 12451	. . . . . 6 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℂ)
309	272, 273, 277, 7, 292, 299, 302, 308	fsumsplitsn 15653	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})))
310	271, 309	eqtr2d 2769	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘))
311		nfcv 2895	. . . . 5 ⊢ Ⅎ𝑘(ϕ‘𝐷)
312	120, 299	eqeltrrd 2834	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (ϕ‘𝑘) ∈ ℂ)
313		fveq2 6828	. . . . 5 ⊢ (𝑘 = 𝐷 → (ϕ‘𝑘) = (ϕ‘𝐷))
314	7	phicld 16685	. . . . . 6 ⊢ (𝜑 → (ϕ‘𝐷) ∈ ℕ)
315	314	nncnd 12148	. . . . 5 ⊢ (𝜑 → (ϕ‘𝐷) ∈ ℂ)
316	272, 311, 277, 7, 292, 312, 313, 315	fsumsplitsn 15653	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
317	310, 316	eqtrd 2768	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
318	123, 317	eqtrd 2768	. 2 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
319	277, 312	fsumcl 15642	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) ∈ ℂ)
320	319, 308, 315	addcand 11323	. 2 ⊢ (𝜑 → ((Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)) ↔ (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷)))
321	318, 320	mpbid 232	1 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) = (ϕ‘𝐷))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 ∀wral 3048 ∃wrex 3057 {crab 3396 ∪ cun 3896 ⊆ wss 3898 ∅c0 4282 {csn 4575 class class class wbr 5093 ‘cfv 6486 (class class class)co 7352 Fincfn 8875 ℂcc 11011 ℝcr 11012 1c1 11014 + caddc 11016 · cmul 11018 < clt 11153 ≤ cle 11154 − cmin 11351 / cdiv 11781 ℕcn 12132 ℕ₀cn0 12388 ℤcz 12475 ...cfz 13409 ♯chash 14239 Σcsu 15595 ∥ cdvds 16165 gcd cgcd 16407 ϕcphi 16677 Basecbs 17122 0_gc0g 17345 Grpcgrp 18848 ._gcmg 18982 odcod 19438

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-inf2 9538 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090 ax-pre-sup 11091

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-disj 5061 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-om 7803 df-1st 7927 df-2nd 7928 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-oadd 8395 df-omul 8396 df-er 8628 df-map 8758 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-sup 9333 df-inf 9334 df-oi 9403 df-card 9839 df-acn 9842 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-div 11782 df-nn 12133 df-2 12195 df-3 12196 df-n0 12389 df-xnn0 12462 df-z 12476 df-uz 12739 df-rp 12893 df-fz 13410 df-fzo 13557 df-fl 13698 df-mod 13776 df-seq 13911 df-exp 13971 df-hash 14240 df-cj 15008 df-re 15009 df-im 15010 df-sqrt 15144 df-abs 15145 df-clim 15397 df-sum 15596 df-dvds 16166 df-gcd 16408 df-phi 16679 df-0g 17347 df-mgm 18550 df-sgrp 18629 df-mnd 18645 df-grp 18851 df-minusg 18852 df-sbg 18853 df-mulg 18983 df-od 19442

This theorem is referenced by: unitscyglem3 42311

W3C validator