Metamath Proof Explorer

Theorem logsqvma

Description: A formula for log ^ 2 ( N ) in terms of the primes. Equation 10.4.6 of Shapiro, p. 418. (Contributed by Mario Carneiro, 13-May-2016)

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

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( N e. NN -> ( 1 ... N ) e. Fin )
2 dvdsssfz1 
 |-  ( N e. NN -> { x e. NN | x || N } C_ ( 1 ... N ) )
3 1 2 ssfid 
 |-  ( N e. NN -> { x e. NN | x || N } e. Fin )
4 fzfid 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> ( 1 ... d ) e. Fin )
5 elrabi 
 |-  ( d e. { x e. NN | x || N } -> d e. NN )
6 5 adantl 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> d e. NN )
7 dvdsssfz1 
 |-  ( d e. NN -> { x e. NN | x || d } C_ ( 1 ... d ) )
8 6 7 syl 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> { x e. NN | x || d } C_ ( 1 ... d ) )
9 4 8 ssfid 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> { x e. NN | x || d } e. Fin )
10 elrabi 
 |-  ( u e. { x e. NN | x || d } -> u e. NN )
11 10 ad2antll 
 |-  ( ( N e. NN /\ ( d e. { x e. NN | x || N } /\ u e. { x e. NN | x || d } ) ) -> u e. NN )
12 vmacl 
 |-  ( u e. NN -> ( Lam ` u ) e. RR )
13 11 12 syl 
 |-  ( ( N e. NN /\ ( d e. { x e. NN | x || N } /\ u e. { x e. NN | x || d } ) ) -> ( Lam ` u ) e. RR )
14 breq1 
 |-  ( x = u -> ( x || d <-> u || d ) )
15 14 elrab 
 |-  ( u e. { x e. NN | x || d } <-> ( u e. NN /\ u || d ) )
16 15 simprbi 
 |-  ( u e. { x e. NN | x || d } -> u || d )
17 16 ad2antll 
 |-  ( ( N e. NN /\ ( d e. { x e. NN | x || N } /\ u e. { x e. NN | x || d } ) ) -> u || d )
18 5 ad2antrl 
 |-  ( ( N e. NN /\ ( d e. { x e. NN | x || N } /\ u e. { x e. NN | x || d } ) ) -> d e. NN )
19 nndivdvds 
 |-  ( ( d e. NN /\ u e. NN ) -> ( u || d <-> ( d / u ) e. NN ) )
20 18 11 19 syl2anc 
 |-  ( ( N e. NN /\ ( d e. { x e. NN | x || N } /\ u e. { x e. NN | x || d } ) ) -> ( u || d <-> ( d / u ) e. NN ) )
21 17 20 mpbid 
 |-  ( ( N e. NN /\ ( d e. { x e. NN | x || N } /\ u e. { x e. NN | x || d } ) ) -> ( d / u ) e. NN )
22 vmacl 
 |-  ( ( d / u ) e. NN -> ( Lam ` ( d / u ) ) e. RR )
23 21 22 syl 
 |-  ( ( N e. NN /\ ( d e. { x e. NN | x || N } /\ u e. { x e. NN | x || d } ) ) -> ( Lam ` ( d / u ) ) e. RR )
24 13 23 remulcld 
 |-  ( ( N e. NN /\ ( d e. { x e. NN | x || N } /\ u e. { x e. NN | x || d } ) ) -> ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) e. RR )
25 24 recnd 
 |-  ( ( N e. NN /\ ( d e. { x e. NN | x || N } /\ u e. { x e. NN | x || d } ) ) -> ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) e. CC )
26 25 anassrs 
 |-  ( ( ( N e. NN /\ d e. { x e. NN | x || N } ) /\ u e. { x e. NN | x || d } ) -> ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) e. CC )
27 9 26 fsumcl 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> sum_ u e. { x e. NN | x || d } ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) e. CC )
28 vmacl 
 |-  ( d e. NN -> ( Lam ` d ) e. RR )
29 6 28 syl 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> ( Lam ` d ) e. RR )
30 6 nnrpd 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> d e. RR+ )
31 30 relogcld 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> ( log ` d ) e. RR )
32 29 31 remulcld 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> ( ( Lam ` d ) x. ( log ` d ) ) e. RR )
33 32 recnd 
 |-  ( ( N e. NN /\ d e. { x e. NN | x || N } ) -> ( ( Lam ` d ) x. ( log ` d ) ) e. CC )
34 3 27 33 fsumadd 
 |-  ( N e. NN -> sum_ d e. { x e. NN | x || N } ( sum_ u e. { x e. NN | x || d } ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) + ( ( Lam ` d ) x. ( log ` d ) ) ) = ( sum_ d e. { x e. NN | x || N } sum_ u e. { x e. NN | x || d } ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) + sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) ) )
35 id 
 |-  ( N e. NN -> N e. NN )
36 fvoveq1 
 |-  ( d = ( u x. k ) -> ( Lam ` ( d / u ) ) = ( Lam ` ( ( u x. k ) / u ) ) )
37 36 oveq2d 
 |-  ( d = ( u x. k ) -> ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) = ( ( Lam ` u ) x. ( Lam ` ( ( u x. k ) / u ) ) ) )
38 35 37 25 fsumdvdscom 
 |-  ( N e. NN -> sum_ d e. { x e. NN | x || N } sum_ u e. { x e. NN | x || d } ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) = sum_ u e. { x e. NN | x || N } sum_ k e. { x e. NN | x || ( N / u ) } ( ( Lam ` u ) x. ( Lam ` ( ( u x. k ) / u ) ) ) )
39 ssrab2 
 |-  { x e. NN | x || ( N / u ) } C_ NN
40 simpr 
 |-  ( ( ( N e. NN /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / u ) } ) -> k e. { x e. NN | x || ( N / u ) } )
41 39 40 sselid 
 |-  ( ( ( N e. NN /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / u ) } ) -> k e. NN )
42 41 nncnd 
 |-  ( ( ( N e. NN /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / u ) } ) -> k e. CC )
43 ssrab2 
 |-  { x e. NN | x || N } C_ NN
44 simpr 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> u e. { x e. NN | x || N } )
45 43 44 sselid 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> u e. NN )
46 45 nncnd 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> u e. CC )
47 46 adantr 
 |-  ( ( ( N e. NN /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / u ) } ) -> u e. CC )
48 45 nnne0d 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> u =/= 0 )
49 48 adantr 
 |-  ( ( ( N e. NN /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / u ) } ) -> u =/= 0 )
50 42 47 49 divcan3d 
 |-  ( ( ( N e. NN /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / u ) } ) -> ( ( u x. k ) / u ) = k )
51 50 fveq2d 
 |-  ( ( ( N e. NN /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / u ) } ) -> ( Lam ` ( ( u x. k ) / u ) ) = ( Lam ` k ) )
52 51 sumeq2dv 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> sum_ k e. { x e. NN | x || ( N / u ) } ( Lam ` ( ( u x. k ) / u ) ) = sum_ k e. { x e. NN | x || ( N / u ) } ( Lam ` k ) )
53 dvdsdivcl 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( N / u ) e. { x e. NN | x || N } )
54 43 53 sselid 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( N / u ) e. NN )
55 vmasum 
 |-  ( ( N / u ) e. NN -> sum_ k e. { x e. NN | x || ( N / u ) } ( Lam ` k ) = ( log ` ( N / u ) ) )
56 54 55 syl 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> sum_ k e. { x e. NN | x || ( N / u ) } ( Lam ` k ) = ( log ` ( N / u ) ) )
57 nnrp 
 |-  ( N e. NN -> N e. RR+ )
58 57 adantr 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> N e. RR+ )
59 45 nnrpd 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> u e. RR+ )
60 58 59 relogdivd 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( log ` ( N / u ) ) = ( ( log ` N ) - ( log ` u ) ) )
61 52 56 60 3eqtrd 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> sum_ k e. { x e. NN | x || ( N / u ) } ( Lam ` ( ( u x. k ) / u ) ) = ( ( log ` N ) - ( log ` u ) ) )
62 61 oveq2d 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( ( Lam ` u ) x. sum_ k e. { x e. NN | x || ( N / u ) } ( Lam ` ( ( u x. k ) / u ) ) ) = ( ( Lam ` u ) x. ( ( log ` N ) - ( log ` u ) ) ) )
63 fzfid 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( 1 ... ( N / u ) ) e. Fin )
64 dvdsssfz1 
 |-  ( ( N / u ) e. NN -> { x e. NN | x || ( N / u ) } C_ ( 1 ... ( N / u ) ) )
65 54 64 syl 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> { x e. NN | x || ( N / u ) } C_ ( 1 ... ( N / u ) ) )
66 63 65 ssfid 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> { x e. NN | x || ( N / u ) } e. Fin )
67 45 12 syl 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( Lam ` u ) e. RR )
68 67 recnd 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( Lam ` u ) e. CC )
69 vmacl 
 |-  ( k e. NN -> ( Lam ` k ) e. RR )
70 41 69 syl 
 |-  ( ( ( N e. NN /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / u ) } ) -> ( Lam ` k ) e. RR )
71 70 recnd 
 |-  ( ( ( N e. NN /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / u ) } ) -> ( Lam ` k ) e. CC )
72 51 71 eqeltrd 
 |-  ( ( ( N e. NN /\ u e. { x e. NN | x || N } ) /\ k e. { x e. NN | x || ( N / u ) } ) -> ( Lam ` ( ( u x. k ) / u ) ) e. CC )
73 66 68 72 fsummulc2 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( ( Lam ` u ) x. sum_ k e. { x e. NN | x || ( N / u ) } ( Lam ` ( ( u x. k ) / u ) ) ) = sum_ k e. { x e. NN | x || ( N / u ) } ( ( Lam ` u ) x. ( Lam ` ( ( u x. k ) / u ) ) ) )
74 relogcl 
 |-  ( N e. RR+ -> ( log ` N ) e. RR )
75 74 recnd 
 |-  ( N e. RR+ -> ( log ` N ) e. CC )
76 58 75 syl 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( log ` N ) e. CC )
77 59 relogcld 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( log ` u ) e. RR )
78 77 recnd 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( log ` u ) e. CC )
79 68 76 78 subdid 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( ( Lam ` u ) x. ( ( log ` N ) - ( log ` u ) ) ) = ( ( ( Lam ` u ) x. ( log ` N ) ) - ( ( Lam ` u ) x. ( log ` u ) ) ) )
80 62 73 79 3eqtr3d 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> sum_ k e. { x e. NN | x || ( N / u ) } ( ( Lam ` u ) x. ( Lam ` ( ( u x. k ) / u ) ) ) = ( ( ( Lam ` u ) x. ( log ` N ) ) - ( ( Lam ` u ) x. ( log ` u ) ) ) )
81 80 sumeq2dv 
 |-  ( N e. NN -> sum_ u e. { x e. NN | x || N } sum_ k e. { x e. NN | x || ( N / u ) } ( ( Lam ` u ) x. ( Lam ` ( ( u x. k ) / u ) ) ) = sum_ u e. { x e. NN | x || N } ( ( ( Lam ` u ) x. ( log ` N ) ) - ( ( Lam ` u ) x. ( log ` u ) ) ) )
82 68 76 mulcld 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( ( Lam ` u ) x. ( log ` N ) ) e. CC )
83 68 78 mulcld 
 |-  ( ( N e. NN /\ u e. { x e. NN | x || N } ) -> ( ( Lam ` u ) x. ( log ` u ) ) e. CC )
84 3 82 83 fsumsub 
 |-  ( N e. NN -> sum_ u e. { x e. NN | x || N } ( ( ( Lam ` u ) x. ( log ` N ) ) - ( ( Lam ` u ) x. ( log ` u ) ) ) = ( sum_ u e. { x e. NN | x || N } ( ( Lam ` u ) x. ( log ` N ) ) - sum_ u e. { x e. NN | x || N } ( ( Lam ` u ) x. ( log ` u ) ) ) )
85 57 75 syl 
 |-  ( N e. NN -> ( log ` N ) e. CC )
86 85 sqvald 
 |-  ( N e. NN -> ( ( log ` N ) ^ 2 ) = ( ( log ` N ) x. ( log ` N ) ) )
87 vmasum 
 |-  ( N e. NN -> sum_ u e. { x e. NN | x || N } ( Lam ` u ) = ( log ` N ) )
88 87 oveq1d 
 |-  ( N e. NN -> ( sum_ u e. { x e. NN | x || N } ( Lam ` u ) x. ( log ` N ) ) = ( ( log ` N ) x. ( log ` N ) ) )
89 3 85 68 fsummulc1 
 |-  ( N e. NN -> ( sum_ u e. { x e. NN | x || N } ( Lam ` u ) x. ( log ` N ) ) = sum_ u e. { x e. NN | x || N } ( ( Lam ` u ) x. ( log ` N ) ) )
90 86 88 89 3eqtr2rd 
 |-  ( N e. NN -> sum_ u e. { x e. NN | x || N } ( ( Lam ` u ) x. ( log ` N ) ) = ( ( log ` N ) ^ 2 ) )
91 fveq2 
 |-  ( u = d -> ( Lam ` u ) = ( Lam ` d ) )
92 fveq2 
 |-  ( u = d -> ( log ` u ) = ( log ` d ) )
93 91 92 oveq12d 
 |-  ( u = d -> ( ( Lam ` u ) x. ( log ` u ) ) = ( ( Lam ` d ) x. ( log ` d ) ) )
94 93 cbvsumv 
 |-  sum_ u e. { x e. NN | x || N } ( ( Lam ` u ) x. ( log ` u ) ) = sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) )
95 94 a1i 
 |-  ( N e. NN -> sum_ u e. { x e. NN | x || N } ( ( Lam ` u ) x. ( log ` u ) ) = sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) )
96 90 95 oveq12d 
 |-  ( N e. NN -> ( sum_ u e. { x e. NN | x || N } ( ( Lam ` u ) x. ( log ` N ) ) - sum_ u e. { x e. NN | x || N } ( ( Lam ` u ) x. ( log ` u ) ) ) = ( ( ( log ` N ) ^ 2 ) - sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) ) )
97 84 96 eqtrd 
 |-  ( N e. NN -> sum_ u e. { x e. NN | x || N } ( ( ( Lam ` u ) x. ( log ` N ) ) - ( ( Lam ` u ) x. ( log ` u ) ) ) = ( ( ( log ` N ) ^ 2 ) - sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) ) )
98 38 81 97 3eqtrd 
 |-  ( N e. NN -> sum_ d e. { x e. NN | x || N } sum_ u e. { x e. NN | x || d } ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) = ( ( ( log ` N ) ^ 2 ) - sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) ) )
99 98 oveq1d 
 |-  ( N e. NN -> ( sum_ d e. { x e. NN | x || N } sum_ u e. { x e. NN | x || d } ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) + sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) ) = ( ( ( ( log ` N ) ^ 2 ) - sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) ) + sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) ) )
100 85 sqcld 
 |-  ( N e. NN -> ( ( log ` N ) ^ 2 ) e. CC )
101 3 33 fsumcl 
 |-  ( N e. NN -> sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) e. CC )
102 100 101 npcand 
 |-  ( N e. NN -> ( ( ( ( log ` N ) ^ 2 ) - sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) ) + sum_ d e. { x e. NN | x || N } ( ( Lam ` d ) x. ( log ` d ) ) ) = ( ( log ` N ) ^ 2 ) )
103 34 99 102 3eqtrd 
 |-  ( N e. NN -> sum_ d e. { x e. NN | x || N } ( sum_ u e. { x e. NN | x || d } ( ( Lam ` u ) x. ( Lam ` ( d / u ) ) ) + ( ( Lam ` d ) x. ( log ` d ) ) ) = ( ( log ` N ) ^ 2 ) )