Metamath Proof Explorer

Theorem logsqvma2

Description: The Möbius inverse of logsqvma . Equation 10.4.8 of Shapiro, p. 418. (Contributed by Mario Carneiro, 13-May-2016)

Ref Expression
Assertion logsqvma2 
|- ( N e. NN -> sum_ d e. { x e. NN | x || N } ( ( mmu ` d ) x. ( ( log ` ( N / d ) ) ^ 2 ) ) = ( sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( Lam ` ( N / d ) ) ) + ( ( Lam ` N ) x. ( log ` N ) ) ) )

Proof

Step Hyp Ref Expression
1 dvdsfi 
 |-  ( k e. NN -> { x e. NN | x || k } e. Fin )
2 ssrab2 
 |-  { x e. NN | x || k } C_ NN
3 simpr 
 |-  ( ( k e. NN /\ d e. { x e. NN | x || k } ) -> d e. { x e. NN | x || k } )
4 2 3 sselid 
 |-  ( ( k e. NN /\ d e. { x e. NN | x || k } ) -> d e. NN )
5 vmacl 
 |-  ( d e. NN -> ( Lam ` d ) e. RR )
6 4 5 syl 
 |-  ( ( k e. NN /\ d e. { x e. NN | x || k } ) -> ( Lam ` d ) e. RR )
7 dvdsdivcl 
 |-  ( ( k e. NN /\ d e. { x e. NN | x || k } ) -> ( k / d ) e. { x e. NN | x || k } )
8 2 7 sselid 
 |-  ( ( k e. NN /\ d e. { x e. NN | x || k } ) -> ( k / d ) e. NN )
9 vmacl 
 |-  ( ( k / d ) e. NN -> ( Lam ` ( k / d ) ) e. RR )
10 8 9 syl 
 |-  ( ( k e. NN /\ d e. { x e. NN | x || k } ) -> ( Lam ` ( k / d ) ) e. RR )
11 6 10 remulcld 
 |-  ( ( k e. NN /\ d e. { x e. NN | x || k } ) -> ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) e. RR )
12 1 11 fsumrecl 
 |-  ( k e. NN -> sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) e. RR )
13 vmacl 
 |-  ( k e. NN -> ( Lam ` k ) e. RR )
14 nnrp 
 |-  ( k e. NN -> k e. RR+ )
15 14 relogcld 
 |-  ( k e. NN -> ( log ` k ) e. RR )
16 13 15 remulcld 
 |-  ( k e. NN -> ( ( Lam ` k ) x. ( log ` k ) ) e. RR )
17 12 16 readdcld 
 |-  ( k e. NN -> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) e. RR )
18 17 recnd 
 |-  ( k e. NN -> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) e. CC )
19 18 adantl 
 |-  ( ( N e. NN /\ k e. NN ) -> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) e. CC )
20 19 fmpttd 
 |-  ( N e. NN -> ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) ) : NN --> CC )
21 ssrab2 
 |-  { x e. NN | x || n } C_ NN
22 simpr 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ m e. { x e. NN | x || n } ) -> m e. { x e. NN | x || n } )
23 21 22 sselid 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ m e. { x e. NN | x || n } ) -> m e. NN )
24 breq2 
 |-  ( k = m -> ( x || k <-> x || m ) )
25 24 rabbidv 
 |-  ( k = m -> { x e. NN | x || k } = { x e. NN | x || m } )
26 fvoveq1 
 |-  ( k = m -> ( Lam ` ( k / d ) ) = ( Lam ` ( m / d ) ) )
27 26 oveq2d 
 |-  ( k = m -> ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) = ( ( Lam ` d ) x. ( Lam ` ( m / d ) ) ) )
28 27 adantr 
 |-  ( ( k = m /\ d e. { x e. NN | x || k } ) -> ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) = ( ( Lam ` d ) x. ( Lam ` ( m / d ) ) ) )
29 25 28 sumeq12dv 
 |-  ( k = m -> sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) = sum_ d e. { x e. NN | x || m } ( ( Lam ` d ) x. ( Lam ` ( m / d ) ) ) )
30 fveq2 
 |-  ( k = m -> ( Lam ` k ) = ( Lam ` m ) )
31 fveq2 
 |-  ( k = m -> ( log ` k ) = ( log ` m ) )
32 30 31 oveq12d 
 |-  ( k = m -> ( ( Lam ` k ) x. ( log ` k ) ) = ( ( Lam ` m ) x. ( log ` m ) ) )
33 29 32 oveq12d 
 |-  ( k = m -> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) = ( sum_ d e. { x e. NN | x || m } ( ( Lam ` d ) x. ( Lam ` ( m / d ) ) ) + ( ( Lam ` m ) x. ( log ` m ) ) ) )
34 eqid 
 |-  ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) ) = ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) )
35 ovex 
 |-  ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) e. _V
36 33 34 35 fvmpt3i 
 |-  ( m e. NN -> ( ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) ) ` m ) = ( sum_ d e. { x e. NN | x || m } ( ( Lam ` d ) x. ( Lam ` ( m / d ) ) ) + ( ( Lam ` m ) x. ( log ` m ) ) ) )
37 23 36 syl 
 |-  ( ( ( N e. NN /\ n e. NN ) /\ m e. { x e. NN | x || n } ) -> ( ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) ) ` m ) = ( sum_ d e. { x e. NN | x || m } ( ( Lam ` d ) x. ( Lam ` ( m / d ) ) ) + ( ( Lam ` m ) x. ( log ` m ) ) ) )
38 37 sumeq2dv 
 |-  ( ( N e. NN /\ n e. NN ) -> sum_ m e. { x e. NN | x || n } ( ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) ) ` m ) = sum_ m e. { x e. NN | x || n } ( sum_ d e. { x e. NN | x || m } ( ( Lam ` d ) x. ( Lam ` ( m / d ) ) ) + ( ( Lam ` m ) x. ( log ` m ) ) ) )
39 logsqvma 
 |-  ( n e. NN -> sum_ m e. { x e. NN | x || n } ( sum_ d e. { x e. NN | x || m } ( ( Lam ` d ) x. ( Lam ` ( m / d ) ) ) + ( ( Lam ` m ) x. ( log ` m ) ) ) = ( ( log ` n ) ^ 2 ) )
40 39 adantl 
 |-  ( ( N e. NN /\ n e. NN ) -> sum_ m e. { x e. NN | x || n } ( sum_ d e. { x e. NN | x || m } ( ( Lam ` d ) x. ( Lam ` ( m / d ) ) ) + ( ( Lam ` m ) x. ( log ` m ) ) ) = ( ( log ` n ) ^ 2 ) )
41 38 40 eqtr2d 
 |-  ( ( N e. NN /\ n e. NN ) -> ( ( log ` n ) ^ 2 ) = sum_ m e. { x e. NN | x || n } ( ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) ) ` m ) )
42 41 mpteq2dva 
 |-  ( N e. NN -> ( n e. NN |-> ( ( log ` n ) ^ 2 ) ) = ( n e. NN |-> sum_ m e. { x e. NN | x || n } ( ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) ) ` m ) ) )
43 20 42 muinv 
 |-  ( N e. NN -> ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) ) = ( i e. NN |-> sum_ j e. { x e. NN | x || i } ( ( mmu ` j ) x. ( ( n e. NN |-> ( ( log ` n ) ^ 2 ) ) ` ( i / j ) ) ) ) )
44 43 fveq1d 
 |-  ( N e. NN -> ( ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) ) ` N ) = ( ( i e. NN |-> sum_ j e. { x e. NN | x || i } ( ( mmu ` j ) x. ( ( n e. NN |-> ( ( log ` n ) ^ 2 ) ) ` ( i / j ) ) ) ) ` N ) )
45 breq2 
 |-  ( k = N -> ( x || k <-> x || N ) )
46 45 rabbidv 
 |-  ( k = N -> { x e. NN | x || k } = { x e. NN | x || N } )
47 fvoveq1 
 |-  ( k = N -> ( Lam ` ( k / d ) ) = ( Lam ` ( N / d ) ) )
48 47 oveq2d 
 |-  ( k = N -> ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) = ( ( Lam ` d ) x. ( Lam ` ( N / d ) ) ) )
49 48 adantr 
 |-  ( ( k = N /\ d e. { x e. NN | x || k } ) -> ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) = ( ( Lam ` d ) x. ( Lam ` ( N / d ) ) ) )
50 46 49 sumeq12dv 
 |-  ( k = N -> sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) = sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( Lam ` ( N / d ) ) ) )
51 fveq2 
 |-  ( k = N -> ( Lam ` k ) = ( Lam ` N ) )
52 fveq2 
 |-  ( k = N -> ( log ` k ) = ( log ` N ) )
53 51 52 oveq12d 
 |-  ( k = N -> ( ( Lam ` k ) x. ( log ` k ) ) = ( ( Lam ` N ) x. ( log ` N ) ) )
54 50 53 oveq12d 
 |-  ( k = N -> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) = ( sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( Lam ` ( N / d ) ) ) + ( ( Lam ` N ) x. ( log ` N ) ) ) )
55 54 34 35 fvmpt3i 
 |-  ( N e. NN -> ( ( k e. NN |-> ( sum_ d e. { x e. NN | x || k } ( ( Lam ` d ) x. ( Lam ` ( k / d ) ) ) + ( ( Lam ` k ) x. ( log ` k ) ) ) ) ` N ) = ( sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( Lam ` ( N / d ) ) ) + ( ( Lam ` N ) x. ( log ` N ) ) ) )
56 fveq2 
 |-  ( j = d -> ( mmu ` j ) = ( mmu ` d ) )
57 oveq2 
 |-  ( j = d -> ( i / j ) = ( i / d ) )
58 57 fveq2d 
 |-  ( j = d -> ( log ` ( i / j ) ) = ( log ` ( i / d ) ) )
59 58 oveq1d 
 |-  ( j = d -> ( ( log ` ( i / j ) ) ^ 2 ) = ( ( log ` ( i / d ) ) ^ 2 ) )
60 56 59 oveq12d 
 |-  ( j = d -> ( ( mmu ` j ) x. ( ( log ` ( i / j ) ) ^ 2 ) ) = ( ( mmu ` d ) x. ( ( log ` ( i / d ) ) ^ 2 ) ) )
61 60 cbvsumv 
 |-  sum_ j e. { x e. NN | x || i } ( ( mmu ` j ) x. ( ( log ` ( i / j ) ) ^ 2 ) ) = sum_ d e. { x e. NN | x || i } ( ( mmu ` d ) x. ( ( log ` ( i / d ) ) ^ 2 ) )
62 breq2 
 |-  ( i = N -> ( x || i <-> x || N ) )
63 62 rabbidv 
 |-  ( i = N -> { x e. NN | x || i } = { x e. NN | x || N } )
64 fvoveq1 
 |-  ( i = N -> ( log ` ( i / d ) ) = ( log ` ( N / d ) ) )
65 64 oveq1d 
 |-  ( i = N -> ( ( log ` ( i / d ) ) ^ 2 ) = ( ( log ` ( N / d ) ) ^ 2 ) )
66 65 oveq2d 
 |-  ( i = N -> ( ( mmu ` d ) x. ( ( log ` ( i / d ) ) ^ 2 ) ) = ( ( mmu ` d ) x. ( ( log ` ( N / d ) ) ^ 2 ) ) )
67 66 adantr 
 |-  ( ( i = N /\ d e. { x e. NN | x || i } ) -> ( ( mmu ` d ) x. ( ( log ` ( i / d ) ) ^ 2 ) ) = ( ( mmu ` d ) x. ( ( log ` ( N / d ) ) ^ 2 ) ) )
68 63 67 sumeq12dv 
 |-  ( i = N -> sum_ d e. { x e. NN | x || i } ( ( mmu ` d ) x. ( ( log ` ( i / d ) ) ^ 2 ) ) = sum_ d e. { x e. NN | x || N } ( ( mmu ` d ) x. ( ( log ` ( N / d ) ) ^ 2 ) ) )
69 61 68 eqtrid 
 |-  ( i = N -> sum_ j e. { x e. NN | x || i } ( ( mmu ` j ) x. ( ( log ` ( i / j ) ) ^ 2 ) ) = sum_ d e. { x e. NN | x || N } ( ( mmu ` d ) x. ( ( log ` ( N / d ) ) ^ 2 ) ) )
70 ssrab2 
 |-  { x e. NN | x || i } C_ NN
71 dvdsdivcl 
 |-  ( ( i e. NN /\ j e. { x e. NN | x || i } ) -> ( i / j ) e. { x e. NN | x || i } )
72 70 71 sselid 
 |-  ( ( i e. NN /\ j e. { x e. NN | x || i } ) -> ( i / j ) e. NN )
73 fveq2 
 |-  ( n = ( i / j ) -> ( log ` n ) = ( log ` ( i / j ) ) )
74 73 oveq1d 
 |-  ( n = ( i / j ) -> ( ( log ` n ) ^ 2 ) = ( ( log ` ( i / j ) ) ^ 2 ) )
75 eqid 
 |-  ( n e. NN |-> ( ( log ` n ) ^ 2 ) ) = ( n e. NN |-> ( ( log ` n ) ^ 2 ) )
76 ovex 
 |-  ( ( log ` n ) ^ 2 ) e. _V
77 74 75 76 fvmpt3i 
 |-  ( ( i / j ) e. NN -> ( ( n e. NN |-> ( ( log ` n ) ^ 2 ) ) ` ( i / j ) ) = ( ( log ` ( i / j ) ) ^ 2 ) )
78 72 77 syl 
 |-  ( ( i e. NN /\ j e. { x e. NN | x || i } ) -> ( ( n e. NN |-> ( ( log ` n ) ^ 2 ) ) ` ( i / j ) ) = ( ( log ` ( i / j ) ) ^ 2 ) )
79 78 oveq2d 
 |-  ( ( i e. NN /\ j e. { x e. NN | x || i } ) -> ( ( mmu ` j ) x. ( ( n e. NN |-> ( ( log ` n ) ^ 2 ) ) ` ( i / j ) ) ) = ( ( mmu ` j ) x. ( ( log ` ( i / j ) ) ^ 2 ) ) )
80 79 sumeq2dv 
 |-  ( i e. NN -> sum_ j e. { x e. NN | x || i } ( ( mmu ` j ) x. ( ( n e. NN |-> ( ( log ` n ) ^ 2 ) ) ` ( i / j ) ) ) = sum_ j e. { x e. NN | x || i } ( ( mmu ` j ) x. ( ( log ` ( i / j ) ) ^ 2 ) ) )
81 80 mpteq2ia 
 |-  ( i e. NN |-> sum_ j e. { x e. NN | x || i } ( ( mmu ` j ) x. ( ( n e. NN |-> ( ( log ` n ) ^ 2 ) ) ` ( i / j ) ) ) ) = ( i e. NN |-> sum_ j e. { x e. NN | x || i } ( ( mmu ` j ) x. ( ( log ` ( i / j ) ) ^ 2 ) ) )
82 sumex 
 |-  sum_ j e. { x e. NN | x || i } ( ( mmu ` j ) x. ( ( log ` ( i / j ) ) ^ 2 ) ) e. _V
83 69 81 82 fvmpt3i 
 |-  ( N e. NN -> ( ( i e. NN |-> sum_ j e. { x e. NN | x || i } ( ( mmu ` j ) x. ( ( n e. NN |-> ( ( log ` n ) ^ 2 ) ) ` ( i / j ) ) ) ) ` N ) = sum_ d e. { x e. NN | x || N } ( ( mmu ` d ) x. ( ( log ` ( N / d ) ) ^ 2 ) ) )
84 44 55 83 3eqtr3rd 
 |-  ( N e. NN -> sum_ d e. { x e. NN | x || N } ( ( mmu ` d ) x. ( ( log ` ( N / d ) ) ^ 2 ) ) = ( sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( Lam ` ( N / d ) ) ) + ( ( Lam ` N ) x. ( log ` N ) ) ) )