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 ⊢φ→F:ℕ⟶ℂ
muinv.2 ⊢φ→G=n∈ℕ⟼∑k∈x∈ℕ|x∥nF⁡k
Assertion muinv ⊢φ→F=m∈ℕ⟼∑j∈x∈ℕ|x∥mμ⁡j⁢G⁡mj

Proof

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