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