muinv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > muinv		Structured version Visualization version GIF version

Theorem muinv 26686

Description: The Möbius inversion formula. If 𝐺(𝑛) = Σ𝑘 ∥ 𝑛𝐹(𝑘) for every 𝑛 ∈ ℕ, then 𝐹(𝑛) = Σ𝑘 ∥ 𝑛 μ(𝑘)𝐺(𝑛 / 𝑘) = Σ𝑘 ∥ 𝑛μ(𝑛 / 𝑘)𝐺(𝑘), i.e. the Möbius function is the Dirichlet convolution inverse of the constant function 1. Theorem 2.9 in [ApostolNT] p. 32. (Contributed by Mario Carneiro, 2-Jul-2015.)

**Hypotheses**
Ref	Expression
muinv.1	⊢ (𝜑 → 𝐹:ℕ⟶ℂ)
muinv.2	⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (𝐹‘𝑘)))

**Assertion**
Ref	Expression
muinv	⊢ (𝜑 → 𝐹 = (𝑚 ∈ ℕ ↦ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((μ‘𝑗) · (𝐺‘(𝑚 / 𝑗)))))

Distinct variable groups: 𝑘,𝑚,𝑗,𝑛,𝐹 𝑥,𝑗,𝑘,𝑚,𝑛 𝜑,𝑗,𝑘,𝑚 Allowed substitution hints: 𝜑(𝑥,𝑛) 𝐹(𝑥) 𝐺(𝑥,𝑗,𝑘,𝑚,𝑛)

**Proof of Theorem muinv**
Step	Hyp	Ref	Expression
1		muinv.1	. . 3 ⊢ (𝜑 → 𝐹:ℕ⟶ℂ)
2	1	feqmptd 6957	. 2 ⊢ (𝜑 → 𝐹 = (𝑚 ∈ ℕ ↦ (𝐹‘𝑚)))
3		muinv.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (𝐹‘𝑘)))
4	3	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝐺 = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (𝐹‘𝑘)))
5	4	fveq1d 6890	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝐺‘(𝑚 / 𝑗)) = ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (𝐹‘𝑘))‘(𝑚 / 𝑗)))
6		breq1 5150	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑗 → (𝑥 ∥ 𝑚 ↔ 𝑗 ∥ 𝑚))
7	6	elrab 3682	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ↔ (𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑚))
8	7	simprbi 497	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} → 𝑗 ∥ 𝑚)
9	8	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝑗 ∥ 𝑚)
10		elrabi 3676	. . . . . . . . . . . . . 14 ⊢ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} → 𝑗 ∈ ℕ)
11	10	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝑗 ∈ ℕ)
12	11	nnzd 12581	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝑗 ∈ ℤ)
13	11	nnne0d 12258	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝑗 ≠ 0)
14		nnz 12575	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
15	14	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝑚 ∈ ℤ)
16		dvdsval2 16196	. . . . . . . . . . . 12 ⊢ ((𝑗 ∈ ℤ ∧ 𝑗 ≠ 0 ∧ 𝑚 ∈ ℤ) → (𝑗 ∥ 𝑚 ↔ (𝑚 / 𝑗) ∈ ℤ))
17	12, 13, 15, 16	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝑗 ∥ 𝑚 ↔ (𝑚 / 𝑗) ∈ ℤ))
18	9, 17	mpbid 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝑚 / 𝑗) ∈ ℤ)
19		nnre 12215	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
20		nngt0 12239	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℕ → 0 < 𝑚)
21	19, 20	jca 512	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
22	21	ad2antlr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
23		nnre 12215	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ)
24		nngt0 12239	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → 0 < 𝑗)
25	23, 24	jca 512	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ ℕ → (𝑗 ∈ ℝ ∧ 0 < 𝑗))
26	11, 25	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝑗 ∈ ℝ ∧ 0 < 𝑗))
27		divgt0 12078	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ℝ ∧ 0 < 𝑚) ∧ (𝑗 ∈ ℝ ∧ 0 < 𝑗)) → 0 < (𝑚 / 𝑗))
28	22, 26, 27	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 0 < (𝑚 / 𝑗))
29		elnnz 12564	. . . . . . . . . 10 ⊢ ((𝑚 / 𝑗) ∈ ℕ ↔ ((𝑚 / 𝑗) ∈ ℤ ∧ 0 < (𝑚 / 𝑗)))
30	18, 28, 29	sylanbrc 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝑚 / 𝑗) ∈ ℕ)
31		breq2 5151	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑚 / 𝑗) → (𝑥 ∥ 𝑛 ↔ 𝑥 ∥ (𝑚 / 𝑗)))
32	31	rabbidv 3440	. . . . . . . . . . 11 ⊢ (𝑛 = (𝑚 / 𝑗) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)})
33	32	sumeq1d 15643	. . . . . . . . . 10 ⊢ (𝑛 = (𝑚 / 𝑗) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (𝐹‘𝑘) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} (𝐹‘𝑘))
34		eqid 2732	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (𝐹‘𝑘)) = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (𝐹‘𝑘))
35		sumex 15630	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} (𝐹‘𝑘) ∈ V
36	33, 34, 35	fvmpt 6995	. . . . . . . . 9 ⊢ ((𝑚 / 𝑗) ∈ ℕ → ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (𝐹‘𝑘))‘(𝑚 / 𝑗)) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} (𝐹‘𝑘))
37	30, 36	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → ((𝑛 ∈ ℕ ↦ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛} (𝐹‘𝑘))‘(𝑚 / 𝑗)) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} (𝐹‘𝑘))
38	5, 37	eqtrd 2772	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝐺‘(𝑚 / 𝑗)) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} (𝐹‘𝑘))
39	38	oveq2d 7421	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → ((μ‘𝑗) · (𝐺‘(𝑚 / 𝑗))) = ((μ‘𝑗) · Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} (𝐹‘𝑘)))
40		fzfid 13934	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (1...(𝑚 / 𝑗)) ∈ Fin)
41		dvdsssfz1 16257	. . . . . . . . 9 ⊢ ((𝑚 / 𝑗) ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} ⊆ (1...(𝑚 / 𝑗)))
42	30, 41	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} ⊆ (1...(𝑚 / 𝑗)))
43	40, 42	ssfid 9263	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} ∈ Fin)
44		mucl 26634	. . . . . . . . 9 ⊢ (𝑗 ∈ ℕ → (μ‘𝑗) ∈ ℤ)
45	11, 44	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (μ‘𝑗) ∈ ℤ)
46	45	zcnd 12663	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (μ‘𝑗) ∈ ℂ)
47	1	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝐹:ℕ⟶ℂ)
48		elrabi 3676	. . . . . . . 8 ⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} → 𝑘 ∈ ℕ)
49		ffvelcdm 7080	. . . . . . . 8 ⊢ ((𝐹:ℕ⟶ℂ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
50	47, 48, 49	syl2an 596	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)}) → (𝐹‘𝑘) ∈ ℂ)
51	43, 46, 50	fsummulc2 15726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → ((μ‘𝑗) · Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} (𝐹‘𝑘)) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} ((μ‘𝑗) · (𝐹‘𝑘)))
52	39, 51	eqtrd 2772	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → ((μ‘𝑗) · (𝐺‘(𝑚 / 𝑗))) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} ((μ‘𝑗) · (𝐹‘𝑘)))
53	52	sumeq2dv 15645	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((μ‘𝑗) · (𝐺‘(𝑚 / 𝑗))) = Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} ((μ‘𝑗) · (𝐹‘𝑘)))
54		simpr 485	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
55	46	adantrr 715	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)})) → (μ‘𝑗) ∈ ℂ)
56	50	anasss 467	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)})) → (𝐹‘𝑘) ∈ ℂ)
57	55, 56	mulcld 11230	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)})) → ((μ‘𝑗) · (𝐹‘𝑘)) ∈ ℂ)
58	54, 57	fsumdvdsdiag 26677	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑗)} ((μ‘𝑗) · (𝐹‘𝑘)) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} ((μ‘𝑗) · (𝐹‘𝑘)))
59		ssrab2 4076	. . . . . . . . . 10 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ⊆ ℕ
60		dvdsdivcl 16255	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝑚 / 𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚})
61	60	adantll 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝑚 / 𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚})
62	59, 61	sselid 3979	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝑚 / 𝑘) ∈ ℕ)
63		musum 26684	. . . . . . . . 9 ⊢ ((𝑚 / 𝑘) ∈ ℕ → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} (μ‘𝑗) = if((𝑚 / 𝑘) = 1, 1, 0))
64	62, 63	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} (μ‘𝑗) = if((𝑚 / 𝑘) = 1, 1, 0))
65	64	oveq1d 7420	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} (μ‘𝑗) · (𝐹‘𝑘)) = (if((𝑚 / 𝑘) = 1, 1, 0) · (𝐹‘𝑘)))
66		fzfid 13934	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (1...(𝑚 / 𝑘)) ∈ Fin)
67		dvdsssfz1 16257	. . . . . . . . . 10 ⊢ ((𝑚 / 𝑘) ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} ⊆ (1...(𝑚 / 𝑘)))
68	62, 67	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} ⊆ (1...(𝑚 / 𝑘)))
69	66, 68	ssfid 9263	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} ∈ Fin)
70	1	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝐹:ℕ⟶ℂ)
71		elrabi 3676	. . . . . . . . 9 ⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} → 𝑘 ∈ ℕ)
72	70, 71, 49	syl2an 596	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝐹‘𝑘) ∈ ℂ)
73		ssrab2 4076	. . . . . . . . . . 11 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} ⊆ ℕ
74		simpr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)}) → 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)})
75	73, 74	sselid 3979	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)}) → 𝑗 ∈ ℕ)
76	75, 44	syl 17	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)}) → (μ‘𝑗) ∈ ℤ)
77	76	zcnd 12663	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) ∧ 𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)}) → (μ‘𝑗) ∈ ℂ)
78	69, 72, 77	fsummulc1 15727	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} (μ‘𝑗) · (𝐹‘𝑘)) = Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} ((μ‘𝑗) · (𝐹‘𝑘)))
79		ovif 7502	. . . . . . . 8 ⊢ (if((𝑚 / 𝑘) = 1, 1, 0) · (𝐹‘𝑘)) = if((𝑚 / 𝑘) = 1, (1 · (𝐹‘𝑘)), (0 · (𝐹‘𝑘)))
80		nncn 12216	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
81	80	ad2antlr 725	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝑚 ∈ ℂ)
82	71	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝑘 ∈ ℕ)
83	82	nncnd 12224	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝑘 ∈ ℂ)
84		1cnd 11205	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 1 ∈ ℂ)
85	82	nnne0d 12258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → 𝑘 ≠ 0)
86	81, 83, 84, 85	divmuld 12008	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → ((𝑚 / 𝑘) = 1 ↔ (𝑘 · 1) = 𝑚))
87	83	mulridd 11227	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (𝑘 · 1) = 𝑘)
88	87	eqeq1d 2734	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → ((𝑘 · 1) = 𝑚 ↔ 𝑘 = 𝑚))
89	86, 88	bitrd 278	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → ((𝑚 / 𝑘) = 1 ↔ 𝑘 = 𝑚))
90	72	mullidd 11228	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (1 · (𝐹‘𝑘)) = (𝐹‘𝑘))
91	72	mul02d 11408	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (0 · (𝐹‘𝑘)) = 0)
92	89, 90, 91	ifbieq12d 4555	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → if((𝑚 / 𝑘) = 1, (1 · (𝐹‘𝑘)), (0 · (𝐹‘𝑘))) = if(𝑘 = 𝑚, (𝐹‘𝑘), 0))
93	79, 92	eqtrid 2784	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → (if((𝑚 / 𝑘) = 1, 1, 0) · (𝐹‘𝑘)) = if(𝑘 = 𝑚, (𝐹‘𝑘), 0))
94	65, 78, 93	3eqtr3d 2780	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}) → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} ((μ‘𝑗) · (𝐹‘𝑘)) = if(𝑘 = 𝑚, (𝐹‘𝑘), 0))
95	94	sumeq2dv 15645	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} ((μ‘𝑗) · (𝐹‘𝑘)) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}if(𝑘 = 𝑚, (𝐹‘𝑘), 0))
96		breq1 5150	. . . . . . . 8 ⊢ (𝑥 = 𝑚 → (𝑥 ∥ 𝑚 ↔ 𝑚 ∥ 𝑚))
97	54	nnzd 12581	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℤ)
98		iddvds 16209	. . . . . . . . 9 ⊢ (𝑚 ∈ ℤ → 𝑚 ∥ 𝑚)
99	97, 98	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∥ 𝑚)
100	96, 54, 99	elrabd 3684	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚})
101	100	snssd 4811	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → {𝑚} ⊆ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚})
102	101	sselda 3981	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑚}) → 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚})
103	102, 72	syldan 591	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑚}) → (𝐹‘𝑘) ∈ ℂ)
104		0cn 11202	. . . . . . 7 ⊢ 0 ∈ ℂ
105		ifcl 4572	. . . . . . 7 ⊢ (((𝐹‘𝑘) ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 = 𝑚, (𝐹‘𝑘), 0) ∈ ℂ)
106	103, 104, 105	sylancl 586	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ {𝑚}) → if(𝑘 = 𝑚, (𝐹‘𝑘), 0) ∈ ℂ)
107		eldifsni 4792	. . . . . . . . 9 ⊢ (𝑘 ∈ ({𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ∖ {𝑚}) → 𝑘 ≠ 𝑚)
108	107	adantl 482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ({𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ∖ {𝑚})) → 𝑘 ≠ 𝑚)
109	108	neneqd 2945	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ({𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ∖ {𝑚})) → ¬ 𝑘 = 𝑚)
110	109	iffalsed 4538	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ({𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ∖ {𝑚})) → if(𝑘 = 𝑚, (𝐹‘𝑘), 0) = 0)
111		fzfid 13934	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (1...𝑚) ∈ Fin)
112		dvdsssfz1 16257	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ⊆ (1...𝑚))
113	112	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ⊆ (1...𝑚))
114	111, 113	ssfid 9263	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ∈ Fin)
115	101, 106, 110, 114	fsumss 15667	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ {𝑚}if(𝑘 = 𝑚, (𝐹‘𝑘), 0) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}if(𝑘 = 𝑚, (𝐹‘𝑘), 0))
116	1	ffvelcdmda 7083	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ ℂ)
117		iftrue 4533	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → if(𝑘 = 𝑚, (𝐹‘𝑘), 0) = (𝐹‘𝑘))
118		fveq2 6888	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚))
119	117, 118	eqtrd 2772	. . . . . . 7 ⊢ (𝑘 = 𝑚 → if(𝑘 = 𝑚, (𝐹‘𝑘), 0) = (𝐹‘𝑚))
120	119	sumsn 15688	. . . . . 6 ⊢ ((𝑚 ∈ ℕ ∧ (𝐹‘𝑚) ∈ ℂ) → Σ𝑘 ∈ {𝑚}if(𝑘 = 𝑚, (𝐹‘𝑘), 0) = (𝐹‘𝑚))
121	54, 116, 120	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ {𝑚}if(𝑘 = 𝑚, (𝐹‘𝑘), 0) = (𝐹‘𝑚))
122	95, 115, 121	3eqtr2d 2778	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚}Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑚 / 𝑘)} ((μ‘𝑗) · (𝐹‘𝑘)) = (𝐹‘𝑚))
123	53, 58, 122	3eqtrd 2776	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((μ‘𝑗) · (𝐺‘(𝑚 / 𝑗))) = (𝐹‘𝑚))
124	123	mpteq2dva 5247	. 2 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((μ‘𝑗) · (𝐺‘(𝑚 / 𝑗)))) = (𝑚 ∈ ℕ ↦ (𝐹‘𝑚)))
125	2, 124	eqtr4d 2775	1 ⊢ (𝜑 → 𝐹 = (𝑚 ∈ ℕ ↦ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚} ((μ‘𝑗) · (𝐺‘(𝑚 / 𝑗)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 {crab 3432 ∖ cdif 3944 ⊆ wss 3947 ifcif 4527 {csn 4627 class class class wbr 5147 ↦ cmpt 5230 ⟶wf 6536 ‘cfv 6540 (class class class)co 7405 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 · cmul 11111 < clt 11244 / cdiv 11867 ℕcn 12208 ℤcz 12554 ...cfz 13480 Σcsu 15628 ∥ cdvds 16193 μcmu 26588

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-inf2 9632 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-disj 5113 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-oadd 8466 df-er 8699 df-map 8818 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-sup 9433 df-inf 9434 df-oi 9501 df-dju 9892 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-div 11868 df-nn 12209 df-2 12271 df-3 12272 df-n0 12469 df-xnn0 12541 df-z 12555 df-uz 12819 df-q 12929 df-rp 12971 df-fz 13481 df-fzo 13624 df-fl 13753 df-mod 13831 df-seq 13963 df-exp 14024 df-fac 14230 df-bc 14259 df-hash 14287 df-cj 15042 df-re 15043 df-im 15044 df-sqrt 15178 df-abs 15179 df-clim 15428 df-sum 15629 df-dvds 16194 df-gcd 16432 df-prm 16605 df-pc 16766 df-mu 26594

This theorem is referenced by: dchrvmasumlem1 26987 logsqvma2 27035

W3C validator