Metamath Proof Explorer

Theorem pntrsumbnd

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 pntrsumbnd 
|- E. c e. RR+ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c

Proof

Step Hyp Ref Expression
1 pntrval.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 ssidd 
 |-  ( T. -> RR C_ RR )
3 1red 
 |-  ( T. -> 1 e. RR )
4 fzfid 
 |-  ( ( T. /\ m e. RR ) -> ( 1 ... ( |_ ` m ) ) e. Fin )
5 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` m ) ) -> n e. NN )
6 5 adantl 
 |-  ( ( ( T. /\ m e. RR ) /\ n e. ( 1 ... ( |_ ` m ) ) ) -> n e. NN )
7 nnrp 
 |-  ( n e. NN -> n e. RR+ )
8 1 pntrf 
 |-  R : RR+ --> RR
9 8 ffvelrni 
 |-  ( n e. RR+ -> ( R ` n ) e. RR )
10 7 9 syl 
 |-  ( n e. NN -> ( R ` n ) e. RR )
11 peano2nn 
 |-  ( n e. NN -> ( n + 1 ) e. NN )
12 nnmulcl 
 |-  ( ( n e. NN /\ ( n + 1 ) e. NN ) -> ( n x. ( n + 1 ) ) e. NN )
13 11 12 mpdan 
 |-  ( n e. NN -> ( n x. ( n + 1 ) ) e. NN )
14 10 13 nndivred 
 |-  ( n e. NN -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
15 14 recnd 
 |-  ( n e. NN -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
16 6 15 syl 
 |-  ( ( ( T. /\ m e. RR ) /\ n e. ( 1 ... ( |_ ` m ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
17 4 16 fsumcl 
 |-  ( ( T. /\ m e. RR ) -> sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
18 1 pntrsumo1 
 |-  ( m e. RR |-> sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. O(1)
19 18 a1i 
 |-  ( T. -> ( m e. RR |-> sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. O(1) )
20 fzfid 
 |-  ( ( T. /\ ( x e. RR /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
21 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
22 21 adantl 
 |-  ( ( ( T. /\ ( x e. RR /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
23 22 15 syl 
 |-  ( ( ( T. /\ ( x e. RR /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
24 23 abscld 
 |-  ( ( ( T. /\ ( x e. RR /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
25 20 24 fsumrecl 
 |-  ( ( T. /\ ( x e. RR /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
26 17 adantr 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
27 26 abscld 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
28 fzfid 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> ( 1 ... ( |_ ` m ) ) e. Fin )
29 16 adantlr 
 |-  ( ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) /\ n e. ( 1 ... ( |_ ` m ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
30 29 abscld 
 |-  ( ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) /\ n e. ( 1 ... ( |_ ` m ) ) ) -> ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
31 28 30 fsumrecl 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> sum_ n e. ( 1 ... ( |_ ` m ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
32 25 ad2ant2r 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
33 28 29 fsumabs 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` m ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
34 fzfid 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
35 21 adantl 
 |-  ( ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
36 35 15 syl 
 |-  ( ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
37 36 abscld 
 |-  ( ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) e. RR )
38 36 absge0d 
 |-  ( ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
39 simplr 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> m e. RR )
40 simprll 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> x e. RR )
41 simprr 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> m < x )
42 39 40 41 ltled 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> m <_ x )
43 flword2 
 |-  ( ( m e. RR /\ x e. RR /\ m <_ x ) -> ( |_ ` x ) e. ( ZZ>= ` ( |_ ` m ) ) )
44 39 40 42 43 syl3anc 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> ( |_ ` x ) e. ( ZZ>= ` ( |_ ` m ) ) )
45 fzss2 
 |-  ( ( |_ ` x ) e. ( ZZ>= ` ( |_ ` m ) ) -> ( 1 ... ( |_ ` m ) ) C_ ( 1 ... ( |_ ` x ) ) )
46 44 45 syl 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> ( 1 ... ( |_ ` m ) ) C_ ( 1 ... ( |_ ` x ) ) )
47 34 37 38 46 fsumless 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> sum_ n e. ( 1 ... ( |_ ` m ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
48 27 31 32 33 47 letrd 
 |-  ( ( ( T. /\ m e. RR ) /\ ( ( x e. RR /\ 1 <_ x ) /\ m < x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
49 2 3 17 19 25 48 o1bddrp 
 |-  ( T. -> E. c e. RR+ A. m e. RR ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c )
50 49 mptru 
 |-  E. c e. RR+ A. m e. RR ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c
51 zre 
 |-  ( m e. ZZ -> m e. RR )
52 51 imim1i 
 |-  ( ( m e. RR -> ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c ) -> ( m e. ZZ -> ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c ) )
53 flid 
 |-  ( m e. ZZ -> ( |_ ` m ) = m )
54 53 oveq2d 
 |-  ( m e. ZZ -> ( 1 ... ( |_ ` m ) ) = ( 1 ... m ) )
55 54 sumeq1d 
 |-  ( m e. ZZ -> sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
56 55 fveq2d 
 |-  ( m e. ZZ -> ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
57 56 breq1d 
 |-  ( m e. ZZ -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c <-> ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c ) )
58 52 57 mpbidi 
 |-  ( ( m e. RR -> ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c ) -> ( m e. ZZ -> ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c ) )
59 58 ralimi2 
 |-  ( A. m e. RR ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c -> A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c )
60 59 reximi 
 |-  ( E. c e. RR+ A. m e. RR ( abs ` sum_ n e. ( 1 ... ( |_ ` m ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c -> E. c e. RR+ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c )
61 50 60 ax-mp 
 |-  E. c e. RR+ A. m e. ZZ ( abs ` sum_ n e. ( 1 ... m ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ c