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 42214

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 5127	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑘 → (𝑎 ∥ 𝐷 ↔ 𝑘 ∥ 𝐷))
2	1	elrab 3676	. . . . . . . . . . . . 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 13547	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℤ)
7		unitscyglem2.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ)
8	7	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℕ)
9	8	nnzd 12620	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℤ)
10		unitscyglem1.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ Fin)
11		hashcl 14379	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ₀)
12	10, 11	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ₀)
13	12	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘𝐵) ∈ ℕ₀)
14	13	nn0zd 12619	. . . . . . . . 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 16319	. . . . . . . 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 6890	. . . . . . . . . . . . . . 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 2742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (𝑙 · 𝑘))
31	30	oveq1d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) = ((𝑙 · 𝑘) / 𝑘))
32		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑙 ∈ ℕ)
33	32	nncnd 12261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑙 ∈ ℂ)
34		elfzelz 13546	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 𝑘 ∈ ℤ)
35	34	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 𝑘 ∈ ℤ)
36	35	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℤ)
37	36	zcnd 12703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℂ)
38		elfzle1 13549	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 1 ≤ 𝑘)
39	38	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 1 ≤ 𝑘)
40	35, 39	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
41		elnnz1 12623	. . . . . . . . . . . . . . . . . . . . . . . . 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 12295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ≠ 0)
46	33, 37, 45	divcan4d 12028	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝑙 · 𝑘) / 𝑘) = 𝑙)
47	31, 46	eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) = 𝑙)
48	47, 32	eqeltrd 2835	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℕ)
49	48	nnnn0d 12567	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℕ₀)
50	49	nn0zd 12619	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℤ)
51		unitscyglem2.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
52	51	ad4antr 732	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐴 ∈ 𝐵)
53	25, 26, 28, 50, 52	mulgcld 19084	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) ↑ 𝐴) ∈ 𝐵)
54	7	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → 𝐷 ∈ ℕ)
55	54	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ∈ ℕ)
56	55	nncnd 12261	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ∈ ℂ)
57	56, 37, 45	divcan1d 12023	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) · 𝑘) = 𝐷)
58		unitscyglem2.4	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((od‘𝐺)‘𝐴) = 𝐷)
59	58	ad4antr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘𝐴) = 𝐷)
60	59	eqcomd 2742	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = ((od‘𝐺)‘𝐴))
61		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (od‘𝐺) = (od‘𝐺)
62	25, 61, 26	odmulg 19542	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ (𝐷 / 𝑘) ∈ ℤ) → ((od‘𝐺)‘𝐴) = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
63	28, 52, 50, 62	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘𝐴) = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
64	60, 63	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
65	59	oveq2d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) = ((𝐷 / 𝑘) gcd 𝐷))
66	56, 37, 45	divcan2d 12024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝑘 · (𝐷 / 𝑘)) = 𝐷)
67	66	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (𝑘 · (𝐷 / 𝑘)))
68	67	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd 𝐷) = ((𝐷 / 𝑘) gcd (𝑘 · (𝐷 / 𝑘))))
69	49, 36	gcdmultipled 16558	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd (𝑘 · (𝐷 / 𝑘))) = (𝐷 / 𝑘))
70	68, 69	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd 𝐷) = (𝐷 / 𝑘))
71	65, 70	eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) = (𝐷 / 𝑘))
72	71	oveq1d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
73	64, 72	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
74	57, 73	eqtr2d 2772	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · 𝑘))
75	25, 61, 53	odcld 19538	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) ∈ ℕ₀)
76	75	nn0cnd 12569	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) ∈ ℂ)
77	50	zcnd 12703	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℂ)
78	55	nnne0d 12295	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ≠ 0)
79	56, 37, 78, 45	divne0d 12038	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ≠ 0)
80	76, 37, 77, 79	mulcand 11875	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · 𝑘) ↔ ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘))
81	74, 80	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘)
82	24, 53, 81	elrabd 3678	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) ↑ 𝐴) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
83	82	ne0d 4322	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
84		nndivides 16287	. . . . . . . . . . . . . . . 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 3149	. . . . . . . . . . . 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 12260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℝ)
98	8	nnred 12260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℝ)
99		1red 11241	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 1 ∈ ℝ)
100	98, 99	resubcld 11670	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝐷 − 1) ∈ ℝ)
101		elfzle2 13550	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 𝑘 ≤ (𝐷 − 1))
102	5, 101	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ≤ (𝐷 − 1))
103	98	ltm1d 12179	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝐷 − 1) < 𝐷)
104	97, 100, 98, 102, 103	lelttrd 11398	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 < 𝐷)
105		breq1 5127	. . . . . . . . . 10 ⊢ (𝑐 = 𝑘 → (𝑐 < 𝐷 ↔ 𝑘 < 𝐷))
106		breq1 5127	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (𝑐 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
107		eqeq2 2748	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑘 → (((od‘𝐺)‘𝑥) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑘))
108	107	rabbidv 3428	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑘 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
109	108	neeq1d 2992	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
110	106, 109	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑘 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)))
111	108	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
112		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (ϕ‘𝑐) = (ϕ‘𝑘))
113	111, 112	eqeq12d 2752	. . . . . . . . . . 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 3607	. . . . . . . 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 15723	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
122	121	eqcomd 2742	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
123	122	oveq1d 7425	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})))
124		elun 4133	. . . . . . . . . . . . 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 12628	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ∈ ℤ)
128	7	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℕ)
129	128	nnzd 12620	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℤ)
130		elfzelz 13546	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 𝑎 ∈ ℤ)
131	130	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 𝑎 ∈ ℤ)
132	131	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℤ)
133		elfzle1 13549	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 1 ≤ 𝑎)
134	133	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 1 ≤ 𝑎)
135	134	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ≤ 𝑎)
136	132	zred 12702	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℝ)
137	128	nnred 12260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℝ)
138		1red 11241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ∈ ℝ)
139	137, 138	resubcld 11670	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → (𝐷 − 1) ∈ ℝ)
140		elfzle2 13550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 𝑎 ≤ (𝐷 − 1))
141	140	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 𝑎 ≤ (𝐷 − 1))
142	141	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ≤ (𝐷 − 1))
143	137	ltm1d 12179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → (𝐷 − 1) < 𝐷)
144	136, 139, 137, 142, 143	lelttrd 11398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 < 𝐷)
145	136, 137, 144	ltled 11388	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ≤ 𝐷)
146	127, 129, 132, 135, 145	elfzd 13537	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ (1...𝐷))
147	146	rabss3d 4061	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
148	147	sseld 3962	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
149	148	imp 406	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
150		elsni 4623	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝐷} → 𝑦 = 𝐷)
151	150	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → 𝑦 = 𝐷)
152		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝑦 = 𝐷)
153		breq1 5127	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝐷 → (𝑎 ∥ 𝐷 ↔ 𝐷 ∥ 𝐷))
154		1zzd 12628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℤ)
155	7	nnzd 12620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℤ)
156	7	nnge1d 12293	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ 𝐷)
157	7	nnred 12260	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐷 ∈ ℝ)
158	157	leidd 11808	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ≤ 𝐷)
159	154, 155, 155, 156, 158	elfzd 13537	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∈ (1...𝐷))
160		iddvds 16294	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ ℤ → 𝐷 ∥ 𝐷)
161	155, 160	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∥ 𝐷)
162	153, 159, 161	elrabd 3678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
163	162	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝐷 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
164	152, 163	eqeltrd 2835	. . . . . . . . . . . . . . . . 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 2737	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 = 𝐷)
175	7	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 ∈ ℕ)
176		elsng 4620	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℕ → (𝐷 ∈ {𝐷} ↔ 𝐷 = 𝐷))
177	175, 176	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → (𝐷 ∈ {𝐷} ↔ 𝐷 = 𝐷))
178	174, 177	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 ∈ {𝐷})
179	173, 178	eqeltrd 2835	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝑦 ∈ {𝐷})
180	179	olcd 874	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
181		breq1 5127	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑦 → (𝑎 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷))
182	181	elrab 3676	. . . . . . . . . . . . . . . . 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 12628	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 1 ∈ ℤ)
187	155	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℤ)
188	187, 186	zsubcld 12707	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝐷 − 1) ∈ ℤ)
189		elfzelz 13546	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝐷) → 𝑦 ∈ ℤ)
190	189	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ∈ ℤ)
191	190	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ ℤ)
192		elfzle1 13549	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝐷) → 1 ≤ 𝑦)
193	192	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 1 ≤ 𝑦)
194	193	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 1 ≤ 𝑦)
195		elfzle2 13550	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝐷) → 𝑦 ≤ 𝐷)
196	195	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ≤ 𝐷)
197	196	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ≤ 𝐷)
198		neqne 2941	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑦 = 𝐷 → 𝑦 ≠ 𝐷)
199	198	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝑦 ≠ 𝐷)
200	199	necomd 2988	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝐷 ≠ 𝑦)
201	200	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ≠ 𝑦)
202	197, 201	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦))
203	191	zred 12702	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ ℝ)
204	157	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℝ)
205	203, 204	ltlend 11385	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 < 𝐷 ↔ (𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦)))
206	202, 205	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 < 𝐷)
207	7	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℕ)
208	207	nnzd 12620	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℤ)
209	191, 208	zltlem1d 12651	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 < 𝐷 ↔ 𝑦 ≤ (𝐷 − 1)))
210	206, 209	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ≤ (𝐷 − 1))
211	186, 188, 191, 194, 210	elfzd 13537	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ (1...(𝐷 − 1)))
212		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∥ 𝐷)
213	181, 211, 212	elrabd 3678	. . . . . . . . . . . . . . 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 2734	. . . . . . 7 ⊢ (𝜑 → ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) = {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
222	221	sumeq1d 15721	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
223		phisum 16815	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = 𝐷)
224	7, 223	syl 17	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = 𝐷)
225		eqcom 2743	. . . . . . . . . . . . . . . . . 18 ⊢ (((od‘𝐺)‘𝐴) = 𝐷 ↔ 𝐷 = ((od‘𝐺)‘𝐴))
226	225	imbi2i 336	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 → ((od‘𝐺)‘𝐴) = 𝐷) ↔ (𝜑 → 𝐷 = ((od‘𝐺)‘𝐴)))
227	58, 226	mpbi 230	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 = ((od‘𝐺)‘𝐴))
228	227	oveq1d 7425	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 ↑ 𝑥) = (((od‘𝐺)‘𝐴) ↑ 𝑥))
229	228	eqeq1d 2738	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 ↑ 𝑥) = (0_g‘𝐺) ↔ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)))
230	229	rabbidv 3428	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)} = {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)})
231	230	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}) = (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)}))
232		unitscyglem1.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0_g‘𝐺)}) ≤ 𝑛)
233	25, 26, 27, 10, 232, 51	unitscyglem1 42213	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)}) = ((od‘𝐺)‘𝐴))
234	231, 233	eqtrd 2771	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}) = ((od‘𝐺)‘𝐴))
235	234, 58	eqtr2d 2772	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 = (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}))
236	25, 26, 27, 10, 7	grpods 42212	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}))
237	235, 236	eqtr4d 2774	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
238	221	eqcomd 2742	. . . . . . . . . 10 ⊢ (𝜑 → {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} = ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}))
239	238	sumeq1d 15721	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
240	237, 239	eqtrd 2771	. . . . . . . 8 ⊢ (𝜑 → 𝐷 = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
241	224, 240	eqtr2d 2772	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
242		1zzd 12628	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 1 ∈ ℤ)
243	155	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℤ)
244	181	elrab 3676	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} ↔ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
245	244	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} → (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
246	245	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
247	246	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ℕ)
248	247	nnzd 12620	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ℤ)
249	247	nnge1d 12293	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 1 ≤ 𝑦)
250	246	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∥ 𝐷)
251	7	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℕ)
252		dvdsle 16334	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
253	248, 251, 252	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
254	250, 253	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ≤ 𝐷)
255	242, 243, 248, 249, 254	elfzd 13537	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ (1...𝐷))
256	181, 255, 250	elrabd 3678	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
257	256	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
258		elfzelz 13546	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (1...𝐷) → 𝑎 ∈ ℤ)
259		elfzle1 13549	. . . . . . . . . . . . . . . 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 12623	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
264	262, 263	sylibr 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℕ)
265	264	rabss3d 4061	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} ⊆ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷})
266	265	sseld 3962	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}))
267	257, 266	impbid 212	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} ↔ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
268	267	eqrdv 2734	. . . . . . . 8 ⊢ (𝜑 → {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} = {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
269	268	sumeq1d 15721	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
270	241, 269	eqtr2d 2772	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
271	222, 270	eqtrd 2771	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
272		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑘𝜑
273		nfcv 2899	. . . . . 6 ⊢ Ⅎ𝑘(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
274		fzfid 13996	. . . . . . 7 ⊢ (𝜑 → (1...(𝐷 − 1)) ∈ Fin)
275		ssrab2 4060	. . . . . . . 8 ⊢ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ (1...(𝐷 − 1))
276	275	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ (1...(𝐷 − 1)))
277	274, 276	ssfid 9278	. . . . . 6 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∈ Fin)
278	153	elrab 3676	. . . . . . . . . . . 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 13550	. . . . . . . . 9 ⊢ (𝐷 ∈ (1...(𝐷 − 1)) → 𝐷 ≤ (𝐷 − 1))
283	281, 282	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ≤ (𝐷 − 1))
284	157	ltm1d 12179	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 − 1) < 𝐷)
285		1red 11241	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℝ)
286	157, 285	resubcld 11670	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 − 1) ∈ ℝ)
287	286, 157	ltnled 11387	. . . . . . . . . 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 4060	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵
295	294	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
296	293, 295	ssfid 9278	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
297		hashcl 14379	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ₀)
298	296, 297	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ₀)
299	298	nn0cnd 12569	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℂ)
300		eqeq2 2748	. . . . . . . 8 ⊢ (𝑘 = 𝐷 → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
301	300	rabbidv 3428	. . . . . . 7 ⊢ (𝑘 = 𝐷 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
302	301	fveq2d 6885	. . . . . 6 ⊢ (𝑘 = 𝐷 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))
303		ssrab2 4060	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ⊆ 𝐵
304	303	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ⊆ 𝐵)
305	10, 304	ssfid 9278	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ∈ Fin)
306		hashcl 14379	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℕ₀)
307	305, 306	syl 17	. . . . . . 7 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℕ₀)
308	307	nn0cnd 12569	. . . . . 6 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℂ)
309	272, 273, 277, 7, 292, 299, 302, 308	fsumsplitsn 15765	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})))
310	271, 309	eqtr2d 2772	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘))
311		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑘(ϕ‘𝐷)
312	120, 299	eqeltrrd 2836	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (ϕ‘𝑘) ∈ ℂ)
313		fveq2 6881	. . . . 5 ⊢ (𝑘 = 𝐷 → (ϕ‘𝑘) = (ϕ‘𝐷))
314	7	phicld 16796	. . . . . 6 ⊢ (𝜑 → (ϕ‘𝐷) ∈ ℕ)
315	314	nncnd 12261	. . . . 5 ⊢ (𝜑 → (ϕ‘𝐷) ∈ ℂ)
316	272, 311, 277, 7, 292, 312, 313, 315	fsumsplitsn 15765	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
317	310, 316	eqtrd 2771	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
318	123, 317	eqtrd 2771	. 2 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
319	277, 312	fsumcl 15754	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) ∈ ℂ)
320	319, 308, 315	addcand 11443	. 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 1540 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 {crab 3420 ∪ cun 3929 ⊆ wss 3931 ∅c0 4313 {csn 4606 class class class wbr 5124 ‘cfv 6536 (class class class)co 7410 Fincfn 8964 ℂcc 11132 ℝcr 11133 1c1 11135 + caddc 11137 · cmul 11139 < clt 11274 ≤ cle 11275 − cmin 11471 / cdiv 11899 ℕcn 12245 ℕ₀cn0 12506 ℤcz 12593 ...cfz 13529 ♯chash 14353 Σcsu 15707 ∥ cdvds 16277 gcd cgcd 16518 ϕcphi 16788 Basecbs 17233 0_gc0g 17458 Grpcgrp 18921 ._gcmg 19055 odcod 19510

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-inf2 9660 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-disj 5092 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-oadd 8489 df-omul 8490 df-er 8724 df-map 8847 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-sup 9459 df-inf 9460 df-oi 9529 df-card 9958 df-acn 9961 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-n0 12507 df-xnn0 12580 df-z 12594 df-uz 12858 df-rp 13014 df-fz 13530 df-fzo 13677 df-fl 13814 df-mod 13892 df-seq 14025 df-exp 14085 df-hash 14354 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-clim 15509 df-sum 15708 df-dvds 16278 df-gcd 16519 df-phi 16790 df-0g 17460 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-grp 18924 df-minusg 18925 df-sbg 18926 df-mulg 19056 df-od 19514

This theorem is referenced by: unitscyglem3 42215

W3C validator