This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rplogsumlem1

Description: Lemma for rplogsum . (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Assertion rplogsumlem1 
|- ( A e. NN -> sum_ n e. ( 2 ... A ) ( ( log ` n ) / ( n x. ( n - 1 ) ) ) <_ 2 )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( A e. NN -> ( 2 ... A ) e. Fin )
2 elfzuz 
 |-  ( n e. ( 2 ... A ) -> n e. ( ZZ>= ` 2 ) )
3 eluz2nn 
 |-  ( n e. ( ZZ>= ` 2 ) -> n e. NN )
4 2 3 syl 
 |-  ( n e. ( 2 ... A ) -> n e. NN )
5 4 adantl 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> n e. NN )
6 5 nnrpd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> n e. RR+ )
7 6 relogcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( log ` n ) e. RR )
8 2 adantl 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> n e. ( ZZ>= ` 2 ) )
9 uz2m1nn 
 |-  ( n e. ( ZZ>= ` 2 ) -> ( n - 1 ) e. NN )
10 8 9 syl 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( n - 1 ) e. NN )
11 5 10 nnmulcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( n x. ( n - 1 ) ) e. NN )
12 7 11 nndivred 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( log ` n ) / ( n x. ( n - 1 ) ) ) e. RR )
13 1 12 fsumrecl 
 |-  ( A e. NN -> sum_ n e. ( 2 ... A ) ( ( log ` n ) / ( n x. ( n - 1 ) ) ) e. RR )
14 2re 
 |-  2 e. RR
15 10 nnrpd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( n - 1 ) e. RR+ )
16 15 rpsqrtcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( sqrt ` ( n - 1 ) ) e. RR+ )
17 rerpdivcl 
 |-  ( ( 2 e. RR /\ ( sqrt ` ( n - 1 ) ) e. RR+ ) -> ( 2 / ( sqrt ` ( n - 1 ) ) ) e. RR )
18 14 16 17 sylancr 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( 2 / ( sqrt ` ( n - 1 ) ) ) e. RR )
19 6 rpsqrtcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( sqrt ` n ) e. RR+ )
20 rerpdivcl 
 |-  ( ( 2 e. RR /\ ( sqrt ` n ) e. RR+ ) -> ( 2 / ( sqrt ` n ) ) e. RR )
21 14 19 20 sylancr 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( 2 / ( sqrt ` n ) ) e. RR )
22 18 21 resubcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) e. RR )
23 1 22 fsumrecl 
 |-  ( A e. NN -> sum_ n e. ( 2 ... A ) ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) e. RR )
24 14 a1i 
 |-  ( A e. NN -> 2 e. RR )
25 16 rpred 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( sqrt ` ( n - 1 ) ) e. RR )
26 5 nnred 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> n e. RR )
27 peano2rem 
 |-  ( n e. RR -> ( n - 1 ) e. RR )
28 26 27 syl 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( n - 1 ) e. RR )
29 26 28 remulcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( n x. ( n - 1 ) ) e. RR )
30 29 22 remulcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( n x. ( n - 1 ) ) x. ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) ) e. RR )
31 5 nncnd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> n e. CC )
32 ax-1cn 
 |-  1 e. CC
33 npcan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) + 1 ) = n )
34 31 32 33 sylancl 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( n - 1 ) + 1 ) = n )
35 34 fveq2d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( log ` ( ( n - 1 ) + 1 ) ) = ( log ` n ) )
36 15 rpge0d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> 0 <_ ( n - 1 ) )
37 loglesqrt 
 |-  ( ( ( n - 1 ) e. RR /\ 0 <_ ( n - 1 ) ) -> ( log ` ( ( n - 1 ) + 1 ) ) <_ ( sqrt ` ( n - 1 ) ) )
38 28 36 37 syl2anc 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( log ` ( ( n - 1 ) + 1 ) ) <_ ( sqrt ` ( n - 1 ) ) )
39 35 38 eqbrtrrd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( log ` n ) <_ ( sqrt ` ( n - 1 ) ) )
40 19 rpred 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( sqrt ` n ) e. RR )
41 40 25 readdcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) + ( sqrt ` ( n - 1 ) ) ) e. RR )
42 remulcl 
 |-  ( ( ( sqrt ` n ) e. RR /\ 2 e. RR ) -> ( ( sqrt ` n ) x. 2 ) e. RR )
43 40 14 42 sylancl 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) x. 2 ) e. RR )
44 40 25 resubcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) e. RR )
45 26 lem1d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( n - 1 ) <_ n )
46 6 rpge0d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> 0 <_ n )
47 28 36 26 46 sqrtled 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( n - 1 ) <_ n <-> ( sqrt ` ( n - 1 ) ) <_ ( sqrt ` n ) ) )
48 45 47 mpbid 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( sqrt ` ( n - 1 ) ) <_ ( sqrt ` n ) )
49 40 25 subge0d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( 0 <_ ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) <-> ( sqrt ` ( n - 1 ) ) <_ ( sqrt ` n ) ) )
50 48 49 mpbird 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> 0 <_ ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) )
51 25 40 40 48 leadd2dd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) + ( sqrt ` ( n - 1 ) ) ) <_ ( ( sqrt ` n ) + ( sqrt ` n ) ) )
52 19 rpcnd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( sqrt ` n ) e. CC )
53 52 times2d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) x. 2 ) = ( ( sqrt ` n ) + ( sqrt ` n ) ) )
54 51 53 breqtrrd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) + ( sqrt ` ( n - 1 ) ) ) <_ ( ( sqrt ` n ) x. 2 ) )
55 41 43 44 50 54 lemul1ad 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( sqrt ` n ) + ( sqrt ` ( n - 1 ) ) ) x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) <_ ( ( ( sqrt ` n ) x. 2 ) x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) )
56 31 sqsqrtd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) ^ 2 ) = n )
57 subcl 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( n - 1 ) e. CC )
58 31 32 57 sylancl 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( n - 1 ) e. CC )
59 58 sqsqrtd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` ( n - 1 ) ) ^ 2 ) = ( n - 1 ) )
60 56 59 oveq12d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( sqrt ` n ) ^ 2 ) - ( ( sqrt ` ( n - 1 ) ) ^ 2 ) ) = ( n - ( n - 1 ) ) )
61 16 rpcnd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( sqrt ` ( n - 1 ) ) e. CC )
62 subsq 
 |-  ( ( ( sqrt ` n ) e. CC /\ ( sqrt ` ( n - 1 ) ) e. CC ) -> ( ( ( sqrt ` n ) ^ 2 ) - ( ( sqrt ` ( n - 1 ) ) ^ 2 ) ) = ( ( ( sqrt ` n ) + ( sqrt ` ( n - 1 ) ) ) x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) )
63 52 61 62 syl2anc 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( sqrt ` n ) ^ 2 ) - ( ( sqrt ` ( n - 1 ) ) ^ 2 ) ) = ( ( ( sqrt ` n ) + ( sqrt ` ( n - 1 ) ) ) x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) )
64 nncan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( n - ( n - 1 ) ) = 1 )
65 31 32 64 sylancl 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( n - ( n - 1 ) ) = 1 )
66 60 63 65 3eqtr3d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( sqrt ` n ) + ( sqrt ` ( n - 1 ) ) ) x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) = 1 )
67 2cn 
 |-  2 e. CC
68 67 a1i 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> 2 e. CC )
69 44 recnd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) e. CC )
70 52 68 69 mulassd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( sqrt ` n ) x. 2 ) x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) = ( ( sqrt ` n ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) )
71 55 66 70 3brtr3d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> 1 <_ ( ( sqrt ` n ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) )
72 1red 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> 1 e. RR )
73 remulcl 
 |-  ( ( 2 e. RR /\ ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) e. RR ) -> ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) e. RR )
74 14 44 73 sylancr 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) e. RR )
75 40 74 remulcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) e. RR )
76 72 75 16 lemul1d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( 1 <_ ( ( sqrt ` n ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) <-> ( 1 x. ( sqrt ` ( n - 1 ) ) ) <_ ( ( ( sqrt ` n ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) x. ( sqrt ` ( n - 1 ) ) ) ) )
77 71 76 mpbid 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( 1 x. ( sqrt ` ( n - 1 ) ) ) <_ ( ( ( sqrt ` n ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) x. ( sqrt ` ( n - 1 ) ) ) )
78 61 mullidd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( 1 x. ( sqrt ` ( n - 1 ) ) ) = ( sqrt ` ( n - 1 ) ) )
79 74 recnd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) e. CC )
80 52 79 61 mul32d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( sqrt ` n ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) x. ( sqrt ` ( n - 1 ) ) ) = ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) )
81 77 78 80 3brtr3d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( sqrt ` ( n - 1 ) ) <_ ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) )
82 remsqsqrt 
 |-  ( ( n e. RR /\ 0 <_ n ) -> ( ( sqrt ` n ) x. ( sqrt ` n ) ) = n )
83 26 46 82 syl2anc 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) x. ( sqrt ` n ) ) = n )
84 remsqsqrt 
 |-  ( ( ( n - 1 ) e. RR /\ 0 <_ ( n - 1 ) ) -> ( ( sqrt ` ( n - 1 ) ) x. ( sqrt ` ( n - 1 ) ) ) = ( n - 1 ) )
85 28 36 84 syl2anc 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` ( n - 1 ) ) x. ( sqrt ` ( n - 1 ) ) ) = ( n - 1 ) )
86 83 85 oveq12d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( sqrt ` n ) x. ( sqrt ` n ) ) x. ( ( sqrt ` ( n - 1 ) ) x. ( sqrt ` ( n - 1 ) ) ) ) = ( n x. ( n - 1 ) ) )
87 52 52 61 61 mul4d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( sqrt ` n ) x. ( sqrt ` n ) ) x. ( ( sqrt ` ( n - 1 ) ) x. ( sqrt ` ( n - 1 ) ) ) ) = ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) )
88 86 87 eqtr3d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( n x. ( n - 1 ) ) = ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) )
89 16 rpcnne0d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` ( n - 1 ) ) e. CC /\ ( sqrt ` ( n - 1 ) ) =/= 0 ) )
90 19 rpcnne0d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) e. CC /\ ( sqrt ` n ) =/= 0 ) )
91 divsubdiv 
 |-  ( ( ( 2 e. CC /\ 2 e. CC ) /\ ( ( ( sqrt ` ( n - 1 ) ) e. CC /\ ( sqrt ` ( n - 1 ) ) =/= 0 ) /\ ( ( sqrt ` n ) e. CC /\ ( sqrt ` n ) =/= 0 ) ) ) -> ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) = ( ( ( 2 x. ( sqrt ` n ) ) - ( 2 x. ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` ( n - 1 ) ) x. ( sqrt ` n ) ) ) )
92 68 68 89 90 91 syl22anc 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) = ( ( ( 2 x. ( sqrt ` n ) ) - ( 2 x. ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` ( n - 1 ) ) x. ( sqrt ` n ) ) ) )
93 68 52 61 subdid 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) = ( ( 2 x. ( sqrt ` n ) ) - ( 2 x. ( sqrt ` ( n - 1 ) ) ) ) )
94 52 61 mulcomd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) = ( ( sqrt ` ( n - 1 ) ) x. ( sqrt ` n ) ) )
95 93 94 oveq12d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) = ( ( ( 2 x. ( sqrt ` n ) ) - ( 2 x. ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` ( n - 1 ) ) x. ( sqrt ` n ) ) ) )
96 92 95 eqtr4d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) = ( ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) )
97 88 96 oveq12d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( n x. ( n - 1 ) ) x. ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) ) = ( ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) x. ( ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) ) )
98 52 61 mulcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) e. CC )
99 19 16 rpmulcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) e. RR+ )
100 74 99 rerpdivcld 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) e. RR )
101 100 recnd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) e. CC )
102 98 98 101 mulassd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) x. ( ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) ) = ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) ) ) )
103 99 rpne0d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) =/= 0 )
104 79 98 103 divcan2d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) ) = ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) )
105 104 oveq2d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) / ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) ) ) ) = ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) )
106 97 102 105 3eqtrd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( n x. ( n - 1 ) ) x. ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) ) = ( ( ( sqrt ` n ) x. ( sqrt ` ( n - 1 ) ) ) x. ( 2 x. ( ( sqrt ` n ) - ( sqrt ` ( n - 1 ) ) ) ) ) )
107 81 106 breqtrrd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( sqrt ` ( n - 1 ) ) <_ ( ( n x. ( n - 1 ) ) x. ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) ) )
108 7 25 30 39 107 letrd 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( log ` n ) <_ ( ( n x. ( n - 1 ) ) x. ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) ) )
109 11 nngt0d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> 0 < ( n x. ( n - 1 ) ) )
110 ledivmul 
 |-  ( ( ( log ` n ) e. RR /\ ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) e. RR /\ ( ( n x. ( n - 1 ) ) e. RR /\ 0 < ( n x. ( n - 1 ) ) ) ) -> ( ( ( log ` n ) / ( n x. ( n - 1 ) ) ) <_ ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) <-> ( log ` n ) <_ ( ( n x. ( n - 1 ) ) x. ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) ) ) )
111 7 22 29 109 110 syl112anc 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( ( log ` n ) / ( n x. ( n - 1 ) ) ) <_ ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) <-> ( log ` n ) <_ ( ( n x. ( n - 1 ) ) x. ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) ) ) )
112 108 111 mpbird 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( log ` n ) / ( n x. ( n - 1 ) ) ) <_ ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) )
113 1 12 22 112 fsumle 
 |-  ( A e. NN -> sum_ n e. ( 2 ... A ) ( ( log ` n ) / ( n x. ( n - 1 ) ) ) <_ sum_ n e. ( 2 ... A ) ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) )
114 fvoveq1 
 |-  ( k = n -> ( sqrt ` ( k - 1 ) ) = ( sqrt ` ( n - 1 ) ) )
115 114 oveq2d 
 |-  ( k = n -> ( 2 / ( sqrt ` ( k - 1 ) ) ) = ( 2 / ( sqrt ` ( n - 1 ) ) ) )
116 fvoveq1 
 |-  ( k = ( n + 1 ) -> ( sqrt ` ( k - 1 ) ) = ( sqrt ` ( ( n + 1 ) - 1 ) ) )
117 116 oveq2d 
 |-  ( k = ( n + 1 ) -> ( 2 / ( sqrt ` ( k - 1 ) ) ) = ( 2 / ( sqrt ` ( ( n + 1 ) - 1 ) ) ) )
118 oveq1 
 |-  ( k = 2 -> ( k - 1 ) = ( 2 - 1 ) )
119 2m1e1 
 |-  ( 2 - 1 ) = 1
120 118 119 eqtrdi 
 |-  ( k = 2 -> ( k - 1 ) = 1 )
121 120 fveq2d 
 |-  ( k = 2 -> ( sqrt ` ( k - 1 ) ) = ( sqrt ` 1 ) )
122 sqrt1 
 |-  ( sqrt ` 1 ) = 1
123 121 122 eqtrdi 
 |-  ( k = 2 -> ( sqrt ` ( k - 1 ) ) = 1 )
124 123 oveq2d 
 |-  ( k = 2 -> ( 2 / ( sqrt ` ( k - 1 ) ) ) = ( 2 / 1 ) )
125 67 div1i 
 |-  ( 2 / 1 ) = 2
126 124 125 eqtrdi 
 |-  ( k = 2 -> ( 2 / ( sqrt ` ( k - 1 ) ) ) = 2 )
127 fvoveq1 
 |-  ( k = ( A + 1 ) -> ( sqrt ` ( k - 1 ) ) = ( sqrt ` ( ( A + 1 ) - 1 ) ) )
128 127 oveq2d 
 |-  ( k = ( A + 1 ) -> ( 2 / ( sqrt ` ( k - 1 ) ) ) = ( 2 / ( sqrt ` ( ( A + 1 ) - 1 ) ) ) )
129 nnz 
 |-  ( A e. NN -> A e. ZZ )
130 eluzp1p1 
 |-  ( A e. ( ZZ>= ` 1 ) -> ( A + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
131 nnuz 
 |-  NN = ( ZZ>= ` 1 )
132 130 131 eleq2s 
 |-  ( A e. NN -> ( A + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
133 df-2 
 |-  2 = ( 1 + 1 )
134 133 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
135 132 134 eleqtrrdi 
 |-  ( A e. NN -> ( A + 1 ) e. ( ZZ>= ` 2 ) )
136 elfzuz 
 |-  ( k e. ( 2 ... ( A + 1 ) ) -> k e. ( ZZ>= ` 2 ) )
137 uz2m1nn 
 |-  ( k e. ( ZZ>= ` 2 ) -> ( k - 1 ) e. NN )
138 136 137 syl 
 |-  ( k e. ( 2 ... ( A + 1 ) ) -> ( k - 1 ) e. NN )
139 138 adantl 
 |-  ( ( A e. NN /\ k e. ( 2 ... ( A + 1 ) ) ) -> ( k - 1 ) e. NN )
140 139 nnrpd 
 |-  ( ( A e. NN /\ k e. ( 2 ... ( A + 1 ) ) ) -> ( k - 1 ) e. RR+ )
141 140 rpsqrtcld 
 |-  ( ( A e. NN /\ k e. ( 2 ... ( A + 1 ) ) ) -> ( sqrt ` ( k - 1 ) ) e. RR+ )
142 rerpdivcl 
 |-  ( ( 2 e. RR /\ ( sqrt ` ( k - 1 ) ) e. RR+ ) -> ( 2 / ( sqrt ` ( k - 1 ) ) ) e. RR )
143 14 141 142 sylancr 
 |-  ( ( A e. NN /\ k e. ( 2 ... ( A + 1 ) ) ) -> ( 2 / ( sqrt ` ( k - 1 ) ) ) e. RR )
144 143 recnd 
 |-  ( ( A e. NN /\ k e. ( 2 ... ( A + 1 ) ) ) -> ( 2 / ( sqrt ` ( k - 1 ) ) ) e. CC )
145 115 117 126 128 129 135 144 telfsum 
 |-  ( A e. NN -> sum_ n e. ( 2 ... A ) ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` ( ( n + 1 ) - 1 ) ) ) ) = ( 2 - ( 2 / ( sqrt ` ( ( A + 1 ) - 1 ) ) ) ) )
146 pncan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
147 31 32 146 sylancl 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( n + 1 ) - 1 ) = n )
148 147 fveq2d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( sqrt ` ( ( n + 1 ) - 1 ) ) = ( sqrt ` n ) )
149 148 oveq2d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( 2 / ( sqrt ` ( ( n + 1 ) - 1 ) ) ) = ( 2 / ( sqrt ` n ) ) )
150 149 oveq2d 
 |-  ( ( A e. NN /\ n e. ( 2 ... A ) ) -> ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` ( ( n + 1 ) - 1 ) ) ) ) = ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) )
151 150 sumeq2dv 
 |-  ( A e. NN -> sum_ n e. ( 2 ... A ) ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` ( ( n + 1 ) - 1 ) ) ) ) = sum_ n e. ( 2 ... A ) ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) )
152 nncn 
 |-  ( A e. NN -> A e. CC )
153 pncan 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) - 1 ) = A )
154 152 32 153 sylancl 
 |-  ( A e. NN -> ( ( A + 1 ) - 1 ) = A )
155 154 fveq2d 
 |-  ( A e. NN -> ( sqrt ` ( ( A + 1 ) - 1 ) ) = ( sqrt ` A ) )
156 155 oveq2d 
 |-  ( A e. NN -> ( 2 / ( sqrt ` ( ( A + 1 ) - 1 ) ) ) = ( 2 / ( sqrt ` A ) ) )
157 156 oveq2d 
 |-  ( A e. NN -> ( 2 - ( 2 / ( sqrt ` ( ( A + 1 ) - 1 ) ) ) ) = ( 2 - ( 2 / ( sqrt ` A ) ) ) )
158 145 151 157 3eqtr3d 
 |-  ( A e. NN -> sum_ n e. ( 2 ... A ) ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) = ( 2 - ( 2 / ( sqrt ` A ) ) ) )
159 2rp 
 |-  2 e. RR+
160 nnrp 
 |-  ( A e. NN -> A e. RR+ )
161 160 rpsqrtcld 
 |-  ( A e. NN -> ( sqrt ` A ) e. RR+ )
162 rpdivcl 
 |-  ( ( 2 e. RR+ /\ ( sqrt ` A ) e. RR+ ) -> ( 2 / ( sqrt ` A ) ) e. RR+ )
163 159 161 162 sylancr 
 |-  ( A e. NN -> ( 2 / ( sqrt ` A ) ) e. RR+ )
164 163 rpge0d 
 |-  ( A e. NN -> 0 <_ ( 2 / ( sqrt ` A ) ) )
165 163 rpred 
 |-  ( A e. NN -> ( 2 / ( sqrt ` A ) ) e. RR )
166 subge02 
 |-  ( ( 2 e. RR /\ ( 2 / ( sqrt ` A ) ) e. RR ) -> ( 0 <_ ( 2 / ( sqrt ` A ) ) <-> ( 2 - ( 2 / ( sqrt ` A ) ) ) <_ 2 ) )
167 14 165 166 sylancr 
 |-  ( A e. NN -> ( 0 <_ ( 2 / ( sqrt ` A ) ) <-> ( 2 - ( 2 / ( sqrt ` A ) ) ) <_ 2 ) )
168 164 167 mpbid 
 |-  ( A e. NN -> ( 2 - ( 2 / ( sqrt ` A ) ) ) <_ 2 )
169 158 168 eqbrtrd 
 |-  ( A e. NN -> sum_ n e. ( 2 ... A ) ( ( 2 / ( sqrt ` ( n - 1 ) ) ) - ( 2 / ( sqrt ` n ) ) ) <_ 2 )
170 13 23 24 113 169 letrd 
 |-  ( A e. NN -> sum_ n e. ( 2 ... A ) ( ( log ` n ) / ( n x. ( n - 1 ) ) ) <_ 2 )