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 mulid2d
 |-  ( ( 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 )