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 ffvelcdm 
 |-  ( ( 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 mulridd 
 |-  ( ( ( 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 mullidd 
 |-  ( ( ( 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 eqtrid 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( 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 ) ) ) ) )