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 42191

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 5113	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑘 → (𝑎 ∥ 𝐷 ↔ 𝑘 ∥ 𝐷))
2	1	elrab 3662	. . . . . . . . . . . . 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 13493	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℤ)
7		unitscyglem2.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ)
8	7	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℕ)
9	8	nnzd 12563	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℤ)
10		unitscyglem1.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ Fin)
11		hashcl 14328	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ Fin → (♯‘𝐵) ∈ ℕ₀)
12	10, 11	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ₀)
13	12	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘𝐵) ∈ ℕ₀)
14	13	nn0zd 12562	. . . . . . . . 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 16272	. . . . . . . 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 6870	. . . . . . . . . . . . . . 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 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (𝑙 · 𝑘))
31	30	oveq1d 7405	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) = ((𝑙 · 𝑘) / 𝑘))
32		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑙 ∈ ℕ)
33	32	nncnd 12209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑙 ∈ ℂ)
34		elfzelz 13492	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 𝑘 ∈ ℤ)
35	34	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 𝑘 ∈ ℤ)
36	35	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℤ)
37	36	zcnd 12646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ∈ ℂ)
38		elfzle1 13495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 1 ≤ 𝑘)
39	38	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → 1 ≤ 𝑘)
40	35, 39	jca 511	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) → (𝑘 ∈ ℤ ∧ 1 ≤ 𝑘))
41		elnnz1 12566	. . . . . . . . . . . . . . . . . . . . . . . . 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 12243	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝑘 ≠ 0)
46	33, 37, 45	divcan4d 11971	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝑙 · 𝑘) / 𝑘) = 𝑙)
47	31, 46	eqtrd 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) = 𝑙)
48	47, 32	eqeltrd 2829	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℕ)
49	48	nnnn0d 12510	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℕ₀)
50	49	nn0zd 12562	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℤ)
51		unitscyglem2.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
52	51	ad4antr 732	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐴 ∈ 𝐵)
53	25, 26, 28, 50, 52	mulgcld 19035	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) ↑ 𝐴) ∈ 𝐵)
54	7	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) → 𝐷 ∈ ℕ)
55	54	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ∈ ℕ)
56	55	nncnd 12209	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ∈ ℂ)
57	56, 37, 45	divcan1d 11966	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) · 𝑘) = 𝐷)
58		unitscyglem2.4	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((od‘𝐺)‘𝐴) = 𝐷)
59	58	ad4antr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘𝐴) = 𝐷)
60	59	eqcomd 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = ((od‘𝐺)‘𝐴))
61		eqid 2730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (od‘𝐺) = (od‘𝐺)
62	25, 61, 26	odmulg 19493	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ∧ (𝐷 / 𝑘) ∈ ℤ) → ((od‘𝐺)‘𝐴) = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
63	28, 52, 50, 62	syl3anc 1373	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘𝐴) = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
64	60, 63	eqtrd 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
65	59	oveq2d 7406	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) = ((𝐷 / 𝑘) gcd 𝐷))
66	56, 37, 45	divcan2d 11967	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝑘 · (𝐷 / 𝑘)) = 𝐷)
67	66	eqcomd 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = (𝑘 · (𝐷 / 𝑘)))
68	67	oveq2d 7406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd 𝐷) = ((𝐷 / 𝑘) gcd (𝑘 · (𝐷 / 𝑘))))
69	49, 36	gcdmultipled 16511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd (𝑘 · (𝐷 / 𝑘))) = (𝐷 / 𝑘))
70	68, 69	eqtrd 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd 𝐷) = (𝐷 / 𝑘))
71	65, 70	eqtrd 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) = (𝐷 / 𝑘))
72	71	oveq1d 7405	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (((𝐷 / 𝑘) gcd ((od‘𝐺)‘𝐴)) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
73	64, 72	eqtrd 2765	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 = ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))))
74	57, 73	eqtr2d 2766	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · 𝑘))
75	25, 61, 53	odcld 19489	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) ∈ ℕ₀)
76	75	nn0cnd 12512	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) ∈ ℂ)
77	50	zcnd 12646	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ∈ ℂ)
78	55	nnne0d 12243	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → 𝐷 ≠ 0)
79	56, 37, 78, 45	divne0d 11981	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (𝐷 / 𝑘) ≠ 0)
80	76, 37, 77, 79	mulcand 11818	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → (((𝐷 / 𝑘) · ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴))) = ((𝐷 / 𝑘) · 𝑘) ↔ ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘))
81	74, 80	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((od‘𝐺)‘((𝐷 / 𝑘) ↑ 𝐴)) = 𝑘)
82	24, 53, 81	elrabd 3664	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → ((𝐷 / 𝑘) ↑ 𝐴) ∈ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
83	82	ne0d 4308	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ (1...(𝐷 − 1))) ∧ 𝑘 ∥ 𝐷) ∧ 𝑙 ∈ ℕ) ∧ (𝑙 · 𝑘) = 𝐷) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)
84		nndivides 16239	. . . . . . . . . . . . . . . 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 3142	. . . . . . . . . . . 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 12208	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ∈ ℝ)
98	8	nnred 12208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℝ)
99		1red 11182	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 1 ∈ ℝ)
100	98, 99	resubcld 11613	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝐷 − 1) ∈ ℝ)
101		elfzle2 13496	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...(𝐷 − 1)) → 𝑘 ≤ (𝐷 − 1))
102	5, 101	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 ≤ (𝐷 − 1))
103	98	ltm1d 12122	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (𝐷 − 1) < 𝐷)
104	97, 100, 98, 102, 103	lelttrd 11339	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑘 < 𝐷)
105		breq1 5113	. . . . . . . . . 10 ⊢ (𝑐 = 𝑘 → (𝑐 < 𝐷 ↔ 𝑘 < 𝐷))
106		breq1 5113	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (𝑐 ∥ (♯‘𝐵) ↔ 𝑘 ∥ (♯‘𝐵)))
107		eqeq2 2742	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑘 → (((od‘𝐺)‘𝑥) = 𝑐 ↔ ((od‘𝐺)‘𝑥) = 𝑘))
108	107	rabbidv 3416	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑘 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘})
109	108	neeq1d 2985	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅ ↔ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅))
110	106, 109	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑐 = 𝑘 → ((𝑐 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐} ≠ ∅) ↔ (𝑘 ∥ (♯‘𝐵) ∧ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ≠ ∅)))
111	108	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑐}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
112		fveq2 6861	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑘 → (ϕ‘𝑐) = (ϕ‘𝑘))
113	111, 112	eqeq12d 2746	. . . . . . . . . . 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 3592	. . . . . . . 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 15675	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
122	121	eqcomd 2736	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
123	122	oveq1d 7405	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})))
124		elun 4119	. . . . . . . . . . . . 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 12571	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ∈ ℤ)
128	7	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℕ)
129	128	nnzd 12563	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℤ)
130		elfzelz 13492	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 𝑎 ∈ ℤ)
131	130	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 𝑎 ∈ ℤ)
132	131	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℤ)
133		elfzle1 13495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 1 ≤ 𝑎)
134	133	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 1 ≤ 𝑎)
135	134	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ≤ 𝑎)
136	132	zred 12645	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℝ)
137	128	nnred 12208	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝐷 ∈ ℝ)
138		1red 11182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 1 ∈ ℝ)
139	137, 138	resubcld 11613	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → (𝐷 − 1) ∈ ℝ)
140		elfzle2 13496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 ∈ (1...(𝐷 − 1)) → 𝑎 ≤ (𝐷 − 1))
141	140	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷) → 𝑎 ≤ (𝐷 − 1))
142	141	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ≤ (𝐷 − 1))
143	137	ltm1d 12122	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → (𝐷 − 1) < 𝐷)
144	136, 139, 137, 142, 143	lelttrd 11339	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 < 𝐷)
145	136, 137, 144	ltled 11329	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ≤ 𝐷)
146	127, 129, 132, 135, 145	elfzd 13483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...(𝐷 − 1)) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ (1...𝐷))
147	146	rabss3d 4047	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
148	147	sseld 3948	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
149	148	imp 406	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
150		elsni 4609	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝐷} → 𝑦 = 𝐷)
151	150	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝐷}) → 𝑦 = 𝐷)
152		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝑦 = 𝐷)
153		breq1 5113	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 𝐷 → (𝑎 ∥ 𝐷 ↔ 𝐷 ∥ 𝐷))
154		1zzd 12571	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ∈ ℤ)
155	7	nnzd 12563	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ∈ ℤ)
156	7	nnge1d 12241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 1 ≤ 𝐷)
157	7	nnred 12208	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐷 ∈ ℝ)
158	157	leidd 11751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐷 ≤ 𝐷)
159	154, 155, 155, 156, 158	elfzd 13483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∈ (1...𝐷))
160		iddvds 16246	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ ℤ → 𝐷 ∥ 𝐷)
161	155, 160	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐷 ∥ 𝐷)
162	153, 159, 161	elrabd 3664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
163	162	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 = 𝐷) → 𝐷 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
164	152, 163	eqeltrd 2829	. . . . . . . . . . . . . . . . 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 2731	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 = 𝐷)
175	7	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 ∈ ℕ)
176		elsng 4606	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∈ ℕ → (𝐷 ∈ {𝐷} ↔ 𝐷 = 𝐷))
177	175, 176	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → (𝐷 ∈ {𝐷} ↔ 𝐷 = 𝐷))
178	174, 177	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝐷 ∈ {𝐷})
179	173, 178	eqeltrd 2829	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → 𝑦 ∈ {𝐷})
180	179	olcd 874	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ 𝑦 = 𝐷) → (𝑦 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∨ 𝑦 ∈ {𝐷}))
181		breq1 5113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 𝑦 → (𝑎 ∥ 𝐷 ↔ 𝑦 ∥ 𝐷))
182	181	elrab 3662	. . . . . . . . . . . . . . . . 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 12571	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 1 ∈ ℤ)
187	155	ad3antrrr 730	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℤ)
188	187, 186	zsubcld 12650	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝐷 − 1) ∈ ℤ)
189		elfzelz 13492	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝐷) → 𝑦 ∈ ℤ)
190	189	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ∈ ℤ)
191	190	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ ℤ)
192		elfzle1 13495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ (1...𝐷) → 1 ≤ 𝑦)
193	192	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 1 ≤ 𝑦)
194	193	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 1 ≤ 𝑦)
195		elfzle2 13496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝐷) → 𝑦 ≤ 𝐷)
196	195	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷) → 𝑦 ≤ 𝐷)
197	196	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ≤ 𝐷)
198		neqne 2934	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑦 = 𝐷 → 𝑦 ≠ 𝐷)
199	198	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝑦 ≠ 𝐷)
200	199	necomd 2981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) → 𝐷 ≠ 𝑦)
201	200	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ≠ 𝑦)
202	197, 201	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦))
203	191	zred 12645	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ ℝ)
204	157	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℝ)
205	203, 204	ltlend 11326	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 < 𝐷 ↔ (𝑦 ≤ 𝐷 ∧ 𝐷 ≠ 𝑦)))
206	202, 205	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 < 𝐷)
207	7	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℕ)
208	207	nnzd 12563	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝐷 ∈ ℤ)
209	191, 208	zltlem1d 12594	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → (𝑦 < 𝐷 ↔ 𝑦 ≤ (𝐷 − 1)))
210	206, 209	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ≤ (𝐷 − 1))
211	186, 188, 191, 194, 210	elfzd 13483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∈ (1...(𝐷 − 1)))
212		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}) ∧ ¬ 𝑦 = 𝐷) ∧ (𝑦 ∈ (1...𝐷) ∧ 𝑦 ∥ 𝐷)) → 𝑦 ∥ 𝐷)
213	181, 211, 212	elrabd 3664	. . . . . . . . . . . . . . 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 2728	. . . . . . 7 ⊢ (𝜑 → ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}) = {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
222	221	sumeq1d 15673	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
223		phisum 16768	. . . . . . . . 9 ⊢ (𝐷 ∈ ℕ → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = 𝐷)
224	7, 223	syl 17	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = 𝐷)
225		eqcom 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (((od‘𝐺)‘𝐴) = 𝐷 ↔ 𝐷 = ((od‘𝐺)‘𝐴))
226	225	imbi2i 336	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 → ((od‘𝐺)‘𝐴) = 𝐷) ↔ (𝜑 → 𝐷 = ((od‘𝐺)‘𝐴)))
227	58, 226	mpbi 230	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐷 = ((od‘𝐺)‘𝐴))
228	227	oveq1d 7405	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 ↑ 𝑥) = (((od‘𝐺)‘𝐴) ↑ 𝑥))
229	228	eqeq1d 2732	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 ↑ 𝑥) = (0_g‘𝐺) ↔ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)))
230	229	rabbidv 3416	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)} = {𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)})
231	230	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}) = (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)}))
232		unitscyglem1.5	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (♯‘{𝑥 ∈ 𝐵 ∣ (𝑛 ↑ 𝑥) = (0_g‘𝐺)}) ≤ 𝑛)
233	25, 26, 27, 10, 232, 51	unitscyglem1 42190	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (((od‘𝐺)‘𝐴) ↑ 𝑥) = (0_g‘𝐺)}) = ((od‘𝐺)‘𝐴))
234	231, 233	eqtrd 2765	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}) = ((od‘𝐺)‘𝐴))
235	234, 58	eqtr2d 2766	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 = (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}))
236	25, 26, 27, 10, 7	grpods 42189	. . . . . . . . . 10 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ (𝐷 ↑ 𝑥) = (0_g‘𝐺)}))
237	235, 236	eqtr4d 2768	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
238	221	eqcomd 2736	. . . . . . . . . 10 ⊢ (𝜑 → {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} = ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷}))
239	238	sumeq1d 15673	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
240	237, 239	eqtrd 2765	. . . . . . . 8 ⊢ (𝜑 → 𝐷 = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
241	224, 240	eqtr2d 2766	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
242		1zzd 12571	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 1 ∈ ℤ)
243	155	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℤ)
244	181	elrab 3662	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} ↔ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
245	244	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} → (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
246	245	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝐷))
247	246	simpld 494	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ℕ)
248	247	nnzd 12563	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ ℤ)
249	247	nnge1d 12241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 1 ≤ 𝑦)
250	246	simprd 495	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∥ 𝐷)
251	7	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝐷 ∈ ℕ)
252		dvdsle 16287	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
253	248, 251, 252	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → (𝑦 ∥ 𝐷 → 𝑦 ≤ 𝐷))
254	250, 253	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ≤ 𝐷)
255	242, 243, 248, 249, 254	elfzd 13483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ (1...𝐷))
256	181, 255, 250	elrabd 3664	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}) → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
257	256	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
258		elfzelz 13492	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (1...𝐷) → 𝑎 ∈ ℤ)
259		elfzle1 13495	. . . . . . . . . . . . . . . 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 12566	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ ↔ (𝑎 ∈ ℤ ∧ 1 ≤ 𝑎))
264	262, 263	sylibr 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑎 ∈ (1...𝐷) ∧ 𝑎 ∥ 𝐷)) → 𝑎 ∈ ℕ)
265	264	rabss3d 4047	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} ⊆ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷})
266	265	sseld 3948	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} → 𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷}))
267	257, 266	impbid 212	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} ↔ 𝑦 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷}))
268	267	eqrdv 2728	. . . . . . . 8 ⊢ (𝜑 → {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} = {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷})
269	268	sumeq1d 15673	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ ℕ ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘))
270	241, 269	eqtr2d 2766	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...𝐷) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
271	222, 270	eqtrd 2765	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}))
272		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑘𝜑
273		nfcv 2892	. . . . . 6 ⊢ Ⅎ𝑘(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
274		fzfid 13945	. . . . . . 7 ⊢ (𝜑 → (1...(𝐷 − 1)) ∈ Fin)
275		ssrab2 4046	. . . . . . . 8 ⊢ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ (1...(𝐷 − 1))
276	275	a1i 11	. . . . . . 7 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ⊆ (1...(𝐷 − 1)))
277	274, 276	ssfid 9219	. . . . . 6 ⊢ (𝜑 → {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∈ Fin)
278	153	elrab 3662	. . . . . . . . . . . 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 13496	. . . . . . . . 9 ⊢ (𝐷 ∈ (1...(𝐷 − 1)) → 𝐷 ≤ (𝐷 − 1))
283	281, 282	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → 𝐷 ≤ (𝐷 − 1))
284	157	ltm1d 12122	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 − 1) < 𝐷)
285		1red 11182	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℝ)
286	157, 285	resubcld 11613	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 − 1) ∈ ℝ)
287	286, 157	ltnled 11328	. . . . . . . . . 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 4046	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵
295	294	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ⊆ 𝐵)
296	293, 295	ssfid 9219	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin)
297		hashcl 14328	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ₀)
298	296, 297	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℕ₀)
299	298	nn0cnd 12512	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) ∈ ℂ)
300		eqeq2 2742	. . . . . . . 8 ⊢ (𝑘 = 𝐷 → (((od‘𝐺)‘𝑥) = 𝑘 ↔ ((od‘𝐺)‘𝑥) = 𝐷))
301	300	rabbidv 3416	. . . . . . 7 ⊢ (𝑘 = 𝐷 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘} = {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})
302	301	fveq2d 6865	. . . . . 6 ⊢ (𝑘 = 𝐷 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}))
303		ssrab2 4046	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ⊆ 𝐵
304	303	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ⊆ 𝐵)
305	10, 304	ssfid 9219	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ∈ Fin)
306		hashcl 14328	. . . . . . . 8 ⊢ ({𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷} ∈ Fin → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℕ₀)
307	305, 306	syl 17	. . . . . . 7 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℕ₀)
308	307	nn0cnd 12512	. . . . . 6 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷}) ∈ ℂ)
309	272, 273, 277, 7, 292, 299, 302, 308	fsumsplitsn 15717	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})))
310	271, 309	eqtr2d 2766	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘))
311		nfcv 2892	. . . . 5 ⊢ Ⅎ𝑘(ϕ‘𝐷)
312	120, 299	eqeltrrd 2830	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷}) → (ϕ‘𝑘) ∈ ℂ)
313		fveq2 6861	. . . . 5 ⊢ (𝑘 = 𝐷 → (ϕ‘𝑘) = (ϕ‘𝐷))
314	7	phicld 16749	. . . . . 6 ⊢ (𝜑 → (ϕ‘𝐷) ∈ ℕ)
315	314	nncnd 12209	. . . . 5 ⊢ (𝜑 → (ϕ‘𝐷) ∈ ℂ)
316	272, 311, 277, 7, 292, 312, 313, 315	fsumsplitsn 15717	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ ({𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} ∪ {𝐷})(ϕ‘𝑘) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
317	310, 316	eqtrd 2765	. . 3 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝑘}) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
318	123, 317	eqtrd 2765	. 2 ⊢ (𝜑 → (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (♯‘{𝑥 ∈ 𝐵 ∣ ((od‘𝐺)‘𝑥) = 𝐷})) = (Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) + (ϕ‘𝐷)))
319	277, 312	fsumcl 15706	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ {𝑎 ∈ (1...(𝐷 − 1)) ∣ 𝑎 ∥ 𝐷} (ϕ‘𝑘) ∈ ℂ)
320	319, 308, 315	addcand 11384	. 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 2926 ∀wral 3045 ∃wrex 3054 {crab 3408 ∪ cun 3915 ⊆ wss 3917 ∅c0 4299 {csn 4592 class class class wbr 5110 ‘cfv 6514 (class class class)co 7390 Fincfn 8921 ℂcc 11073 ℝcr 11074 1c1 11076 + caddc 11078 · cmul 11080 < clt 11215 ≤ cle 11216 − cmin 11412 / cdiv 11842 ℕcn 12193 ℕ₀cn0 12449 ℤcz 12536 ...cfz 13475 ♯chash 14302 Σcsu 15659 ∥ cdvds 16229 gcd cgcd 16471 ϕcphi 16741 Basecbs 17186 0_gc0g 17409 Grpcgrp 18872 ._gcmg 19006 odcod 19461

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 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

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 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-disj 5078 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-oadd 8441 df-omul 8442 df-er 8674 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9400 df-inf 9401 df-oi 9470 df-card 9899 df-acn 9902 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-n0 12450 df-xnn0 12523 df-z 12537 df-uz 12801 df-rp 12959 df-fz 13476 df-fzo 13623 df-fl 13761 df-mod 13839 df-seq 13974 df-exp 14034 df-hash 14303 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-clim 15461 df-sum 15660 df-dvds 16230 df-gcd 16472 df-phi 16743 df-0g 17411 df-mgm 18574 df-sgrp 18653 df-mnd 18669 df-grp 18875 df-minusg 18876 df-sbg 18877 df-mulg 19007 df-od 19465

This theorem is referenced by: unitscyglem3 42192

W3C validator