Metamath Proof Explorer

Theorem pntrsumbnd2

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

Ref Expression
Hypothesis pntrval.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion pntrsumbnd2 
|- E. c e. RR+ A. k e. NN A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c

Proof

Step Hyp Ref Expression
1 pntrval.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 1 pntrsumbnd 
 |-  E. b e. RR+ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b
3 2rp 
 |-  2 e. RR+
4 rpmulcl 
 |-  ( ( 2 e. RR+ /\ b e. RR+ ) -> ( 2 x. b ) e. RR+ )
5 3 4 mpan 
 |-  ( b e. RR+ -> ( 2 x. b ) e. RR+ )
6 oveq2 
 |-  ( m = ( k - 1 ) -> ( 1 ... m ) = ( 1 ... ( k - 1 ) ) )
7 6 sumeq1d 
 |-  ( m = ( k - 1 ) -> sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
8 7 fveq2d 
 |-  ( m = ( k - 1 ) -> ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
9 8 breq1d 
 |-  ( m = ( k - 1 ) -> ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b <-> ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) )
10 simplr 
 |-  ( ( ( b e. RR+ /\ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) /\ k e. NN ) -> A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b )
11 nnz 
 |-  ( k e. NN -> k e. ZZ )
12 11 adantl 
 |-  ( ( ( b e. RR+ /\ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) /\ k e. NN ) -> k e. ZZ )
13 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
14 12 13 syl 
 |-  ( ( ( b e. RR+ /\ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) /\ k e. NN ) -> ( k - 1 ) e. ZZ )
15 9 10 14 rspcdva 
 |-  ( ( ( b e. RR+ /\ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) /\ k e. NN ) -> ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b )
16 5 ad2antrr 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) -> ( 2 x. b ) e. RR+ )
17 16 rpge0d 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) -> 0 <_ ( 2 x. b ) )
18 sumeq1 
 |-  ( ( k ... m ) = (/) -> sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = sum_ n e. (/) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
19 sum0 
 |-  sum_ n e. (/) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = 0
20 18 19 eqtrdi 
 |-  ( ( k ... m ) = (/) -> sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = 0 )
21 20 abs00bd 
 |-  ( ( k ... m ) = (/) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = 0 )
22 21 breq1d 
 |-  ( ( k ... m ) = (/) -> ( ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) <-> 0 <_ ( 2 x. b ) ) )
23 17 22 syl5ibrcom 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) -> ( ( k ... m ) = (/) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
24 23 imp 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ ( k ... m ) = (/) ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) )
25 24 a1d 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ ( k ... m ) = (/) ) -> ( ( ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b /\ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
26 fzn0 
 |-  ( ( k ... m ) =/= (/) <-> m e. ( ZZ>= ` k ) )
27 fzfid 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( 1 ... m ) e. Fin )
28 elfznn 
 |-  ( n e. ( 1 ... m ) -> n e. NN )
29 simpr 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. NN ) -> n e. NN )
30 29 nnrpd 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. NN ) -> n e. RR+ )
31 1 pntrf 
 |-  R : RR+ --> RR
32 31 ffvelrni 
 |-  ( n e. RR+ -> ( R ` n ) e. RR )
33 30 32 syl 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. NN ) -> ( R ` n ) e. RR )
34 29 peano2nnd 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. NN ) -> ( n + 1 ) e. NN )
35 29 34 nnmulcld 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. NN ) -> ( n x. ( n + 1 ) ) e. NN )
36 33 35 nndivred 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. NN ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
37 28 36 sylan2 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. ( 1 ... m ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
38 27 37 fsumrecl 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
39 38 recnd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
40 39 abscld 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
41 fzfid 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( 1 ... ( k - 1 ) ) e. Fin )
42 elfznn 
 |-  ( n e. ( 1 ... ( k - 1 ) ) -> n e. NN )
43 42 36 sylan2 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. ( 1 ... ( k - 1 ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
44 41 43 fsumrecl 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
45 44 recnd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
46 45 abscld 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
47 simplll 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> b e. RR+ )
48 47 rpred 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> b e. RR )
49 le2add 
 |-  ( ( ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR /\ ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR ) /\ ( b e. RR /\ b e. RR ) ) -> ( ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b /\ ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) <_ ( b + b ) ) )
50 40 46 48 48 49 syl22anc 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b /\ ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) <_ ( b + b ) ) )
51 48 recnd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> b e. CC )
52 51 2timesd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( 2 x. b ) = ( b + b ) )
53 52 breq2d 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) <_ ( 2 x. b ) <-> ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) <_ ( b + b ) ) )
54 fzfid 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( k ... m ) e. Fin )
55 simpllr 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> k e. NN )
56 elfzuz 
 |-  ( n e. ( k ... m ) -> n e. ( ZZ>= ` k ) )
57 eluznn 
 |-  ( ( k e. NN /\ n e. ( ZZ>= ` k ) ) -> n e. NN )
58 55 56 57 syl2an 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. ( k ... m ) ) -> n e. NN )
59 58 36 syldan 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. ( k ... m ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
60 54 59 fsumrecl 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
61 60 recnd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
62 55 nnred 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> k e. RR )
63 62 ltm1d 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( k - 1 ) < k )
64 fzdisj 
 |-  ( ( k - 1 ) < k -> ( ( 1 ... ( k - 1 ) ) i^i ( k ... m ) ) = (/) )
65 63 64 syl 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( 1 ... ( k - 1 ) ) i^i ( k ... m ) ) = (/) )
66 55 nncnd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> k e. CC )
67 ax-1cn 
 |-  1 e. CC
68 npcan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k - 1 ) + 1 ) = k )
69 66 67 68 sylancl 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( k - 1 ) + 1 ) = k )
70 69 55 eqeltrd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( k - 1 ) + 1 ) e. NN )
71 nnuz 
 |-  NN = ( ZZ>= ` 1 )
72 70 71 eleqtrdi 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( k - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
73 55 nnzd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> k e. ZZ )
74 73 13 syl 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( k - 1 ) e. ZZ )
75 simplr 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) -> k e. NN )
76 75 nncnd 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) -> k e. CC )
77 76 67 68 sylancl 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) -> ( ( k - 1 ) + 1 ) = k )
78 77 fveq2d 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) -> ( ZZ>= ` ( ( k - 1 ) + 1 ) ) = ( ZZ>= ` k ) )
79 78 eleq2d 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) -> ( m e. ( ZZ>= ` ( ( k - 1 ) + 1 ) ) <-> m e. ( ZZ>= ` k ) ) )
80 79 biimpar 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> m e. ( ZZ>= ` ( ( k - 1 ) + 1 ) ) )
81 peano2uzr 
 |-  ( ( ( k - 1 ) e. ZZ /\ m e. ( ZZ>= ` ( ( k - 1 ) + 1 ) ) ) -> m e. ( ZZ>= ` ( k - 1 ) ) )
82 74 80 81 syl2anc 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> m e. ( ZZ>= ` ( k - 1 ) ) )
83 fzsplit2 
 |-  ( ( ( ( k - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ m e. ( ZZ>= ` ( k - 1 ) ) ) -> ( 1 ... m ) = ( ( 1 ... ( k - 1 ) ) u. ( ( ( k - 1 ) + 1 ) ... m ) ) )
84 72 82 83 syl2anc 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( 1 ... m ) = ( ( 1 ... ( k - 1 ) ) u. ( ( ( k - 1 ) + 1 ) ... m ) ) )
85 69 oveq1d 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( ( k - 1 ) + 1 ) ... m ) = ( k ... m ) )
86 85 uneq2d 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( 1 ... ( k - 1 ) ) u. ( ( ( k - 1 ) + 1 ) ... m ) ) = ( ( 1 ... ( k - 1 ) ) u. ( k ... m ) ) )
87 84 86 eqtrd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( 1 ... m ) = ( ( 1 ... ( k - 1 ) ) u. ( k ... m ) ) )
88 37 recnd 
 |-  ( ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) /\ n e. ( 1 ... m ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
89 65 87 27 88 fsumsplit 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = ( sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) + sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
90 45 61 89 mvrladdd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) - sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
91 90 fveq2d 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( abs ` ( sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) - sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) = ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
92 39 45 abs2dif2d 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( abs ` ( sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) - sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) <_ ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) )
93 91 92 eqbrtrrd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) )
94 61 abscld 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
95 40 46 readdcld 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) e. RR )
96 2re 
 |-  2 e. RR
97 96 a1i 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> 2 e. RR )
98 97 48 remulcld 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( 2 x. b ) e. RR )
99 letr 
 |-  ( ( ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR /\ ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) e. RR /\ ( 2 x. b ) e. RR ) -> ( ( ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) /\ ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) <_ ( 2 x. b ) ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
100 94 95 98 99 syl3anc 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) /\ ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) <_ ( 2 x. b ) ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
101 93 100 mpand 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) <_ ( 2 x. b ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
102 53 101 sylbird 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) + ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) ) <_ ( b + b ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
103 50 102 syld 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b /\ ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
104 103 ancomsd 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ m e. ( ZZ>= ` k ) ) -> ( ( ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b /\ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
105 26 104 sylan2b 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ ( k ... m ) =/= (/) ) -> ( ( ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b /\ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
106 25 105 pm2.61dane 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) -> ( ( ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b /\ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
107 106 imp 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ m e. ZZ ) /\ ( ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b /\ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) )
108 107 an4s 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) /\ ( m e. ZZ /\ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) ) -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) )
109 108 expr 
 |-  ( ( ( ( b e. RR+ /\ k e. NN ) /\ ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) /\ m e. ZZ ) -> ( ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b -> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
110 109 ralimdva 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> ( A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b -> A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
111 110 impancom 
 |-  ( ( ( b e. RR+ /\ k e. NN ) /\ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> ( ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b -> A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
112 111 an32s 
 |-  ( ( ( b e. RR+ /\ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) /\ k e. NN ) -> ( ( abs ` sum_ n e. ( 1 ... ( k - 1 ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b -> A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
113 15 112 mpd 
 |-  ( ( ( b e. RR+ /\ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) /\ k e. NN ) -> A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) )
114 113 ralrimiva 
 |-  ( ( b e. RR+ /\ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> A. k e. NN A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) )
115 breq2 
 |-  ( c = ( 2 x. b ) -> ( ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c <-> ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
116 115 2ralbidv 
 |-  ( c = ( 2 x. b ) -> ( A. k e. NN A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c <-> A. k e. NN A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) )
117 116 rspcev 
 |-  ( ( ( 2 x. b ) e. RR+ /\ A. k e. NN A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ ( 2 x. b ) ) -> E. c e. RR+ A. k e. NN A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c )
118 5 114 117 syl2an2r 
 |-  ( ( b e. RR+ /\ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b ) -> E. c e. RR+ A. k e. NN A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c )
119 118 rexlimiva 
 |-  ( E. b e. RR+ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ b -> E. c e. RR+ A. k e. NN A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c )
120 2 119 ax-mp 
 |-  E. c e. RR+ A. k e. NN A. m e. ZZ ( abs ` sum_ n e. ( k ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c