Theorem musumsum

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

	Ref	Expression
Hypotheses	musumsum.1	⊢ ( 𝑚 = 1 → 𝐵 = 𝐶 )
	musumsum.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	musumsum.3	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
	musumsum.4	⊢ ( 𝜑 → 1 ∈ 𝐴 )
	musumsum.5	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion	musumsum	⊢ ( 𝜑 → Σ 𝑚 ∈ 𝐴 Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ( ( μ ‘ 𝑘 ) · 𝐵 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		musumsum.1	⊢ ( 𝑚 = 1 → 𝐵 = 𝐶 )
2		musumsum.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		musumsum.3	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
4		musumsum.4	⊢ ( 𝜑 → 1 ∈ 𝐴 )
5		musumsum.5	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
6	3	sselda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → 𝑚 ∈ ℕ )
7		musum	⊢ ( 𝑚 ∈ ℕ → Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ( μ ‘ 𝑘 ) = if ( 𝑚 = 1 , 1 , 0 ) )
8	6 7	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ( μ ‘ 𝑘 ) = if ( 𝑚 = 1 , 1 , 0 ) )
9	8	oveq1d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ( Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ( μ ‘ 𝑘 ) · 𝐵 ) = ( if ( 𝑚 = 1 , 1 , 0 ) · 𝐵 ) )
10		fzfid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ( 1 ... 𝑚 ) ∈ Fin )
11		dvdsssfz1	⊢ ( 𝑚 ∈ ℕ → { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ⊆ ( 1 ... 𝑚 ) )
12	6 11	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ⊆ ( 1 ... 𝑚 ) )
13	10 12	ssfid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ∈ Fin )
14		elrabi	⊢ ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } → 𝑘 ∈ ℕ )
15		mucl	⊢ ( 𝑘 ∈ ℕ → ( μ ‘ 𝑘 ) ∈ ℤ )
16	14 15	syl	⊢ ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } → ( μ ‘ 𝑘 ) ∈ ℤ )
17	16	zcnd	⊢ ( 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } → ( μ ‘ 𝑘 ) ∈ ℂ )
18	17	adantl	⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) ∧ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ) → ( μ ‘ 𝑘 ) ∈ ℂ )
19	13 5 18	fsummulc1	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ( Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ( μ ‘ 𝑘 ) · 𝐵 ) = Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ( ( μ ‘ 𝑘 ) · 𝐵 ) )
20		ovif	⊢ ( if ( 𝑚 = 1 , 1 , 0 ) · 𝐵 ) = if ( 𝑚 = 1 , ( 1 · 𝐵 ) , ( 0 · 𝐵 ) )
21		velsn	⊢ ( 𝑚 ∈ { 1 } ↔ 𝑚 = 1 )
22	21	bicomi	⊢ ( 𝑚 = 1 ↔ 𝑚 ∈ { 1 } )
23	22	a1i	⊢ ( 𝐵 ∈ ℂ → ( 𝑚 = 1 ↔ 𝑚 ∈ { 1 } ) )
24		mulid2	⊢ ( 𝐵 ∈ ℂ → ( 1 · 𝐵 ) = 𝐵 )
25		mul02	⊢ ( 𝐵 ∈ ℂ → ( 0 · 𝐵 ) = 0 )
26	23 24 25	ifbieq12d	⊢ ( 𝐵 ∈ ℂ → if ( 𝑚 = 1 , ( 1 · 𝐵 ) , ( 0 · 𝐵 ) ) = if ( 𝑚 ∈ { 1 } , 𝐵 , 0 ) )
27	5 26	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → if ( 𝑚 = 1 , ( 1 · 𝐵 ) , ( 0 · 𝐵 ) ) = if ( 𝑚 ∈ { 1 } , 𝐵 , 0 ) )
28	20 27	syl5eq	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ( if ( 𝑚 = 1 , 1 , 0 ) · 𝐵 ) = if ( 𝑚 ∈ { 1 } , 𝐵 , 0 ) )
29	9 19 28	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ( ( μ ‘ 𝑘 ) · 𝐵 ) = if ( 𝑚 ∈ { 1 } , 𝐵 , 0 ) )
30	29	sumeq2dv	⊢ ( 𝜑 → Σ 𝑚 ∈ 𝐴 Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ( ( μ ‘ 𝑘 ) · 𝐵 ) = Σ 𝑚 ∈ 𝐴 if ( 𝑚 ∈ { 1 } , 𝐵 , 0 ) )
31	4	snssd	⊢ ( 𝜑 → { 1 } ⊆ 𝐴 )
32	31	sselda	⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 1 } ) → 𝑚 ∈ 𝐴 )
33	32 5	syldan	⊢ ( ( 𝜑 ∧ 𝑚 ∈ { 1 } ) → 𝐵 ∈ ℂ )
34	33	ralrimiva	⊢ ( 𝜑 → ∀ 𝑚 ∈ { 1 } 𝐵 ∈ ℂ )
35	2	olcd	⊢ ( 𝜑 → ( 𝐴 ⊆ ( ℤ≥ ‘ 1 ) ∨ 𝐴 ∈ Fin ) )
36		sumss2	⊢ ( ( ( { 1 } ⊆ 𝐴 ∧ ∀ 𝑚 ∈ { 1 } 𝐵 ∈ ℂ ) ∧ ( 𝐴 ⊆ ( ℤ≥ ‘ 1 ) ∨ 𝐴 ∈ Fin ) ) → Σ 𝑚 ∈ { 1 } 𝐵 = Σ 𝑚 ∈ 𝐴 if ( 𝑚 ∈ { 1 } , 𝐵 , 0 ) )
37	31 34 35 36	syl21anc	⊢ ( 𝜑 → Σ 𝑚 ∈ { 1 } 𝐵 = Σ 𝑚 ∈ 𝐴 if ( 𝑚 ∈ { 1 } , 𝐵 , 0 ) )
38	1	eleq1d	⊢ ( 𝑚 = 1 → ( 𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
39	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝐴 𝐵 ∈ ℂ )
40	38 39 4	rspcdva	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
41	1	sumsn	⊢ ( ( 1 ∈ 𝐴 ∧ 𝐶 ∈ ℂ ) → Σ 𝑚 ∈ { 1 } 𝐵 = 𝐶 )
42	4 40 41	syl2anc	⊢ ( 𝜑 → Σ 𝑚 ∈ { 1 } 𝐵 = 𝐶 )
43	30 37 42	3eqtr2d	⊢ ( 𝜑 → Σ 𝑚 ∈ 𝐴 Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ( ( μ ‘ 𝑘 ) · 𝐵 ) = 𝐶 )