Metamath Proof Explorer

Theorem pntrsumo1

Description: A bound on a sum over R . Equation 10.1.16 of Shapiro, p. 403. (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypothesis pntrval.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion pntrsumo1 
|- ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 pntrval.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 1re 
 |-  1 e. RR
3 elicopnf 
 |-  ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
4 2 3 ax-mp 
 |-  ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) )
5 4 simplbi 
 |-  ( x e. ( 1 [,) +oo ) -> x e. RR )
6 0red 
 |-  ( x e. ( 1 [,) +oo ) -> 0 e. RR )
7 1red 
 |-  ( x e. ( 1 [,) +oo ) -> 1 e. RR )
8 0lt1 
 |-  0 < 1
9 8 a1i 
 |-  ( x e. ( 1 [,) +oo ) -> 0 < 1 )
10 4 simprbi 
 |-  ( x e. ( 1 [,) +oo ) -> 1 <_ x )
11 6 7 5 9 10 ltletrd 
 |-  ( x e. ( 1 [,) +oo ) -> 0 < x )
12 5 11 elrpd 
 |-  ( x e. ( 1 [,) +oo ) -> x e. RR+ )
13 12 ssriv 
 |-  ( 1 [,) +oo ) C_ RR+
14 13 a1i 
 |-  ( T. -> ( 1 [,) +oo ) C_ RR+ )
15 rpssre 
 |-  RR+ C_ RR
16 14 15 sstrdi 
 |-  ( T. -> ( 1 [,) +oo ) C_ RR )
17 16 resmptd 
 |-  ( T. -> ( ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) |` ( 1 [,) +oo ) ) = ( x e. ( 1 [,) +oo ) |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
18 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
19 5 18 syl 
 |-  ( x e. ( 1 [,) +oo ) -> ( psi ` x ) e. RR )
20 peano2re 
 |-  ( ( psi ` x ) e. RR -> ( ( psi ` x ) + 1 ) e. RR )
21 19 20 syl 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( psi ` x ) + 1 ) e. RR )
22 12 rprege0d 
 |-  ( x e. ( 1 [,) +oo ) -> ( x e. RR /\ 0 <_ x ) )
23 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
24 22 23 syl 
 |-  ( x e. ( 1 [,) +oo ) -> ( |_ ` x ) e. NN0 )
25 nn0p1nn 
 |-  ( ( |_ ` x ) e. NN0 -> ( ( |_ ` x ) + 1 ) e. NN )
26 24 25 syl 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( |_ ` x ) + 1 ) e. NN )
27 21 26 nndivred 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) e. RR )
28 27 recnd 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) e. CC )
29 ax-1cn 
 |-  1 e. CC
30 subcl 
 |-  ( ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) e. CC )
31 28 29 30 sylancl 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) e. CC )
32 fzfid 
 |-  ( x e. RR -> ( 1 ... ( |_ ` x ) ) e. Fin )
33 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
34 33 adantl 
 |-  ( ( x e. RR /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
35 nnrp 
 |-  ( n e. NN -> n e. RR+ )
36 1 pntrf 
 |-  R : RR+ --> RR
37 36 ffvelcdmi 
 |-  ( n e. RR+ -> ( R ` n ) e. RR )
38 35 37 syl 
 |-  ( n e. NN -> ( R ` n ) e. RR )
39 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
40 nnmulcl 
 |-  ( ( n e. NN /\ ( n + 1 ) e. NN ) -> ( n x. ( n + 1 ) ) e. NN )
41 39 40 mpdan 
 |-  ( n e. NN -> ( n x. ( n + 1 ) ) e. NN )
42 38 41 nndivred 
 |-  ( n e. NN -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
43 34 42 syl 
 |-  ( ( x e. RR /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
44 32 43 fsumrecl 
 |-  ( x e. RR -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
45 44 recnd 
 |-  ( x e. RR -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
46 5 45 syl 
 |-  ( x e. ( 1 [,) +oo ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
47 oveq2 
 |-  ( m = n -> ( 1 / m ) = ( 1 / n ) )
48 fvoveq1 
 |-  ( m = n -> ( psi ` ( m - 1 ) ) = ( psi ` ( n - 1 ) ) )
49 oveq1 
 |-  ( m = n -> ( m - 1 ) = ( n - 1 ) )
50 48 49 oveq12d 
 |-  ( m = n -> ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) = ( ( psi ` ( n - 1 ) ) - ( n - 1 ) ) )
51 47 50 jca 
 |-  ( m = n -> ( ( 1 / m ) = ( 1 / n ) /\ ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) = ( ( psi ` ( n - 1 ) ) - ( n - 1 ) ) ) )
52 oveq2 
 |-  ( m = ( n + 1 ) -> ( 1 / m ) = ( 1 / ( n + 1 ) ) )
53 fvoveq1 
 |-  ( m = ( n + 1 ) -> ( psi ` ( m - 1 ) ) = ( psi ` ( ( n + 1 ) - 1 ) ) )
54 oveq1 
 |-  ( m = ( n + 1 ) -> ( m - 1 ) = ( ( n + 1 ) - 1 ) )
55 53 54 oveq12d 
 |-  ( m = ( n + 1 ) -> ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) = ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) )
56 52 55 jca 
 |-  ( m = ( n + 1 ) -> ( ( 1 / m ) = ( 1 / ( n + 1 ) ) /\ ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) = ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) ) )
57 oveq2 
 |-  ( m = 1 -> ( 1 / m ) = ( 1 / 1 ) )
58 1div1e1 
 |-  ( 1 / 1 ) = 1
59 57 58 eqtrdi 
 |-  ( m = 1 -> ( 1 / m ) = 1 )
60 oveq1 
 |-  ( m = 1 -> ( m - 1 ) = ( 1 - 1 ) )
61 1m1e0 
 |-  ( 1 - 1 ) = 0
62 60 61 eqtrdi 
 |-  ( m = 1 -> ( m - 1 ) = 0 )
63 62 fveq2d 
 |-  ( m = 1 -> ( psi ` ( m - 1 ) ) = ( psi ` 0 ) )
64 2pos 
 |-  0 < 2
65 0re 
 |-  0 e. RR
66 chpeq0 
 |-  ( 0 e. RR -> ( ( psi ` 0 ) = 0 <-> 0 < 2 ) )
67 65 66 ax-mp 
 |-  ( ( psi ` 0 ) = 0 <-> 0 < 2 )
68 64 67 mpbir 
 |-  ( psi ` 0 ) = 0
69 63 68 eqtrdi 
 |-  ( m = 1 -> ( psi ` ( m - 1 ) ) = 0 )
70 69 62 oveq12d 
 |-  ( m = 1 -> ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) = ( 0 - 0 ) )
71 0m0e0 
 |-  ( 0 - 0 ) = 0
72 70 71 eqtrdi 
 |-  ( m = 1 -> ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) = 0 )
73 59 72 jca 
 |-  ( m = 1 -> ( ( 1 / m ) = 1 /\ ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) = 0 ) )
74 oveq2 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( 1 / m ) = ( 1 / ( ( |_ ` x ) + 1 ) ) )
75 fvoveq1 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( psi ` ( m - 1 ) ) = ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
76 oveq1 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( m - 1 ) = ( ( ( |_ ` x ) + 1 ) - 1 ) )
77 75 76 oveq12d 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) = ( ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
78 74 77 jca 
 |-  ( m = ( ( |_ ` x ) + 1 ) -> ( ( 1 / m ) = ( 1 / ( ( |_ ` x ) + 1 ) ) /\ ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) = ( ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) )
79 nnuz 
 |-  NN = ( ZZ>= ` 1 )
80 26 79 eleqtrdi 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( |_ ` x ) + 1 ) e. ( ZZ>= ` 1 ) )
81 elfznn 
 |-  ( m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) -> m e. NN )
82 81 adantl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. NN )
83 82 nnrecred 
 |-  ( ( x e. ( 1 [,) +oo ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( 1 / m ) e. RR )
84 83 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( 1 / m ) e. CC )
85 82 nnred 
 |-  ( ( x e. ( 1 [,) +oo ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> m e. RR )
86 peano2rem 
 |-  ( m e. RR -> ( m - 1 ) e. RR )
87 85 86 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( m - 1 ) e. RR )
88 chpcl 
 |-  ( ( m - 1 ) e. RR -> ( psi ` ( m - 1 ) ) e. RR )
89 87 88 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( psi ` ( m - 1 ) ) e. RR )
90 89 87 resubcld 
 |-  ( ( x e. ( 1 [,) +oo ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) e. RR )
91 90 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ m e. ( 1 ... ( ( |_ ` x ) + 1 ) ) ) -> ( ( psi ` ( m - 1 ) ) - ( m - 1 ) ) e. CC )
92 51 56 73 78 80 84 91 fsumparts 
 |-  ( x e. ( 1 [,) +oo ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( 1 / n ) x. ( ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) - ( ( psi ` ( n - 1 ) ) - ( n - 1 ) ) ) ) = ( ( ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 1 x. 0 ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( 1 / ( n + 1 ) ) - ( 1 / n ) ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) ) ) )
93 5 flcld 
 |-  ( x e. ( 1 [,) +oo ) -> ( |_ ` x ) e. ZZ )
94 fzval3 
 |-  ( ( |_ ` x ) e. ZZ -> ( 1 ... ( |_ ` x ) ) = ( 1 ..^ ( ( |_ ` x ) + 1 ) ) )
95 93 94 syl 
 |-  ( x e. ( 1 [,) +oo ) -> ( 1 ... ( |_ ` x ) ) = ( 1 ..^ ( ( |_ ` x ) + 1 ) ) )
96 95 eqcomd 
 |-  ( x e. ( 1 [,) +oo ) -> ( 1 ..^ ( ( |_ ` x ) + 1 ) ) = ( 1 ... ( |_ ` x ) ) )
97 33 adantl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
98 97 nncnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
99 pncan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
100 98 29 99 sylancl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) = n )
101 97 nnred 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
102 100 101 eqeltrd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) e. RR )
103 chpcl 
 |-  ( ( ( n + 1 ) - 1 ) e. RR -> ( psi ` ( ( n + 1 ) - 1 ) ) e. RR )
104 102 103 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n + 1 ) - 1 ) ) e. RR )
105 104 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n + 1 ) - 1 ) ) e. CC )
106 102 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) e. CC )
107 peano2rem 
 |-  ( n e. RR -> ( n - 1 ) e. RR )
108 101 107 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
109 chpcl 
 |-  ( ( n - 1 ) e. RR -> ( psi ` ( n - 1 ) ) e. RR )
110 108 109 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( n - 1 ) ) e. RR )
111 110 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( n - 1 ) ) e. CC )
112 1cnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
113 98 112 subcld 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. CC )
114 105 106 111 113 sub4d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) - ( ( psi ` ( n - 1 ) ) - ( n - 1 ) ) ) = ( ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) - ( ( ( n + 1 ) - 1 ) - ( n - 1 ) ) ) )
115 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
116 97 115 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
117 116 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
118 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
119 97 118 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. NN0 )
120 chpp1 
 |-  ( ( n - 1 ) e. NN0 -> ( psi ` ( ( n - 1 ) + 1 ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` ( ( n - 1 ) + 1 ) ) ) )
121 119 120 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n - 1 ) + 1 ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` ( ( n - 1 ) + 1 ) ) ) )
122 npcan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) + 1 ) = n )
123 98 29 122 sylancl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n - 1 ) + 1 ) = n )
124 123 100 eqtr4d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n - 1 ) + 1 ) = ( ( n + 1 ) - 1 ) )
125 124 fveq2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n - 1 ) + 1 ) ) = ( psi ` ( ( n + 1 ) - 1 ) ) )
126 123 fveq2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` ( ( n - 1 ) + 1 ) ) = ( Lam ` n ) )
127 126 oveq2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( n - 1 ) ) + ( Lam ` ( ( n - 1 ) + 1 ) ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` n ) ) )
128 121 125 127 3eqtr3d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( psi ` ( ( n + 1 ) - 1 ) ) = ( ( psi ` ( n - 1 ) ) + ( Lam ` n ) ) )
129 111 117 128 mvrladdd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) = ( Lam ` n ) )
130 peano2cn 
 |-  ( n e. CC -> ( n + 1 ) e. CC )
131 98 130 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. CC )
132 131 98 112 nnncan2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) - 1 ) - ( n - 1 ) ) = ( ( n + 1 ) - n ) )
133 pncan2 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - n ) = 1 )
134 98 29 133 sylancl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - n ) = 1 )
135 132 134 eqtrd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) - 1 ) - ( n - 1 ) ) = 1 )
136 129 135 oveq12d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( psi ` ( n - 1 ) ) ) - ( ( ( n + 1 ) - 1 ) - ( n - 1 ) ) ) = ( ( Lam ` n ) - 1 ) )
137 114 136 eqtrd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) - ( ( psi ` ( n - 1 ) ) - ( n - 1 ) ) ) = ( ( Lam ` n ) - 1 ) )
138 137 oveq2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 / n ) x. ( ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) - ( ( psi ` ( n - 1 ) ) - ( n - 1 ) ) ) ) = ( ( 1 / n ) x. ( ( Lam ` n ) - 1 ) ) )
139 peano2rem 
 |-  ( ( Lam ` n ) e. RR -> ( ( Lam ` n ) - 1 ) e. RR )
140 116 139 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) - 1 ) e. RR )
141 140 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) - 1 ) e. CC )
142 97 nnne0d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
143 141 98 142 divrec2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) - 1 ) / n ) = ( ( 1 / n ) x. ( ( Lam ` n ) - 1 ) ) )
144 138 143 eqtr4d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 / n ) x. ( ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) - ( ( psi ` ( n - 1 ) ) - ( n - 1 ) ) ) ) = ( ( ( Lam ` n ) - 1 ) / n ) )
145 96 144 sumeq12rdv 
 |-  ( x e. ( 1 [,) +oo ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( 1 / n ) x. ( ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) - ( ( psi ` ( n - 1 ) ) - ( n - 1 ) ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) )
146 24 nn0cnd 
 |-  ( x e. ( 1 [,) +oo ) -> ( |_ ` x ) e. CC )
147 pncan 
 |-  ( ( ( |_ ` x ) e. CC /\ 1 e. CC ) -> ( ( ( |_ ` x ) + 1 ) - 1 ) = ( |_ ` x ) )
148 146 29 147 sylancl 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( |_ ` x ) + 1 ) - 1 ) = ( |_ ` x ) )
149 148 fveq2d 
 |-  ( x e. ( 1 [,) +oo ) -> ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( psi ` ( |_ ` x ) ) )
150 chpfl 
 |-  ( x e. RR -> ( psi ` ( |_ ` x ) ) = ( psi ` x ) )
151 5 150 syl 
 |-  ( x e. ( 1 [,) +oo ) -> ( psi ` ( |_ ` x ) ) = ( psi ` x ) )
152 149 151 eqtrd 
 |-  ( x e. ( 1 [,) +oo ) -> ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( psi ` x ) )
153 152 oveq1d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( ( psi ` x ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) )
154 19 recnd 
 |-  ( x e. ( 1 [,) +oo ) -> ( psi ` x ) e. CC )
155 26 nncnd 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( |_ ` x ) + 1 ) e. CC )
156 1cnd 
 |-  ( x e. ( 1 [,) +oo ) -> 1 e. CC )
157 154 155 156 subsub3d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( psi ` x ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( ( ( psi ` x ) + 1 ) - ( ( |_ ` x ) + 1 ) ) )
158 153 157 eqtrd 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) = ( ( ( psi ` x ) + 1 ) - ( ( |_ ` x ) + 1 ) ) )
159 158 oveq2d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) = ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( ( psi ` x ) + 1 ) - ( ( |_ ` x ) + 1 ) ) ) )
160 26 nnrecred 
 |-  ( x e. ( 1 [,) +oo ) -> ( 1 / ( ( |_ ` x ) + 1 ) ) e. RR )
161 160 recnd 
 |-  ( x e. ( 1 [,) +oo ) -> ( 1 / ( ( |_ ` x ) + 1 ) ) e. CC )
162 peano2cn 
 |-  ( ( psi ` x ) e. CC -> ( ( psi ` x ) + 1 ) e. CC )
163 154 162 syl 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( psi ` x ) + 1 ) e. CC )
164 161 163 155 subdid 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( ( psi ` x ) + 1 ) - ( ( |_ ` x ) + 1 ) ) ) = ( ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( psi ` x ) + 1 ) ) - ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( |_ ` x ) + 1 ) ) ) )
165 26 nnne0d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( |_ ` x ) + 1 ) =/= 0 )
166 163 155 165 divrec2d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) = ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( psi ` x ) + 1 ) ) )
167 166 eqcomd 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( psi ` x ) + 1 ) ) = ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) )
168 155 165 recid2d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( |_ ` x ) + 1 ) ) = 1 )
169 167 168 oveq12d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( psi ` x ) + 1 ) ) - ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( |_ ` x ) + 1 ) ) ) = ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) )
170 159 164 169 3eqtrd 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) = ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) )
171 29 mul01i 
 |-  ( 1 x. 0 ) = 0
172 171 a1i 
 |-  ( x e. ( 1 [,) +oo ) -> ( 1 x. 0 ) = 0 )
173 170 172 oveq12d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 1 x. 0 ) ) = ( ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) - 0 ) )
174 31 subid1d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) - 0 ) = ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) )
175 173 174 eqtrd 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 1 x. 0 ) ) = ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) )
176 97 41 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( n + 1 ) ) e. NN )
177 176 nnrecred 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( n x. ( n + 1 ) ) ) e. RR )
178 177 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( n x. ( n + 1 ) ) ) e. CC )
179 97 38 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` n ) e. RR )
180 179 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` n ) e. CC )
181 178 180 mulneg1d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( -u ( 1 / ( n x. ( n + 1 ) ) ) x. ( R ` n ) ) = -u ( ( 1 / ( n x. ( n + 1 ) ) ) x. ( R ` n ) ) )
182 98 112 mulcld 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. 1 ) e. CC )
183 98 131 mulcld 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( n + 1 ) ) e. CC )
184 176 nnne0d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. ( n + 1 ) ) =/= 0 )
185 131 182 183 184 divsubdird 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) - ( n x. 1 ) ) / ( n x. ( n + 1 ) ) ) = ( ( ( n + 1 ) / ( n x. ( n + 1 ) ) ) - ( ( n x. 1 ) / ( n x. ( n + 1 ) ) ) ) )
186 98 mulridd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n x. 1 ) = n )
187 186 oveq2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - ( n x. 1 ) ) = ( ( n + 1 ) - n ) )
188 187 134 eqtrd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - ( n x. 1 ) ) = 1 )
189 188 oveq1d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) - ( n x. 1 ) ) / ( n x. ( n + 1 ) ) ) = ( 1 / ( n x. ( n + 1 ) ) ) )
190 131 mulridd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) x. 1 ) = ( n + 1 ) )
191 131 98 mulcomd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) x. n ) = ( n x. ( n + 1 ) ) )
192 190 191 oveq12d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) x. 1 ) / ( ( n + 1 ) x. n ) ) = ( ( n + 1 ) / ( n x. ( n + 1 ) ) ) )
193 97 39 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) e. NN )
194 193 nnne0d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n + 1 ) =/= 0 )
195 112 98 131 142 194 divcan5d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) x. 1 ) / ( ( n + 1 ) x. n ) ) = ( 1 / n ) )
196 192 195 eqtr3d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) / ( n x. ( n + 1 ) ) ) = ( 1 / n ) )
197 112 131 98 194 142 divcan5d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n x. 1 ) / ( n x. ( n + 1 ) ) ) = ( 1 / ( n + 1 ) ) )
198 196 197 oveq12d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( n + 1 ) / ( n x. ( n + 1 ) ) ) - ( ( n x. 1 ) / ( n x. ( n + 1 ) ) ) ) = ( ( 1 / n ) - ( 1 / ( n + 1 ) ) ) )
199 185 189 198 3eqtr3d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( n x. ( n + 1 ) ) ) = ( ( 1 / n ) - ( 1 / ( n + 1 ) ) ) )
200 199 negeqd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> -u ( 1 / ( n x. ( n + 1 ) ) ) = -u ( ( 1 / n ) - ( 1 / ( n + 1 ) ) ) )
201 97 nnrecred 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
202 201 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
203 193 nnrecred 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( n + 1 ) ) e. RR )
204 203 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / ( n + 1 ) ) e. CC )
205 202 204 negsubdi2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> -u ( ( 1 / n ) - ( 1 / ( n + 1 ) ) ) = ( ( 1 / ( n + 1 ) ) - ( 1 / n ) ) )
206 200 205 eqtr2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 / ( n + 1 ) ) - ( 1 / n ) ) = -u ( 1 / ( n x. ( n + 1 ) ) ) )
207 97 nnrpd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
208 100 207 eqeltrd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( n + 1 ) - 1 ) e. RR+ )
209 1 pntrval 
 |-  ( ( ( n + 1 ) - 1 ) e. RR+ -> ( R ` ( ( n + 1 ) - 1 ) ) = ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) )
210 208 209 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( ( n + 1 ) - 1 ) ) = ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) )
211 100 fveq2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( ( n + 1 ) - 1 ) ) = ( R ` n ) )
212 210 211 eqtr3d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) = ( R ` n ) )
213 206 212 oveq12d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( 1 / ( n + 1 ) ) - ( 1 / n ) ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) ) = ( -u ( 1 / ( n x. ( n + 1 ) ) ) x. ( R ` n ) ) )
214 180 183 184 divrec2d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = ( ( 1 / ( n x. ( n + 1 ) ) ) x. ( R ` n ) ) )
215 214 negeqd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = -u ( ( 1 / ( n x. ( n + 1 ) ) ) x. ( R ` n ) ) )
216 181 213 215 3eqtr4d 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( 1 / ( n + 1 ) ) - ( 1 / n ) ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) ) = -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
217 96 216 sumeq12rdv 
 |-  ( x e. ( 1 [,) +oo ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( 1 / ( n + 1 ) ) - ( 1 / n ) ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
218 fzfid 
 |-  ( x e. ( 1 [,) +oo ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
219 97 42 syl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
220 219 recnd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
221 218 220 fsumneg 
 |-  ( x e. ( 1 [,) +oo ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
222 217 221 eqtrd 
 |-  ( x e. ( 1 [,) +oo ) -> sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( 1 / ( n + 1 ) ) - ( 1 / n ) ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) ) = -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
223 175 222 oveq12d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( ( 1 / ( ( |_ ` x ) + 1 ) ) x. ( ( psi ` ( ( ( |_ ` x ) + 1 ) - 1 ) ) - ( ( ( |_ ` x ) + 1 ) - 1 ) ) ) - ( 1 x. 0 ) ) - sum_ n e. ( 1 ..^ ( ( |_ ` x ) + 1 ) ) ( ( ( 1 / ( n + 1 ) ) - ( 1 / n ) ) x. ( ( psi ` ( ( n + 1 ) - 1 ) ) - ( ( n + 1 ) - 1 ) ) ) ) = ( ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) - -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
224 92 145 223 3eqtr3d 
 |-  ( x e. ( 1 [,) +oo ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) = ( ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) - -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
225 31 46 subnegd 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) - -u sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = ( ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
226 224 225 eqtrd 
 |-  ( x e. ( 1 [,) +oo ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) = ( ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) + sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
227 31 46 226 mvrladdd 
 |-  ( x e. ( 1 [,) +oo ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) - ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
228 227 mpteq2ia 
 |-  ( x e. ( 1 [,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) - ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) ) ) = ( x e. ( 1 [,) +oo ) |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
229 fzfid 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
230 33 adantl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
231 230 115 syl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
232 231 139 syl 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) - 1 ) e. RR )
233 232 230 nndivred 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) - 1 ) / n ) e. RR )
234 229 233 fsumrecl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) e. RR )
235 rpre 
 |-  ( x e. RR+ -> x e. RR )
236 235 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> x e. RR )
237 236 18 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( psi ` x ) e. RR )
238 237 20 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( psi ` x ) + 1 ) e. RR )
239 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
240 239 23 syl 
 |-  ( x e. RR+ -> ( |_ ` x ) e. NN0 )
241 240 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( |_ ` x ) e. NN0 )
242 241 25 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( |_ ` x ) + 1 ) e. NN )
243 238 242 nndivred 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) e. RR )
244 peano2rem 
 |-  ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) e. RR -> ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) e. RR )
245 243 244 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) e. RR )
246 reex 
 |-  RR e. _V
247 246 15 ssexi 
 |-  RR+ e. _V
248 247 a1i 
 |-  ( T. -> RR+ e. _V )
249 231 230 nndivred 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
250 249 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
251 229 250 fsumcl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC )
252 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
253 252 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` x ) e. RR )
254 253 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` x ) e. CC )
255 251 254 subcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC )
256 230 nnrecred 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. RR )
257 229 256 fsumrecl 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) e. RR )
258 257 253 resubcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) e. RR )
259 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) )
260 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) )
261 248 255 258 259 260 offval2 
 |-  ( T. -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) oF - ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) ) )
262 256 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / n ) e. CC )
263 229 250 262 fsumsub 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) - ( 1 / n ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) ) )
264 231 recnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. CC )
265 1cnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
266 230 nncnd 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
267 230 nnne0d 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
268 264 265 266 267 divsubdird 
 |-  ( ( ( T. /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) - 1 ) / n ) = ( ( ( Lam ` n ) / n ) - ( 1 / n ) ) )
269 268 sumeq2dv 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) - ( 1 / n ) ) )
270 257 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) e. CC )
271 251 270 254 nnncan2d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) ) )
272 263 269 271 3eqtr4rd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) )
273 272 mpteq2dva 
 |-  ( T. -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) ) )
274 261 273 eqtrd 
 |-  ( T. -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) oF - ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) ) )
275 vmadivsum 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1)
276 15 a1i 
 |-  ( T. -> RR+ C_ RR )
277 258 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) e. CC )
278 1red 
 |-  ( T. -> 1 e. RR )
279 harmoniclbnd 
 |-  ( x e. RR+ -> ( log ` x ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) )
280 279 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` x ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) )
281 253 257 280 abssubge0d 
 |-  ( ( T. /\ x e. RR+ ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) )
282 281 adantrr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) )
283 235 ad2antrl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR )
284 simprr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
285 harmonicubnd 
 |-  ( ( x e. RR /\ 1 <_ x ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
286 283 284 285 syl2anc 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) )
287 1red 
 |-  ( ( T. /\ x e. RR+ ) -> 1 e. RR )
288 257 253 287 lesubadd2d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) <_ 1 <-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) ) )
289 288 adantrr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) <_ 1 <-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) <_ ( ( log ` x ) + 1 ) ) )
290 286 289 mpbird 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) <_ 1 )
291 282 290 eqbrtrd 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) <_ 1 )
292 276 277 278 278 291 elo1d 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) e. O(1) )
293 o1sub 
 |-  ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) /\ ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) e. O(1) ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) oF - ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) ) e. O(1) )
294 275 292 293 sylancr 
 |-  ( T. -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) oF - ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / n ) - ( log ` x ) ) ) ) e. O(1) )
295 274 294 eqeltrrd 
 |-  ( T. -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) ) e. O(1) )
296 243 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) e. CC )
297 1cnd 
 |-  ( ( T. /\ x e. RR+ ) -> 1 e. CC )
298 237 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( psi ` x ) e. CC )
299 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
300 299 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( x e. CC /\ x =/= 0 ) )
301 divdir 
 |-  ( ( ( psi ` x ) e. CC /\ 1 e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( psi ` x ) + 1 ) / x ) = ( ( ( psi ` x ) / x ) + ( 1 / x ) ) )
302 298 297 300 301 syl3anc 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) + 1 ) / x ) = ( ( ( psi ` x ) / x ) + ( 1 / x ) ) )
303 302 mpteq2dva 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( psi ` x ) + 1 ) / x ) ) = ( x e. RR+ |-> ( ( ( psi ` x ) / x ) + ( 1 / x ) ) ) )
304 simpr 
 |-  ( ( T. /\ x e. RR+ ) -> x e. RR+ )
305 237 304 rerpdivcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. RR )
306 rpreccl 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR+ )
307 306 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 / x ) e. RR+ )
308 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) = ( x e. RR+ |-> ( ( psi ` x ) / x ) ) )
309 eqidd 
 |-  ( T. -> ( x e. RR+ |-> ( 1 / x ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
310 248 305 307 308 309 offval2 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) oF + ( x e. RR+ |-> ( 1 / x ) ) ) = ( x e. RR+ |-> ( ( ( psi ` x ) / x ) + ( 1 / x ) ) ) )
311 chpo1ub 
 |-  ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1)
312 divrcnv 
 |-  ( 1 e. CC -> ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0 )
313 29 312 ax-mp 
 |-  ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0
314 rlimo1 
 |-  ( ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0 -> ( x e. RR+ |-> ( 1 / x ) ) e. O(1) )
315 313 314 mp1i 
 |-  ( T. -> ( x e. RR+ |-> ( 1 / x ) ) e. O(1) )
316 o1add 
 |-  ( ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) /\ ( x e. RR+ |-> ( 1 / x ) ) e. O(1) ) -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) oF + ( x e. RR+ |-> ( 1 / x ) ) ) e. O(1) )
317 311 315 316 sylancr 
 |-  ( T. -> ( ( x e. RR+ |-> ( ( psi ` x ) / x ) ) oF + ( x e. RR+ |-> ( 1 / x ) ) ) e. O(1) )
318 310 317 eqeltrrd 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( psi ` x ) / x ) + ( 1 / x ) ) ) e. O(1) )
319 303 318 eqeltrd 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( psi ` x ) + 1 ) / x ) ) e. O(1) )
320 238 304 rerpdivcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) + 1 ) / x ) e. RR )
321 chpge0 
 |-  ( x e. RR -> 0 <_ ( psi ` x ) )
322 236 321 syl 
 |-  ( ( T. /\ x e. RR+ ) -> 0 <_ ( psi ` x ) )
323 237 322 ge0p1rpd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( psi ` x ) + 1 ) e. RR+ )
324 323 rprege0d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) + 1 ) e. RR /\ 0 <_ ( ( psi ` x ) + 1 ) ) )
325 242 nnrpd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( |_ ` x ) + 1 ) e. RR+ )
326 325 rpregt0d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( |_ ` x ) + 1 ) e. RR /\ 0 < ( ( |_ ` x ) + 1 ) ) )
327 divge0 
 |-  ( ( ( ( ( psi ` x ) + 1 ) e. RR /\ 0 <_ ( ( psi ` x ) + 1 ) ) /\ ( ( ( |_ ` x ) + 1 ) e. RR /\ 0 < ( ( |_ ` x ) + 1 ) ) ) -> 0 <_ ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) )
328 324 326 327 syl2anc 
 |-  ( ( T. /\ x e. RR+ ) -> 0 <_ ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) )
329 243 328 absidd 
 |-  ( ( T. /\ x e. RR+ ) -> ( abs ` ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) ) = ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) )
330 320 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) + 1 ) / x ) e. CC )
331 330 abscld 
 |-  ( ( T. /\ x e. RR+ ) -> ( abs ` ( ( ( psi ` x ) + 1 ) / x ) ) e. RR )
332 fllep1 
 |-  ( x e. RR -> x <_ ( ( |_ ` x ) + 1 ) )
333 236 332 syl 
 |-  ( ( T. /\ x e. RR+ ) -> x <_ ( ( |_ ` x ) + 1 ) )
334 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
335 334 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( x e. RR /\ 0 < x ) )
336 323 rpregt0d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) + 1 ) e. RR /\ 0 < ( ( psi ` x ) + 1 ) ) )
337 lediv2 
 |-  ( ( ( x e. RR /\ 0 < x ) /\ ( ( ( |_ ` x ) + 1 ) e. RR /\ 0 < ( ( |_ ` x ) + 1 ) ) /\ ( ( ( psi ` x ) + 1 ) e. RR /\ 0 < ( ( psi ` x ) + 1 ) ) ) -> ( x <_ ( ( |_ ` x ) + 1 ) <-> ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) <_ ( ( ( psi ` x ) + 1 ) / x ) ) )
338 335 326 336 337 syl3anc 
 |-  ( ( T. /\ x e. RR+ ) -> ( x <_ ( ( |_ ` x ) + 1 ) <-> ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) <_ ( ( ( psi ` x ) + 1 ) / x ) ) )
339 333 338 mpbid 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) <_ ( ( ( psi ` x ) + 1 ) / x ) )
340 320 leabsd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) + 1 ) / x ) <_ ( abs ` ( ( ( psi ` x ) + 1 ) / x ) ) )
341 243 320 331 339 340 letrd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) <_ ( abs ` ( ( ( psi ` x ) + 1 ) / x ) ) )
342 329 341 eqbrtrd 
 |-  ( ( T. /\ x e. RR+ ) -> ( abs ` ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) ) <_ ( abs ` ( ( ( psi ` x ) + 1 ) / x ) ) )
343 342 adantrr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) ) <_ ( abs ` ( ( ( psi ` x ) + 1 ) / x ) ) )
344 278 319 320 296 343 o1le 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) ) e. O(1) )
345 o1const 
 |-  ( ( RR+ C_ RR /\ 1 e. CC ) -> ( x e. RR+ |-> 1 ) e. O(1) )
346 15 29 345 mp2an 
 |-  ( x e. RR+ |-> 1 ) e. O(1)
347 346 a1i 
 |-  ( T. -> ( x e. RR+ |-> 1 ) e. O(1) )
348 296 297 344 347 o1sub2 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) ) e. O(1) )
349 234 245 295 348 o1sub2 
 |-  ( T. -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) - ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) ) ) e. O(1) )
350 14 349 o1res2 
 |-  ( T. -> ( x e. ( 1 [,) +oo ) |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) - 1 ) / n ) - ( ( ( ( psi ` x ) + 1 ) / ( ( |_ ` x ) + 1 ) ) - 1 ) ) ) e. O(1) )
351 228 350 eqeltrrid 
 |-  ( T. -> ( x e. ( 1 [,) +oo ) |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. O(1) )
352 17 351 eqeltrd 
 |-  ( T. -> ( ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) |` ( 1 [,) +oo ) ) e. O(1) )
353 eqid 
 |-  ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
354 353 45 fmpti 
 |-  ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) : RR --> CC
355 354 a1i 
 |-  ( T. -> ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) : RR --> CC )
356 ssidd 
 |-  ( T. -> RR C_ RR )
357 355 356 278 o1resb 
 |-  ( T. -> ( ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. O(1) <-> ( ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) |` ( 1 [,) +oo ) ) e. O(1) ) )
358 352 357 mpbird 
 |-  ( T. -> ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. O(1) )
359 358 mptru 
 |-  ( x e. RR |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. O(1)