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