Metamath Proof Explorer

Theorem muinv

Description: The Möbius inversion formula. If G ( n ) = sum_ k || n F ( k ) for every n e. NN , then F ( n ) = sum_ k || n mmu ( k ) G ( n / k ) = sum_ k || n mmu ( n / k ) G ( k ) , 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)

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

Proof

Step Hyp Ref Expression
1 muinv.1 ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℂ )
2 muinv.2 ⊢ ( 𝜑 → 𝐺 = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( 𝐹 ‘ 𝑘 ) ) )
3 1 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑚 ∈ ℕ ↦ ( 𝐹 ‘ 𝑚 ) ) )
4 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝐺 = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( 𝐹 ‘ 𝑘 ) ) )
5 4 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝐺 ‘ ( 𝑚 / 𝑗 ) ) = ( ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( 𝐹 ‘ 𝑘 ) ) ‘ ( 𝑚 / 𝑗 ) ) )
6 breq1 ⊢ ( 𝑥 = 𝑗 → ( 𝑥 ∥ 𝑚 ↔ 𝑗 ∥ 𝑚 ) )
7 6 elrab ⊢ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ↔ ( 𝑗 ∈ ℕ ∧ 𝑗 ∥ 𝑚 ) )
8 7 simprbi ⊢ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } → 𝑗 ∥ 𝑚 )
9 8 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝑗 ∥ 𝑚 )
10 elrabi ⊢ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } → 𝑗 ∈ ℕ )
11 10 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝑗 ∈ ℕ )
12 11 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝑗 ∈ ℤ )
13 11 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝑗 ≠ 0 )
14 nnz ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
15 14 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝑚 ∈ ℤ )
16 dvdsval2 ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝑗 ≠ 0 ∧ 𝑚 ∈ ℤ ) → ( 𝑗 ∥ 𝑚 ↔ ( 𝑚 / 𝑗 ) ∈ ℤ ) )
17 12 13 15 16 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝑗 ∥ 𝑚 ↔ ( 𝑚 / 𝑗 ) ∈ ℤ ) )
18 9 17 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝑚 / 𝑗 ) ∈ ℤ )
19 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
20 nngt0 ⊢ ( 𝑚 ∈ ℕ → 0 < 𝑚 )
21 19 20 jca ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 ∈ ℝ ∧ 0 < 𝑚 ) )
22 21 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝑚 ∈ ℝ ∧ 0 < 𝑚 ) )
23 nnre ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ )
24 nngt0 ⊢ ( 𝑗 ∈ ℕ → 0 < 𝑗 )
25 23 24 jca ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 ∈ ℝ ∧ 0 < 𝑗 ) )
26 11 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝑗 ∈ ℝ ∧ 0 < 𝑗 ) )
27 divgt0 ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 0 < 𝑚 ) ∧ ( 𝑗 ∈ ℝ ∧ 0 < 𝑗 ) ) → 0 < ( 𝑚 / 𝑗 ) )
28 22 26 27 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 0 < ( 𝑚 / 𝑗 ) )
29 elnnz ⊢ ( ( 𝑚 / 𝑗 ) ∈ ℕ ↔ ( ( 𝑚 / 𝑗 ) ∈ ℤ ∧ 0 < ( 𝑚 / 𝑗 ) ) )
30 18 28 29 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝑚 / 𝑗 ) ∈ ℕ )
31 breq2 ⊢ ( 𝑛 = ( 𝑚 / 𝑗 ) → ( 𝑥 ∥ 𝑛 ↔ 𝑥 ∥ ( 𝑚 / 𝑗 ) ) )
32 31 rabbidv ⊢ ( 𝑛 = ( 𝑚 / 𝑗 ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } )
33 32 sumeq1d ⊢ ( 𝑛 = ( 𝑚 / 𝑗 ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( 𝐹 ‘ 𝑘 ) )
34 eqid ⊢ ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( 𝐹 ‘ 𝑘 ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( 𝐹 ‘ 𝑘 ) )
35 sumex ⊢ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( 𝐹 ‘ 𝑘 ) ∈ V
36 33 34 35 fvmpt ⊢ ( ( 𝑚 / 𝑗 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( 𝐹 ‘ 𝑘 ) ) ‘ ( 𝑚 / 𝑗 ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( 𝐹 ‘ 𝑘 ) )
37 30 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( ( 𝑛 ∈ ℕ ↦ Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( 𝐹 ‘ 𝑘 ) ) ‘ ( 𝑚 / 𝑗 ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( 𝐹 ‘ 𝑘 ) )
38 5 37 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝐺 ‘ ( 𝑚 / 𝑗 ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( 𝐹 ‘ 𝑘 ) )
39 38 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( ( μ ‘ 𝑗 ) · ( 𝐺 ‘ ( 𝑚 / 𝑗 ) ) ) = ( ( μ ‘ 𝑗 ) · Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( 𝐹 ‘ 𝑘 ) ) )
40 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 1 ... ( 𝑚 / 𝑗 ) ) ∈ Fin )
41 dvdsssfz1 ⊢ ( ( 𝑚 / 𝑗 ) ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ⊆ ( 1 ... ( 𝑚 / 𝑗 ) ) )
42 30 41 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ⊆ ( 1 ... ( 𝑚 / 𝑗 ) ) )
43 40 42 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ∈ Fin )
44 mucl ⊢ ( 𝑗 ∈ ℕ → ( μ ‘ 𝑗 ) ∈ ℤ )
45 11 44 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( μ ‘ 𝑗 ) ∈ ℤ )
46 45 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( μ ‘ 𝑗 ) ∈ ℂ )
47 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝐹 : ℕ ⟶ ℂ )
48 elrabi ⊢ ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } → 𝑘 ∈ ℕ )
49 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ ℂ ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
50 47 48 49 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
51 43 46 50 fsummulc2 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( ( μ ‘ 𝑗 ) · Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( 𝐹 ‘ 𝑘 ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) )
52 39 51 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( ( μ ‘ 𝑗 ) · ( 𝐺 ‘ ( 𝑚 / 𝑗 ) ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) )
53 52 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( μ ‘ 𝑗 ) · ( 𝐺 ‘ ( 𝑚 / 𝑗 ) ) ) = Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) )
54 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
55 46 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ) ) → ( μ ‘ 𝑗 ) ∈ ℂ )
56 50 anasss ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
57 55 56 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ) ) → ( ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) ∈ ℂ )
58 54 57 fsumdvdsdiag ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑗 ) } ( ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ( ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) )
59 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ⊆ ℕ
60 dvdsdivcl ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝑚 / 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } )
61 60 adantll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝑚 / 𝑘 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } )
62 59 61 sselid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝑚 / 𝑘 ) ∈ ℕ )
63 musum ⊢ ( ( 𝑚 / 𝑘 ) ∈ ℕ → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ( μ ‘ 𝑗 ) = if ( ( 𝑚 / 𝑘 ) = 1 , 1 , 0 ) )
64 62 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ( μ ‘ 𝑗 ) = if ( ( 𝑚 / 𝑘 ) = 1 , 1 , 0 ) )
65 64 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) = ( if ( ( 𝑚 / 𝑘 ) = 1 , 1 , 0 ) · ( 𝐹 ‘ 𝑘 ) ) )
66 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 1 ... ( 𝑚 / 𝑘 ) ) ∈ Fin )
67 dvdsssfz1 ⊢ ( ( 𝑚 / 𝑘 ) ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ⊆ ( 1 ... ( 𝑚 / 𝑘 ) ) )
68 62 67 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ⊆ ( 1 ... ( 𝑚 / 𝑘 ) ) )
69 66 68 ssfid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ∈ Fin )
70 1 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝐹 : ℕ ⟶ ℂ )
71 elrabi ⊢ ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } → 𝑘 ∈ ℕ )
72 70 71 49 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
73 ssrab2 ⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ⊆ ℕ
74 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ) → 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } )
75 73 74 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ) → 𝑗 ∈ ℕ )
76 75 44 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ) → ( μ ‘ 𝑗 ) ∈ ℤ )
77 76 zcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ) → ( μ ‘ 𝑗 ) ∈ ℂ )
78 69 72 77 fsummulc1 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) = Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ( ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) )
79 ovif ⊢ ( if ( ( 𝑚 / 𝑘 ) = 1 , 1 , 0 ) · ( 𝐹 ‘ 𝑘 ) ) = if ( ( 𝑚 / 𝑘 ) = 1 , ( 1 · ( 𝐹 ‘ 𝑘 ) ) , ( 0 · ( 𝐹 ‘ 𝑘 ) ) )
80 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
81 80 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝑚 ∈ ℂ )
82 71 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝑘 ∈ ℕ )
83 82 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝑘 ∈ ℂ )
84 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 1 ∈ ℂ )
85 82 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → 𝑘 ≠ 0 )
86 81 83 84 85 divmuld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( ( 𝑚 / 𝑘 ) = 1 ↔ ( 𝑘 · 1 ) = 𝑚 ) )
87 83 mulridd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 𝑘 · 1 ) = 𝑘 )
88 87 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( ( 𝑘 · 1 ) = 𝑚 ↔ 𝑘 = 𝑚 ) )
89 86 88 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( ( 𝑚 / 𝑘 ) = 1 ↔ 𝑘 = 𝑚 ) )
90 72 mullidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 1 · ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑘 ) )
91 72 mul02d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( 0 · ( 𝐹 ‘ 𝑘 ) ) = 0 )
92 89 90 91 ifbieq12d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → if ( ( 𝑚 / 𝑘 ) = 1 , ( 1 · ( 𝐹 ‘ 𝑘 ) ) , ( 0 · ( 𝐹 ‘ 𝑘 ) ) ) = if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) )
93 79 92 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → ( if ( ( 𝑚 / 𝑘 ) = 1 , 1 , 0 ) · ( 𝐹 ‘ 𝑘 ) ) = if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) )
94 65 78 93 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ) → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ( ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) = if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) )
95 94 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ( ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) )
96 breq1 ⊢ ( 𝑥 = 𝑚 → ( 𝑥 ∥ 𝑚 ↔ 𝑚 ∥ 𝑚 ) )
97 54 nnzd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℤ )
98 iddvds ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∥ 𝑚 )
99 97 98 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∥ 𝑚 )
100 96 54 99 elrabd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } )
101 100 snssd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → { 𝑚 } ⊆ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } )
102 101 sselda ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑚 } ) → 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } )
103 102 72 syldan ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑚 } ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
104 0cn ⊢ 0 ∈ ℂ
105 ifcl ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) ∈ ℂ )
106 103 104 105 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ { 𝑚 } ) → if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) ∈ ℂ )
107 eldifsni ⊢ ( 𝑘 ∈ ( { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ∖ { 𝑚 } ) → 𝑘 ≠ 𝑚 )
108 107 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ∖ { 𝑚 } ) ) → 𝑘 ≠ 𝑚 )
109 108 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ∖ { 𝑚 } ) ) → ¬ 𝑘 = 𝑚 )
110 109 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ∖ { 𝑚 } ) ) → if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) = 0 )
111 fzfid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 1 ... 𝑚 ) ∈ Fin )
112 dvdsssfz1 ⊢ ( 𝑚 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ⊆ ( 1 ... 𝑚 ) )
113 112 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ⊆ ( 1 ... 𝑚 ) )
114 111 113 ssfid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ∈ Fin )
115 101 106 110 114 fsumss ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ { 𝑚 } if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) )
116 1 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
117 iftrue ⊢ ( 𝑘 = 𝑚 → if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) = ( 𝐹 ‘ 𝑘 ) )
118 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
119 117 118 eqtrd ⊢ ( 𝑘 = 𝑚 → if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) = ( 𝐹 ‘ 𝑚 ) )
120 119 sumsn ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝐹 ‘ 𝑚 ) ∈ ℂ ) → Σ 𝑘 ∈ { 𝑚 } if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) = ( 𝐹 ‘ 𝑚 ) )
121 54 116 120 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ { 𝑚 } if ( 𝑘 = 𝑚 , ( 𝐹 ‘ 𝑘 ) , 0 ) = ( 𝐹 ‘ 𝑚 ) )
122 95 115 121 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑚 / 𝑘 ) } ( ( μ ‘ 𝑗 ) · ( 𝐹 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑚 ) )
123 53 58 122 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( μ ‘ 𝑗 ) · ( 𝐺 ‘ ( 𝑚 / 𝑗 ) ) ) = ( 𝐹 ‘ 𝑚 ) )
124 123 mpteq2dva ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( μ ‘ 𝑗 ) · ( 𝐺 ‘ ( 𝑚 / 𝑗 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( 𝐹 ‘ 𝑚 ) ) )
125 3 124 eqtr4d ⊢ ( 𝜑 → 𝐹 = ( 𝑚 ∈ ℕ ↦ Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( ( μ ‘ 𝑗 ) · ( 𝐺 ‘ ( 𝑚 / 𝑗 ) ) ) ) )