Metamath Proof Explorer

Theorem pntpbnd

Description: Lemma for pnt . Establish smallness of R at a point. Lemma 10.6.1 in Shapiro, p. 436. (Contributed by Mario Carneiro, 10-Apr-2016)

Ref Expression
Hypothesis pntibnd.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion pntpbnd 
|- E. c e. RR+ A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e )

Proof

Step Hyp Ref Expression
1 pntibnd.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 1 pntrsumbnd2 
 |-  E. d e. RR+ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d
3 simpl 
 |-  ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) -> d e. RR+ )
4 2rp 
 |-  2 e. RR+
5 rpaddcl 
 |-  ( ( d e. RR+ /\ 2 e. RR+ ) -> ( d + 2 ) e. RR+ )
6 3 4 5 sylancl 
 |-  ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) -> ( d + 2 ) e. RR+ )
7 2re 
 |-  2 e. RR
8 elioore 
 |-  ( e e. ( 0 (,) 1 ) -> e e. RR )
9 8 adantl 
 |-  ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> e e. RR )
10 eliooord 
 |-  ( e e. ( 0 (,) 1 ) -> ( 0 < e /\ e < 1 ) )
11 10 adantl 
 |-  ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> ( 0 < e /\ e < 1 ) )
12 11 simpld 
 |-  ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> 0 < e )
13 9 12 elrpd 
 |-  ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> e e. RR+ )
14 rerpdivcl 
 |-  ( ( 2 e. RR /\ e e. RR+ ) -> ( 2 / e ) e. RR )
15 7 13 14 sylancr 
 |-  ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> ( 2 / e ) e. RR )
16 15 rpefcld 
 |-  ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> ( exp ` ( 2 / e ) ) e. RR+ )
17 simpllr 
 |-  ( ( ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) /\ y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) ) ) /\ -. E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) -> e e. ( 0 (,) 1 ) )
18 eqid 
 |-  ( exp ` ( 2 / e ) ) = ( exp ` ( 2 / e ) )
19 simplrr 
 |-  ( ( ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) /\ y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) ) ) /\ -. E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) -> y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) )
20 simp-4l 
 |-  ( ( ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) /\ y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) ) ) /\ -. E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) -> d e. RR+ )
21 simp-4r 
 |-  ( ( ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) /\ y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) ) ) /\ -. E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) -> A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d )
22 eqid 
 |-  ( d + 2 ) = ( d + 2 )
23 simplrl 
 |-  ( ( ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) /\ y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) ) ) /\ -. E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) -> k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) )
24 simpr 
 |-  ( ( ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) /\ y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) ) ) /\ -. E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) -> -. E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) )
25 1 17 18 19 20 21 22 23 24 pntpbnd2 
 |-  -. ( ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) /\ y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) ) ) /\ -. E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) )
26 iman 
 |-  ( ( ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) /\ y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) ) ) -> E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) <-> -. ( ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) /\ y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) ) ) /\ -. E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) )
27 25 26 mpbir 
 |-  ( ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) /\ y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) ) ) -> E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) )
28 27 ralrimivva 
 |-  ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) )
29 oveq1 
 |-  ( x = ( exp ` ( 2 / e ) ) -> ( x (,) +oo ) = ( ( exp ` ( 2 / e ) ) (,) +oo ) )
30 29 raleqdv 
 |-  ( x = ( exp ` ( 2 / e ) ) -> ( A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) <-> A. y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) )
31 30 ralbidv 
 |-  ( x = ( exp ` ( 2 / e ) ) -> ( A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) <-> A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) )
32 31 rspcev 
 |-  ( ( ( exp ` ( 2 / e ) ) e. RR+ /\ A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( ( exp ` ( 2 / e ) ) (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) -> E. x e. RR+ A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) )
33 16 28 32 syl2anc 
 |-  ( ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> E. x e. RR+ A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) )
34 33 ralrimiva 
 |-  ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) )
35 fvoveq1 
 |-  ( c = ( d + 2 ) -> ( exp ` ( c / e ) ) = ( exp ` ( ( d + 2 ) / e ) ) )
36 35 oveq1d 
 |-  ( c = ( d + 2 ) -> ( ( exp ` ( c / e ) ) [,) +oo ) = ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) )
37 36 raleqdv 
 |-  ( c = ( d + 2 ) -> ( A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) <-> A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) )
38 37 rexbidv 
 |-  ( c = ( d + 2 ) -> ( E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) <-> E. x e. RR+ A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) )
39 38 ralbidv 
 |-  ( c = ( d + 2 ) -> ( A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) <-> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) )
40 39 rspcev 
 |-  ( ( ( d + 2 ) e. RR+ /\ A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( ( d + 2 ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) ) -> E. c e. RR+ A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) )
41 6 34 40 syl2anc 
 |-  ( ( d e. RR+ /\ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d ) -> E. c e. RR+ A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) )
42 41 rexlimiva 
 |-  ( E. d e. RR+ A. i e. NN A. j e. ZZ ( abs ` sum_ n e. ( i ... j ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ d -> E. c e. RR+ A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e ) )
43 2 42 ax-mp 
 |-  E. c e. RR+ A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. n e. NN ( ( y < n /\ n <_ ( k x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ e )