Metamath Proof Explorer

Theorem logdivbnd

Description: A bound on a sum of logs, used in pntlemk . This is not as precise as logdivsum in its asymptotic behavior, but it is valid for all N and does not require a limit value. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Assertion logdivbnd 
|- ( N e. NN -> sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` N ) + 1 ) ^ 2 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 fzfid 
 |-  ( N e. NN -> ( 1 ... N ) e. Fin )
3 elfzuz 
 |-  ( n e. ( 1 ... N ) -> n e. ( ZZ>= ` 1 ) )
4 3 adantl 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> n e. ( ZZ>= ` 1 ) )
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 4 5 eleqtrrdi 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> n e. NN )
7 6 nnrpd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> n e. RR+ )
8 7 relogcld 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( log ` n ) e. RR )
9 8 6 nndivred 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( ( log ` n ) / n ) e. RR )
10 2 9 fsumrecl 
 |-  ( N e. NN -> sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) e. RR )
11 remulcl 
 |-  ( ( 2 e. RR /\ sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) e. RR ) -> ( 2 x. sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) ) e. RR )
12 1 10 11 sylancr 
 |-  ( N e. NN -> ( 2 x. sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) ) e. RR )
13 elfznn 
 |-  ( i e. ( 1 ... N ) -> i e. NN )
14 13 adantl 
 |-  ( ( N e. NN /\ i e. ( 1 ... N ) ) -> i e. NN )
15 14 nnrecred 
 |-  ( ( N e. NN /\ i e. ( 1 ... N ) ) -> ( 1 / i ) e. RR )
16 2 15 fsumrecl 
 |-  ( N e. NN -> sum_ i e. ( 1 ... N ) ( 1 / i ) e. RR )
17 16 resqcld 
 |-  ( N e. NN -> ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) e. RR )
18 nnrp 
 |-  ( N e. NN -> N e. RR+ )
19 18 relogcld 
 |-  ( N e. NN -> ( log ` N ) e. RR )
20 peano2re 
 |-  ( ( log ` N ) e. RR -> ( ( log ` N ) + 1 ) e. RR )
21 19 20 syl 
 |-  ( N e. NN -> ( ( log ` N ) + 1 ) e. RR )
22 21 resqcld 
 |-  ( N e. NN -> ( ( ( log ` N ) + 1 ) ^ 2 ) e. RR )
23 10 recnd 
 |-  ( N e. NN -> sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) e. CC )
24 23 2timesd 
 |-  ( N e. NN -> ( 2 x. sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) ) = ( sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) + sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) ) )
25 fzfid 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( 1 ... n ) e. Fin )
26 elfznn 
 |-  ( i e. ( 1 ... n ) -> i e. NN )
27 26 adantl 
 |-  ( ( ( N e. NN /\ n e. ( 1 ... N ) ) /\ i e. ( 1 ... n ) ) -> i e. NN )
28 27 nnrecred 
 |-  ( ( ( N e. NN /\ n e. ( 1 ... N ) ) /\ i e. ( 1 ... n ) ) -> ( 1 / i ) e. RR )
29 25 28 fsumrecl 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> sum_ i e. ( 1 ... n ) ( 1 / i ) e. RR )
30 29 6 nndivred 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) e. RR )
31 2 30 fsumrecl 
 |-  ( N e. NN -> sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) e. RR )
32 fzfid 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( 1 ... ( n - 1 ) ) e. Fin )
33 elfznn 
 |-  ( i e. ( 1 ... ( n - 1 ) ) -> i e. NN )
34 33 adantl 
 |-  ( ( ( N e. NN /\ n e. ( 1 ... N ) ) /\ i e. ( 1 ... ( n - 1 ) ) ) -> i e. NN )
35 34 nnrecred 
 |-  ( ( ( N e. NN /\ n e. ( 1 ... N ) ) /\ i e. ( 1 ... ( n - 1 ) ) ) -> ( 1 / i ) e. RR )
36 32 35 fsumrecl 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) e. RR )
37 36 6 nndivred 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) e. RR )
38 2 37 fsumrecl 
 |-  ( N e. NN -> sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) e. RR )
39 6 nncnd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> n e. CC )
40 ax-1cn 
 |-  1 e. CC
41 npcan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) + 1 ) = n )
42 39 40 41 sylancl 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( ( n - 1 ) + 1 ) = n )
43 42 fveq2d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( log ` ( ( n - 1 ) + 1 ) ) = ( log ` n ) )
44 43 oveq2d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` ( ( n - 1 ) + 1 ) ) ) = ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` n ) ) )
45 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
46 harmonicbnd3 
 |-  ( ( n - 1 ) e. NN0 -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` ( ( n - 1 ) + 1 ) ) ) e. ( 0 [,] gamma ) )
47 6 45 46 3syl 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` ( ( n - 1 ) + 1 ) ) ) e. ( 0 [,] gamma ) )
48 44 47 eqeltrrd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` n ) ) e. ( 0 [,] gamma ) )
49 0re 
 |-  0 e. RR
50 emre 
 |-  gamma e. RR
51 49 50 elicc2i 
 |-  ( ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` n ) ) e. ( 0 [,] gamma ) <-> ( ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` n ) ) e. RR /\ 0 <_ ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` n ) ) /\ ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` n ) ) <_ gamma ) )
52 51 simp2bi 
 |-  ( ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` n ) ) e. ( 0 [,] gamma ) -> 0 <_ ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` n ) ) )
53 48 52 syl 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> 0 <_ ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` n ) ) )
54 36 8 subge0d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( 0 <_ ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) - ( log ` n ) ) <-> ( log ` n ) <_ sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) )
55 53 54 mpbid 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( log ` n ) <_ sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) )
56 8 36 7 55 lediv1dd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( ( log ` n ) / n ) <_ ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) )
57 27 nnrpd 
 |-  ( ( ( N e. NN /\ n e. ( 1 ... N ) ) /\ i e. ( 1 ... n ) ) -> i e. RR+ )
58 57 rpreccld 
 |-  ( ( ( N e. NN /\ n e. ( 1 ... N ) ) /\ i e. ( 1 ... n ) ) -> ( 1 / i ) e. RR+ )
59 58 rpge0d 
 |-  ( ( ( N e. NN /\ n e. ( 1 ... N ) ) /\ i e. ( 1 ... n ) ) -> 0 <_ ( 1 / i ) )
60 elfzelz 
 |-  ( n e. ( 1 ... N ) -> n e. ZZ )
61 60 adantl 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> n e. ZZ )
62 peano2zm 
 |-  ( n e. ZZ -> ( n - 1 ) e. ZZ )
63 61 62 syl 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( n - 1 ) e. ZZ )
64 6 nnred 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> n e. RR )
65 64 lem1d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( n - 1 ) <_ n )
66 eluz2 
 |-  ( n e. ( ZZ>= ` ( n - 1 ) ) <-> ( ( n - 1 ) e. ZZ /\ n e. ZZ /\ ( n - 1 ) <_ n ) )
67 63 61 65 66 syl3anbrc 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> n e. ( ZZ>= ` ( n - 1 ) ) )
68 fzss2 
 |-  ( n e. ( ZZ>= ` ( n - 1 ) ) -> ( 1 ... ( n - 1 ) ) C_ ( 1 ... n ) )
69 67 68 syl 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( 1 ... ( n - 1 ) ) C_ ( 1 ... n ) )
70 25 28 59 69 fsumless 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) <_ sum_ i e. ( 1 ... n ) ( 1 / i ) )
71 6 nngt0d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> 0 < n )
72 lediv1 
 |-  ( ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) e. RR /\ sum_ i e. ( 1 ... n ) ( 1 / i ) e. RR /\ ( n e. RR /\ 0 < n ) ) -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) <_ sum_ i e. ( 1 ... n ) ( 1 / i ) <-> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) <_ ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) ) )
73 36 29 64 71 72 syl112anc 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) <_ sum_ i e. ( 1 ... n ) ( 1 / i ) <-> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) <_ ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) ) )
74 70 73 mpbid 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) <_ ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) )
75 9 37 30 56 74 letrd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( ( log ` n ) / n ) <_ ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) )
76 2 9 30 75 fsumle 
 |-  ( N e. NN -> sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) <_ sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) )
77 2 9 37 56 fsumle 
 |-  ( N e. NN -> sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) <_ sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) )
78 10 10 31 38 76 77 le2addd 
 |-  ( N e. NN -> ( sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) + sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) ) <_ ( sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) + sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) ) )
79 oveq1 
 |-  ( m = n -> ( m - 1 ) = ( n - 1 ) )
80 79 oveq2d 
 |-  ( m = n -> ( 1 ... ( m - 1 ) ) = ( 1 ... ( n - 1 ) ) )
81 80 sumeq1d 
 |-  ( m = n -> sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) )
82 81 81 jca 
 |-  ( m = n -> ( sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) /\ sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) )
83 oveq1 
 |-  ( m = ( n + 1 ) -> ( m - 1 ) = ( ( n + 1 ) - 1 ) )
84 83 oveq2d 
 |-  ( m = ( n + 1 ) -> ( 1 ... ( m - 1 ) ) = ( 1 ... ( ( n + 1 ) - 1 ) ) )
85 84 sumeq1d 
 |-  ( m = ( n + 1 ) -> sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) )
86 85 85 jca 
 |-  ( m = ( n + 1 ) -> ( sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) /\ sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) ) )
87 oveq1 
 |-  ( m = 1 -> ( m - 1 ) = ( 1 - 1 ) )
88 1m1e0 
 |-  ( 1 - 1 ) = 0
89 87 88 eqtrdi 
 |-  ( m = 1 -> ( m - 1 ) = 0 )
90 89 oveq2d 
 |-  ( m = 1 -> ( 1 ... ( m - 1 ) ) = ( 1 ... 0 ) )
91 fz10 
 |-  ( 1 ... 0 ) = (/)
92 90 91 eqtrdi 
 |-  ( m = 1 -> ( 1 ... ( m - 1 ) ) = (/) )
93 92 sumeq1d 
 |-  ( m = 1 -> sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = sum_ i e. (/) ( 1 / i ) )
94 sum0 
 |-  sum_ i e. (/) ( 1 / i ) = 0
95 93 94 eqtrdi 
 |-  ( m = 1 -> sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = 0 )
96 95 95 jca 
 |-  ( m = 1 -> ( sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = 0 /\ sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = 0 ) )
97 oveq1 
 |-  ( m = ( N + 1 ) -> ( m - 1 ) = ( ( N + 1 ) - 1 ) )
98 97 oveq2d 
 |-  ( m = ( N + 1 ) -> ( 1 ... ( m - 1 ) ) = ( 1 ... ( ( N + 1 ) - 1 ) ) )
99 98 sumeq1d 
 |-  ( m = ( N + 1 ) -> sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) )
100 99 99 jca 
 |-  ( m = ( N + 1 ) -> ( sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) /\ sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) ) )
101 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
102 101 5 eleqtrdi 
 |-  ( N e. NN -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
103 fzfid 
 |-  ( ( N e. NN /\ m e. ( 1 ... ( N + 1 ) ) ) -> ( 1 ... ( m - 1 ) ) e. Fin )
104 elfznn 
 |-  ( i e. ( 1 ... ( m - 1 ) ) -> i e. NN )
105 104 adantl 
 |-  ( ( ( N e. NN /\ m e. ( 1 ... ( N + 1 ) ) ) /\ i e. ( 1 ... ( m - 1 ) ) ) -> i e. NN )
106 105 nnrecred 
 |-  ( ( ( N e. NN /\ m e. ( 1 ... ( N + 1 ) ) ) /\ i e. ( 1 ... ( m - 1 ) ) ) -> ( 1 / i ) e. RR )
107 103 106 fsumrecl 
 |-  ( ( N e. NN /\ m e. ( 1 ... ( N + 1 ) ) ) -> sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) e. RR )
108 107 recnd 
 |-  ( ( N e. NN /\ m e. ( 1 ... ( N + 1 ) ) ) -> sum_ i e. ( 1 ... ( m - 1 ) ) ( 1 / i ) e. CC )
109 82 86 96 100 102 108 108 fsumparts 
 |-  ( N e. NN -> sum_ n e. ( 1 ..^ ( N + 1 ) ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) x. ( sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) - sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) ) = ( ( ( sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) x. sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) ) - ( 0 x. 0 ) ) - sum_ n e. ( 1 ..^ ( N + 1 ) ) ( ( sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) - sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) x. sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) ) ) )
110 nnz 
 |-  ( N e. NN -> N e. ZZ )
111 fzval3 
 |-  ( N e. ZZ -> ( 1 ... N ) = ( 1 ..^ ( N + 1 ) ) )
112 110 111 syl 
 |-  ( N e. NN -> ( 1 ... N ) = ( 1 ..^ ( N + 1 ) ) )
113 112 eqcomd 
 |-  ( N e. NN -> ( 1 ..^ ( N + 1 ) ) = ( 1 ... N ) )
114 36 recnd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) e. CC )
115 6 nnrecred 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( 1 / n ) e. RR )
116 115 recnd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( 1 / n ) e. CC )
117 pncan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
118 39 40 117 sylancl 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( ( n + 1 ) - 1 ) = n )
119 118 oveq2d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( 1 ... ( ( n + 1 ) - 1 ) ) = ( 1 ... n ) )
120 119 sumeq1d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... n ) ( 1 / i ) )
121 28 recnd 
 |-  ( ( ( N e. NN /\ n e. ( 1 ... N ) ) /\ i e. ( 1 ... n ) ) -> ( 1 / i ) e. CC )
122 oveq2 
 |-  ( i = n -> ( 1 / i ) = ( 1 / n ) )
123 4 121 122 fsumm1 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> sum_ i e. ( 1 ... n ) ( 1 / i ) = ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) + ( 1 / n ) ) )
124 120 123 eqtrd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) = ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) + ( 1 / n ) ) )
125 114 116 124 mvrladdd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) - sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) = ( 1 / n ) )
126 125 oveq2d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) x. ( sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) - sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) ) = ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) x. ( 1 / n ) ) )
127 6 nnne0d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> n =/= 0 )
128 114 39 127 divrecd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) = ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) x. ( 1 / n ) ) )
129 126 128 eqtr4d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) x. ( sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) - sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) ) = ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) )
130 113 129 sumeq12rdv 
 |-  ( N e. NN -> sum_ n e. ( 1 ..^ ( N + 1 ) ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) x. ( sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) - sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) ) = sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) )
131 nncn 
 |-  ( N e. NN -> N e. CC )
132 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
133 131 40 132 sylancl 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
134 133 oveq2d 
 |-  ( N e. NN -> ( 1 ... ( ( N + 1 ) - 1 ) ) = ( 1 ... N ) )
135 134 sumeq1d 
 |-  ( N e. NN -> sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) = sum_ i e. ( 1 ... N ) ( 1 / i ) )
136 135 135 oveq12d 
 |-  ( N e. NN -> ( sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) x. sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) ) = ( sum_ i e. ( 1 ... N ) ( 1 / i ) x. sum_ i e. ( 1 ... N ) ( 1 / i ) ) )
137 16 recnd 
 |-  ( N e. NN -> sum_ i e. ( 1 ... N ) ( 1 / i ) e. CC )
138 137 sqvald 
 |-  ( N e. NN -> ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) = ( sum_ i e. ( 1 ... N ) ( 1 / i ) x. sum_ i e. ( 1 ... N ) ( 1 / i ) ) )
139 136 138 eqtr4d 
 |-  ( N e. NN -> ( sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) x. sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) ) = ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) )
140 0cn 
 |-  0 e. CC
141 140 mul01i 
 |-  ( 0 x. 0 ) = 0
142 141 a1i 
 |-  ( N e. NN -> ( 0 x. 0 ) = 0 )
143 139 142 oveq12d 
 |-  ( N e. NN -> ( ( sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) x. sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) ) - ( 0 x. 0 ) ) = ( ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) - 0 ) )
144 137 sqcld 
 |-  ( N e. NN -> ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) e. CC )
145 144 subid1d 
 |-  ( N e. NN -> ( ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) - 0 ) = ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) )
146 143 145 eqtrd 
 |-  ( N e. NN -> ( ( sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) x. sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) ) - ( 0 x. 0 ) ) = ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) )
147 125 120 oveq12d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( ( sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) - sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) x. sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) ) = ( ( 1 / n ) x. sum_ i e. ( 1 ... n ) ( 1 / i ) ) )
148 29 recnd 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> sum_ i e. ( 1 ... n ) ( 1 / i ) e. CC )
149 148 39 127 divrec2d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) = ( ( 1 / n ) x. sum_ i e. ( 1 ... n ) ( 1 / i ) ) )
150 147 149 eqtr4d 
 |-  ( ( N e. NN /\ n e. ( 1 ... N ) ) -> ( ( sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) - sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) x. sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) ) = ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) )
151 113 150 sumeq12rdv 
 |-  ( N e. NN -> sum_ n e. ( 1 ..^ ( N + 1 ) ) ( ( sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) - sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) x. sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) ) = sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) )
152 146 151 oveq12d 
 |-  ( N e. NN -> ( ( ( sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) x. sum_ i e. ( 1 ... ( ( N + 1 ) - 1 ) ) ( 1 / i ) ) - ( 0 x. 0 ) ) - sum_ n e. ( 1 ..^ ( N + 1 ) ) ( ( sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) - sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) ) x. sum_ i e. ( 1 ... ( ( n + 1 ) - 1 ) ) ( 1 / i ) ) ) = ( ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) - sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) ) )
153 109 130 152 3eqtr3rd 
 |-  ( N e. NN -> ( ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) - sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) ) = sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) )
154 31 recnd 
 |-  ( N e. NN -> sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) e. CC )
155 38 recnd 
 |-  ( N e. NN -> sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) e. CC )
156 144 154 155 subaddd 
 |-  ( N e. NN -> ( ( ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) - sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) ) = sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) <-> ( sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) + sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) ) = ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) ) )
157 153 156 mpbid 
 |-  ( N e. NN -> ( sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... n ) ( 1 / i ) / n ) + sum_ n e. ( 1 ... N ) ( sum_ i e. ( 1 ... ( n - 1 ) ) ( 1 / i ) / n ) ) = ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) )
158 78 157 breqtrd 
 |-  ( N e. NN -> ( sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) + sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) ) <_ ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) )
159 24 158 eqbrtrd 
 |-  ( N e. NN -> ( 2 x. sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) ) <_ ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) )
160 flid 
 |-  ( N e. ZZ -> ( |_ ` N ) = N )
161 110 160 syl 
 |-  ( N e. NN -> ( |_ ` N ) = N )
162 161 oveq2d 
 |-  ( N e. NN -> ( 1 ... ( |_ ` N ) ) = ( 1 ... N ) )
163 162 sumeq1d 
 |-  ( N e. NN -> sum_ i e. ( 1 ... ( |_ ` N ) ) ( 1 / i ) = sum_ i e. ( 1 ... N ) ( 1 / i ) )
164 nnre 
 |-  ( N e. NN -> N e. RR )
165 nnge1 
 |-  ( N e. NN -> 1 <_ N )
166 harmonicubnd 
 |-  ( ( N e. RR /\ 1 <_ N ) -> sum_ i e. ( 1 ... ( |_ ` N ) ) ( 1 / i ) <_ ( ( log ` N ) + 1 ) )
167 164 165 166 syl2anc 
 |-  ( N e. NN -> sum_ i e. ( 1 ... ( |_ ` N ) ) ( 1 / i ) <_ ( ( log ` N ) + 1 ) )
168 163 167 eqbrtrrd 
 |-  ( N e. NN -> sum_ i e. ( 1 ... N ) ( 1 / i ) <_ ( ( log ` N ) + 1 ) )
169 14 nnrpd 
 |-  ( ( N e. NN /\ i e. ( 1 ... N ) ) -> i e. RR+ )
170 169 rpreccld 
 |-  ( ( N e. NN /\ i e. ( 1 ... N ) ) -> ( 1 / i ) e. RR+ )
171 170 rpge0d 
 |-  ( ( N e. NN /\ i e. ( 1 ... N ) ) -> 0 <_ ( 1 / i ) )
172 2 15 171 fsumge0 
 |-  ( N e. NN -> 0 <_ sum_ i e. ( 1 ... N ) ( 1 / i ) )
173 49 a1i 
 |-  ( N e. NN -> 0 e. RR )
174 log1 
 |-  ( log ` 1 ) = 0
175 1rp 
 |-  1 e. RR+
176 logleb 
 |-  ( ( 1 e. RR+ /\ N e. RR+ ) -> ( 1 <_ N <-> ( log ` 1 ) <_ ( log ` N ) ) )
177 175 18 176 sylancr 
 |-  ( N e. NN -> ( 1 <_ N <-> ( log ` 1 ) <_ ( log ` N ) ) )
178 165 177 mpbid 
 |-  ( N e. NN -> ( log ` 1 ) <_ ( log ` N ) )
179 174 178 eqbrtrrid 
 |-  ( N e. NN -> 0 <_ ( log ` N ) )
180 19 lep1d 
 |-  ( N e. NN -> ( log ` N ) <_ ( ( log ` N ) + 1 ) )
181 173 19 21 179 180 letrd 
 |-  ( N e. NN -> 0 <_ ( ( log ` N ) + 1 ) )
182 16 21 172 181 le2sqd 
 |-  ( N e. NN -> ( sum_ i e. ( 1 ... N ) ( 1 / i ) <_ ( ( log ` N ) + 1 ) <-> ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) <_ ( ( ( log ` N ) + 1 ) ^ 2 ) ) )
183 168 182 mpbid 
 |-  ( N e. NN -> ( sum_ i e. ( 1 ... N ) ( 1 / i ) ^ 2 ) <_ ( ( ( log ` N ) + 1 ) ^ 2 ) )
184 12 17 22 159 183 letrd 
 |-  ( N e. NN -> ( 2 x. sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` N ) + 1 ) ^ 2 ) )
185 1 a1i 
 |-  ( N e. NN -> 2 e. RR )
186 2pos 
 |-  0 < 2
187 186 a1i 
 |-  ( N e. NN -> 0 < 2 )
188 lemuldiv2 
 |-  ( ( sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) e. RR /\ ( ( ( log ` N ) + 1 ) ^ 2 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` N ) + 1 ) ^ 2 ) <-> sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` N ) + 1 ) ^ 2 ) / 2 ) ) )
189 10 22 185 187 188 syl112anc 
 |-  ( N e. NN -> ( ( 2 x. sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) ) <_ ( ( ( log ` N ) + 1 ) ^ 2 ) <-> sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` N ) + 1 ) ^ 2 ) / 2 ) ) )
190 184 189 mpbid 
 |-  ( N e. NN -> sum_ n e. ( 1 ... N ) ( ( log ` n ) / n ) <_ ( ( ( ( log ` N ) + 1 ) ^ 2 ) / 2 ) )