Metamath Proof Explorer

Theorem musumsum

Description: Evaluate a collapsing sum over the Möbius function. (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses musumsum.1 ⊢ m = 1 → B = C
musumsum.2 ⊢ φ → A ∈ Fin
musumsum.3 ⊢ φ → A ⊆ ℕ
musumsum.4 ⊢ φ → 1 ∈ A
musumsum.5 ⊢ φ ∧ m ∈ A → B ∈ ℂ
Assertion musumsum ⊢ φ → ∑ m ∈ A ∑ k ∈ n ∈ ℕ | n ∥ m μ ⁡ k ⁢ B = C

Proof

Step Hyp Ref Expression
1 musumsum.1 ⊢ m = 1 → B = C
2 musumsum.2 ⊢ φ → A ∈ Fin
3 musumsum.3 ⊢ φ → A ⊆ ℕ
4 musumsum.4 ⊢ φ → 1 ∈ A
5 musumsum.5 ⊢ φ ∧ m ∈ A → B ∈ ℂ
6 3 sselda ⊢ φ ∧ m ∈ A → m ∈ ℕ
7 musum ⊢ m ∈ ℕ → ∑ k ∈ n ∈ ℕ | n ∥ m μ ⁡ k = if m = 1 1 0
8 6 7 syl ⊢ φ ∧ m ∈ A → ∑ k ∈ n ∈ ℕ | n ∥ m μ ⁡ k = if m = 1 1 0
9 8 oveq1d ⊢ φ ∧ m ∈ A → ∑ k ∈ n ∈ ℕ | n ∥ m μ ⁡ k ⁢ B = if m = 1 1 0 ⁢ B
10 fzfid ⊢ φ ∧ m ∈ A → 1 … m ∈ Fin
11 dvdsssfz1 ⊢ m ∈ ℕ → n ∈ ℕ | n ∥ m ⊆ 1 … m
12 6 11 syl ⊢ φ ∧ m ∈ A → n ∈ ℕ | n ∥ m ⊆ 1 … m
13 10 12 ssfid ⊢ φ ∧ m ∈ A → n ∈ ℕ | n ∥ m ∈ Fin
14 elrabi ⊢ k ∈ n ∈ ℕ | n ∥ m → k ∈ ℕ
15 mucl ⊢ k ∈ ℕ → μ ⁡ k ∈ ℤ
16 14 15 syl ⊢ k ∈ n ∈ ℕ | n ∥ m → μ ⁡ k ∈ ℤ
17 16 zcnd ⊢ k ∈ n ∈ ℕ | n ∥ m → μ ⁡ k ∈ ℂ
18 17 adantl ⊢ φ ∧ m ∈ A ∧ k ∈ n ∈ ℕ | n ∥ m → μ ⁡ k ∈ ℂ
19 13 5 18 fsummulc1 ⊢ φ ∧ m ∈ A → ∑ k ∈ n ∈ ℕ | n ∥ m μ ⁡ k ⁢ B = ∑ k ∈ n ∈ ℕ | n ∥ m μ ⁡ k ⁢ B
20 ovif ⊢ if m = 1 1 0 ⁢ B = if m = 1 1 ⁢ B 0 ⋅ B
21 velsn ⊢ m ∈ 1 ↔ m = 1
22 21 bicomi ⊢ m = 1 ↔ m ∈ 1
23 22 a1i ⊢ B ∈ ℂ → m = 1 ↔ m ∈ 1
24 mulid2 ⊢ B ∈ ℂ → 1 ⁢ B = B
25 mul02 ⊢ B ∈ ℂ → 0 ⋅ B = 0
26 23 24 25 ifbieq12d ⊢ B ∈ ℂ → if m = 1 1 ⁢ B 0 ⋅ B = if m ∈ 1 B 0
27 5 26 syl ⊢ φ ∧ m ∈ A → if m = 1 1 ⁢ B 0 ⋅ B = if m ∈ 1 B 0
28 20 27 eqtrid ⊢ φ ∧ m ∈ A → if m = 1 1 0 ⁢ B = if m ∈ 1 B 0
29 9 19 28 3eqtr3d ⊢ φ ∧ m ∈ A → ∑ k ∈ n ∈ ℕ | n ∥ m μ ⁡ k ⁢ B = if m ∈ 1 B 0
30 29 sumeq2dv ⊢ φ → ∑ m ∈ A ∑ k ∈ n ∈ ℕ | n ∥ m μ ⁡ k ⁢ B = ∑ m ∈ A if m ∈ 1 B 0
31 4 snssd ⊢ φ → 1 ⊆ A
32 31 sselda ⊢ φ ∧ m ∈ 1 → m ∈ A
33 32 5 syldan ⊢ φ ∧ m ∈ 1 → B ∈ ℂ
34 33 ralrimiva ⊢ φ → ∀ m ∈ 1 B ∈ ℂ
35 2 olcd ⊢ φ → A ⊆ ℤ ≥ 1 ∨ A ∈ Fin
36 sumss2 ⊢ 1 ⊆ A ∧ ∀ m ∈ 1 B ∈ ℂ ∧ A ⊆ ℤ ≥ 1 ∨ A ∈ Fin → ∑ m ∈ 1 B = ∑ m ∈ A if m ∈ 1 B 0
37 31 34 35 36 syl21anc ⊢ φ → ∑ m ∈ 1 B = ∑ m ∈ A if m ∈ 1 B 0
38 1 eleq1d ⊢ m = 1 → B ∈ ℂ ↔ C ∈ ℂ
39 5 ralrimiva ⊢ φ → ∀ m ∈ A B ∈ ℂ
40 38 39 4 rspcdva ⊢ φ → C ∈ ℂ
41 1 sumsn ⊢ 1 ∈ A ∧ C ∈ ℂ → ∑ m ∈ 1 B = C
42 4 40 41 syl2anc ⊢ φ → ∑ m ∈ 1 B = C
43 30 37 42 3eqtr2d ⊢ φ → ∑ m ∈ A ∑ k ∈ n ∈ ℕ | n ∥ m μ ⁡ k ⁢ B = C