This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑚 = 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 mullid ⊢ ( 𝐵 ∈ ℂ → ( 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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐴 ) → ( 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 ⊢ ( 𝜑 → Σ 𝑚 ∈ 𝐴 Σ 𝑘 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑚 } ( ( μ ‘ 𝑘 ) · 𝐵 ) = 𝐶 )