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
|- ( ph -> F : NN --> CC )
muinv.2
|- ( ph -> G = ( n e. NN |-> sum_ k e. { x e. NN | x || n } ( F ` k ) ) )
Assertion muinv
|- ( ph -> F = ( m e. NN |-> sum_ j e. { x e. NN | x || m } ( ( mmu ` j ) x. ( G ` ( m / j ) ) ) ) )

Proof

Step Hyp Ref Expression
1 muinv.1
 |-  ( ph -> F : NN --> CC )
2 muinv.2
 |-  ( ph -> G = ( n e. NN |-> sum_ k e. { x e. NN | x || n } ( F ` k ) ) )
3 1 feqmptd
 |-  ( ph -> F = ( m e. NN |-> ( F ` m ) ) )
4 2 ad2antrr
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> G = ( n e. NN |-> sum_ k e. { x e. NN | x || n } ( F ` k ) ) )
5 4 fveq1d
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( G ` ( m / j ) ) = ( ( n e. NN |-> sum_ k e. { x e. NN | x || n } ( F ` k ) ) ` ( m / j ) ) )
6 breq1
 |-  ( x = j -> ( x || m <-> j || m ) )
7 6 elrab
 |-  ( j e. { x e. NN | x || m } <-> ( j e. NN /\ j || m ) )
8 7 simprbi
 |-  ( j e. { x e. NN | x || m } -> j || m )
9 8 adantl
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> j || m )
10 elrabi
 |-  ( j e. { x e. NN | x || m } -> j e. NN )
11 10 adantl
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> j e. NN )
12 11 nnzd
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> j e. ZZ )
13 11 nnne0d
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> j =/= 0 )
14 nnz
 |-  ( m e. NN -> m e. ZZ )
15 14 ad2antlr
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> m e. ZZ )
16 dvdsval2
 |-  ( ( j e. ZZ /\ j =/= 0 /\ m e. ZZ ) -> ( j || m <-> ( m / j ) e. ZZ ) )
17 12 13 15 16 syl3anc
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( j || m <-> ( m / j ) e. ZZ ) )
18 9 17 mpbid
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( m / j ) e. ZZ )
19 nnre
 |-  ( m e. NN -> m e. RR )
20 nngt0
 |-  ( m e. NN -> 0 < m )
21 19 20 jca
 |-  ( m e. NN -> ( m e. RR /\ 0 < m ) )
22 21 ad2antlr
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( m e. RR /\ 0 < m ) )
23 nnre
 |-  ( j e. NN -> j e. RR )
24 nngt0
 |-  ( j e. NN -> 0 < j )
25 23 24 jca
 |-  ( j e. NN -> ( j e. RR /\ 0 < j ) )
26 11 25 syl
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( j e. RR /\ 0 < j ) )
27 divgt0
 |-  ( ( ( m e. RR /\ 0 < m ) /\ ( j e. RR /\ 0 < j ) ) -> 0 < ( m / j ) )
28 22 26 27 syl2anc
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> 0 < ( m / j ) )
29 elnnz
 |-  ( ( m / j ) e. NN <-> ( ( m / j ) e. ZZ /\ 0 < ( m / j ) ) )
30 18 28 29 sylanbrc
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( m / j ) e. NN )
31 breq2
 |-  ( n = ( m / j ) -> ( x || n <-> x || ( m / j ) ) )
32 31 rabbidv
 |-  ( n = ( m / j ) -> { x e. NN | x || n } = { x e. NN | x || ( m / j ) } )
33 32 sumeq1d
 |-  ( n = ( m / j ) -> sum_ k e. { x e. NN | x || n } ( F ` k ) = sum_ k e. { x e. NN | x || ( m / j ) } ( F ` k ) )
34 eqid
 |-  ( n e. NN |-> sum_ k e. { x e. NN | x || n } ( F ` k ) ) = ( n e. NN |-> sum_ k e. { x e. NN | x || n } ( F ` k ) )
35 sumex
 |-  sum_ k e. { x e. NN | x || ( m / j ) } ( F ` k ) e. _V
36 33 34 35 fvmpt
 |-  ( ( m / j ) e. NN -> ( ( n e. NN |-> sum_ k e. { x e. NN | x || n } ( F ` k ) ) ` ( m / j ) ) = sum_ k e. { x e. NN | x || ( m / j ) } ( F ` k ) )
37 30 36 syl
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( ( n e. NN |-> sum_ k e. { x e. NN | x || n } ( F ` k ) ) ` ( m / j ) ) = sum_ k e. { x e. NN | x || ( m / j ) } ( F ` k ) )
38 5 37 eqtrd
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( G ` ( m / j ) ) = sum_ k e. { x e. NN | x || ( m / j ) } ( F ` k ) )
39 38 oveq2d
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( ( mmu ` j ) x. ( G ` ( m / j ) ) ) = ( ( mmu ` j ) x. sum_ k e. { x e. NN | x || ( m / j ) } ( F ` k ) ) )
40 fzfid
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( 1 ... ( m / j ) ) e. Fin )
41 dvdsssfz1
 |-  ( ( m / j ) e. NN -> { x e. NN | x || ( m / j ) } C_ ( 1 ... ( m / j ) ) )
42 30 41 syl
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> { x e. NN | x || ( m / j ) } C_ ( 1 ... ( m / j ) ) )
43 40 42 ssfid
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> { x e. NN | x || ( m / j ) } e. Fin )
44 mucl
 |-  ( j e. NN -> ( mmu ` j ) e. ZZ )
45 11 44 syl
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( mmu ` j ) e. ZZ )
46 45 zcnd
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( mmu ` j ) e. CC )
47 1 ad2antrr
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> F : NN --> CC )
48 elrabi
 |-  ( k e. { x e. NN | x || ( m / j ) } -> k e. NN )
49 ffvelrn
 |-  ( ( F : NN --> CC /\ k e. NN ) -> ( F ` k ) e. CC )
50 47 48 49 syl2an
 |-  ( ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) /\ k e. { x e. NN | x || ( m / j ) } ) -> ( F ` k ) e. CC )
51 43 46 50 fsummulc2
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( ( mmu ` j ) x. sum_ k e. { x e. NN | x || ( m / j ) } ( F ` k ) ) = sum_ k e. { x e. NN | x || ( m / j ) } ( ( mmu ` j ) x. ( F ` k ) ) )
52 39 51 eqtrd
 |-  ( ( ( ph /\ m e. NN ) /\ j e. { x e. NN | x || m } ) -> ( ( mmu ` j ) x. ( G ` ( m / j ) ) ) = sum_ k e. { x e. NN | x || ( m / j ) } ( ( mmu ` j ) x. ( F ` k ) ) )
53 52 sumeq2dv
 |-  ( ( ph /\ m e. NN ) -> sum_ j e. { x e. NN | x || m } ( ( mmu ` j ) x. ( G ` ( m / j ) ) ) = sum_ j e. { x e. NN | x || m } sum_ k e. { x e. NN | x || ( m / j ) } ( ( mmu ` j ) x. ( F ` k ) ) )
54 simpr
 |-  ( ( ph /\ m e. NN ) -> m e. NN )
55 46 adantrr
 |-  ( ( ( ph /\ m e. NN ) /\ ( j e. { x e. NN | x || m } /\ k e. { x e. NN | x || ( m / j ) } ) ) -> ( mmu ` j ) e. CC )
56 50 anasss
 |-  ( ( ( ph /\ m e. NN ) /\ ( j e. { x e. NN | x || m } /\ k e. { x e. NN | x || ( m / j ) } ) ) -> ( F ` k ) e. CC )
57 55 56 mulcld
 |-  ( ( ( ph /\ m e. NN ) /\ ( j e. { x e. NN | x || m } /\ k e. { x e. NN | x || ( m / j ) } ) ) -> ( ( mmu ` j ) x. ( F ` k ) ) e. CC )
58 54 57 fsumdvdsdiag
 |-  ( ( ph /\ m e. NN ) -> sum_ j e. { x e. NN | x || m } sum_ k e. { x e. NN | x || ( m / j ) } ( ( mmu ` j ) x. ( F ` k ) ) = sum_ k e. { x e. NN | x || m } sum_ j e. { x e. NN | x || ( m / k ) } ( ( mmu ` j ) x. ( F ` k ) ) )
59 ssrab2
 |-  { x e. NN | x || m } C_ NN
60 dvdsdivcl
 |-  ( ( m e. NN /\ k e. { x e. NN | x || m } ) -> ( m / k ) e. { x e. NN | x || m } )
61 60 adantll
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( m / k ) e. { x e. NN | x || m } )
62 59 61 sselid
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( m / k ) e. NN )
63 musum
 |-  ( ( m / k ) e. NN -> sum_ j e. { x e. NN | x || ( m / k ) } ( mmu ` j ) = if ( ( m / k ) = 1 , 1 , 0 ) )
64 62 63 syl
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> sum_ j e. { x e. NN | x || ( m / k ) } ( mmu ` j ) = if ( ( m / k ) = 1 , 1 , 0 ) )
65 64 oveq1d
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( sum_ j e. { x e. NN | x || ( m / k ) } ( mmu ` j ) x. ( F ` k ) ) = ( if ( ( m / k ) = 1 , 1 , 0 ) x. ( F ` k ) ) )
66 fzfid
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( 1 ... ( m / k ) ) e. Fin )
67 dvdsssfz1
 |-  ( ( m / k ) e. NN -> { x e. NN | x || ( m / k ) } C_ ( 1 ... ( m / k ) ) )
68 62 67 syl
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> { x e. NN | x || ( m / k ) } C_ ( 1 ... ( m / k ) ) )
69 66 68 ssfid
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> { x e. NN | x || ( m / k ) } e. Fin )
70 1 adantr
 |-  ( ( ph /\ m e. NN ) -> F : NN --> CC )
71 elrabi
 |-  ( k e. { x e. NN | x || m } -> k e. NN )
72 70 71 49 syl2an
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( F ` k ) e. CC )
73 ssrab2
 |-  { x e. NN | x || ( m / k ) } C_ NN
74 simpr
 |-  ( ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) /\ j e. { x e. NN | x || ( m / k ) } ) -> j e. { x e. NN | x || ( m / k ) } )
75 73 74 sselid
 |-  ( ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) /\ j e. { x e. NN | x || ( m / k ) } ) -> j e. NN )
76 75 44 syl
 |-  ( ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) /\ j e. { x e. NN | x || ( m / k ) } ) -> ( mmu ` j ) e. ZZ )
77 76 zcnd
 |-  ( ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) /\ j e. { x e. NN | x || ( m / k ) } ) -> ( mmu ` j ) e. CC )
78 69 72 77 fsummulc1
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( sum_ j e. { x e. NN | x || ( m / k ) } ( mmu ` j ) x. ( F ` k ) ) = sum_ j e. { x e. NN | x || ( m / k ) } ( ( mmu ` j ) x. ( F ` k ) ) )
79 ovif
 |-  ( if ( ( m / k ) = 1 , 1 , 0 ) x. ( F ` k ) ) = if ( ( m / k ) = 1 , ( 1 x. ( F ` k ) ) , ( 0 x. ( F ` k ) ) )
80 nncn
 |-  ( m e. NN -> m e. CC )
81 80 ad2antlr
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> m e. CC )
82 71 adantl
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> k e. NN )
83 82 nncnd
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> k e. CC )
84 1cnd
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> 1 e. CC )
85 82 nnne0d
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> k =/= 0 )
86 81 83 84 85 divmuld
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( ( m / k ) = 1 <-> ( k x. 1 ) = m ) )
87 83 mulid1d
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( k x. 1 ) = k )
88 87 eqeq1d
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( ( k x. 1 ) = m <-> k = m ) )
89 86 88 bitrd
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( ( m / k ) = 1 <-> k = m ) )
90 72 mulid2d
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( 1 x. ( F ` k ) ) = ( F ` k ) )
91 72 mul02d
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( 0 x. ( F ` k ) ) = 0 )
92 89 90 91 ifbieq12d
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> if ( ( m / k ) = 1 , ( 1 x. ( F ` k ) ) , ( 0 x. ( F ` k ) ) ) = if ( k = m , ( F ` k ) , 0 ) )
93 79 92 syl5eq
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> ( if ( ( m / k ) = 1 , 1 , 0 ) x. ( F ` k ) ) = if ( k = m , ( F ` k ) , 0 ) )
94 65 78 93 3eqtr3d
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { x e. NN | x || m } ) -> sum_ j e. { x e. NN | x || ( m / k ) } ( ( mmu ` j ) x. ( F ` k ) ) = if ( k = m , ( F ` k ) , 0 ) )
95 94 sumeq2dv
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. { x e. NN | x || m } sum_ j e. { x e. NN | x || ( m / k ) } ( ( mmu ` j ) x. ( F ` k ) ) = sum_ k e. { x e. NN | x || m } if ( k = m , ( F ` k ) , 0 ) )
96 breq1
 |-  ( x = m -> ( x || m <-> m || m ) )
97 54 nnzd
 |-  ( ( ph /\ m e. NN ) -> m e. ZZ )
98 iddvds
 |-  ( m e. ZZ -> m || m )
99 97 98 syl
 |-  ( ( ph /\ m e. NN ) -> m || m )
100 96 54 99 elrabd
 |-  ( ( ph /\ m e. NN ) -> m e. { x e. NN | x || m } )
101 100 snssd
 |-  ( ( ph /\ m e. NN ) -> { m } C_ { x e. NN | x || m } )
102 101 sselda
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { m } ) -> k e. { x e. NN | x || m } )
103 102 72 syldan
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { m } ) -> ( F ` k ) e. CC )
104 0cn
 |-  0 e. CC
105 ifcl
 |-  ( ( ( F ` k ) e. CC /\ 0 e. CC ) -> if ( k = m , ( F ` k ) , 0 ) e. CC )
106 103 104 105 sylancl
 |-  ( ( ( ph /\ m e. NN ) /\ k e. { m } ) -> if ( k = m , ( F ` k ) , 0 ) e. CC )
107 eldifsni
 |-  ( k e. ( { x e. NN | x || m } \ { m } ) -> k =/= m )
108 107 adantl
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( { x e. NN | x || m } \ { m } ) ) -> k =/= m )
109 108 neneqd
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( { x e. NN | x || m } \ { m } ) ) -> -. k = m )
110 109 iffalsed
 |-  ( ( ( ph /\ m e. NN ) /\ k e. ( { x e. NN | x || m } \ { m } ) ) -> if ( k = m , ( F ` k ) , 0 ) = 0 )
111 fzfid
 |-  ( ( ph /\ m e. NN ) -> ( 1 ... m ) e. Fin )
112 dvdsssfz1
 |-  ( m e. NN -> { x e. NN | x || m } C_ ( 1 ... m ) )
113 112 adantl
 |-  ( ( ph /\ m e. NN ) -> { x e. NN | x || m } C_ ( 1 ... m ) )
114 111 113 ssfid
 |-  ( ( ph /\ m e. NN ) -> { x e. NN | x || m } e. Fin )
115 101 106 110 114 fsumss
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. { m } if ( k = m , ( F ` k ) , 0 ) = sum_ k e. { x e. NN | x || m } if ( k = m , ( F ` k ) , 0 ) )
116 1 ffvelrnda
 |-  ( ( ph /\ m e. NN ) -> ( F ` m ) e. CC )
117 iftrue
 |-  ( k = m -> if ( k = m , ( F ` k ) , 0 ) = ( F ` k ) )
118 fveq2
 |-  ( k = m -> ( F ` k ) = ( F ` m ) )
119 117 118 eqtrd
 |-  ( k = m -> if ( k = m , ( F ` k ) , 0 ) = ( F ` m ) )
120 119 sumsn
 |-  ( ( m e. NN /\ ( F ` m ) e. CC ) -> sum_ k e. { m } if ( k = m , ( F ` k ) , 0 ) = ( F ` m ) )
121 54 116 120 syl2anc
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. { m } if ( k = m , ( F ` k ) , 0 ) = ( F ` m ) )
122 95 115 121 3eqtr2d
 |-  ( ( ph /\ m e. NN ) -> sum_ k e. { x e. NN | x || m } sum_ j e. { x e. NN | x || ( m / k ) } ( ( mmu ` j ) x. ( F ` k ) ) = ( F ` m ) )
123 53 58 122 3eqtrd
 |-  ( ( ph /\ m e. NN ) -> sum_ j e. { x e. NN | x || m } ( ( mmu ` j ) x. ( G ` ( m / j ) ) ) = ( F ` m ) )
124 123 mpteq2dva
 |-  ( ph -> ( m e. NN |-> sum_ j e. { x e. NN | x || m } ( ( mmu ` j ) x. ( G ` ( m / j ) ) ) ) = ( m e. NN |-> ( F ` m ) ) )
125 3 124 eqtr4d
 |-  ( ph -> F = ( m e. NN |-> sum_ j e. { x e. NN | x || m } ( ( mmu ` j ) x. ( G ` ( m / j ) ) ) ) )