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=ifm=110
8 6 7 syl ⊢φ∧m∈A→∑k∈n∈ℕ|n∥mμ⁡k=ifm=110
9 8 oveq1d ⊢φ∧m∈A→∑k∈n∈ℕ|n∥mμ⁡k⁢B=ifm=110⁢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 ⊢ifm=110⁢B=ifm=11⁢B0⋅B
21 velsn ⊢m∈1↔m=1
22 21 bicomi ⊢m=1↔m∈1
23 22 a1i ⊢B∈ℂ→m=1↔m∈1
24 mullid ⊢B∈ℂ→1⁢B=B
25 mul02 ⊢B∈ℂ→0⋅B=0
26 23 24 25 ifbieq12d ⊢B∈ℂ→ifm=11⁢B0⋅B=ifm∈1B0
27 5 26 syl ⊢φ∧m∈A→ifm=11⁢B0⋅B=ifm∈1B0
28 20 27 eqtrid ⊢φ∧m∈A→ifm=110⁢B=ifm∈1B0
29 9 19 28 3eqtr3d ⊢φ∧m∈A→∑k∈n∈ℕ|n∥mμ⁡k⁢B=ifm∈1B0
30 29 sumeq2dv ⊢φ→∑m∈A∑k∈n∈ℕ|n∥mμ⁡k⁢B=∑m∈Aifm∈1B0
31 4 snssd ⊢φ→1⊆A
32 31 sselda ⊢φ∧m∈1→m∈A
33 32 5 syldan ⊢φ∧m∈1→B∈ℂ
34 33 ralrimiva ⊢φ→∀m∈1B∈ℂ
35 2 olcd ⊢φ→A⊆ℤ≥1∨A∈Fin
36 sumss2 ⊢1⊆A∧∀m∈1B∈ℂ∧A⊆ℤ≥1∨A∈Fin→∑m∈1B=∑m∈Aifm∈1B0
37 31 34 35 36 syl21anc ⊢φ→∑m∈1B=∑m∈Aifm∈1B0
38 1 eleq1d ⊢m=1→B∈ℂ↔C∈ℂ
39 5 ralrimiva ⊢φ→∀m∈AB∈ℂ
40 38 39 4 rspcdva ⊢φ→C∈ℂ
41 1 sumsn ⊢1∈A∧C∈ℂ→∑m∈1B=C
42 4 40 41 syl2anc ⊢φ→∑m∈1B=C
43 30 37 42 3eqtr2d ⊢φ→∑m∈A∑k∈n∈ℕ|n∥mμ⁡k⁢B=C