Theorem pnt3

Description: The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to x . (Contributed by Mario Carneiro, 1-Jun-2016)

	Ref	Expression
Assertion	pnt3	|- ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( a e. RR+ |-> ( ( psi ` a ) - a ) ) = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2	1	pntrmax	|- E. b e. RR+ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b
3	1	pntibnd	|- E. c e. RR+ E. l e. ( 0 (,) 1 ) A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e )
4		simpll	|- ( ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) /\ ( ( c e. RR+ /\ l e. ( 0 (,) 1 ) ) /\ A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) ) -> b e. RR+ )
5		simplr	|- ( ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) /\ ( ( c e. RR+ /\ l e. ( 0 (,) 1 ) ) /\ A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) ) -> A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b )
6		fveq2	|- ( r = x -> ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) = ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` x ) )
7		id	|- ( r = x -> r = x )
8	6 7	oveq12d	|- ( r = x -> ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) = ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` x ) / x ) )
9	8	fveq2d	|- ( r = x -> ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) = ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` x ) / x ) ) )
10	9	breq1d	|- ( r = x -> ( ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b <-> ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` x ) / x ) ) <_ b ) )
11	10	cbvralvw	|- ( A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b <-> A. x e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` x ) / x ) ) <_ b )
12	5 11	sylib	|- ( ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) /\ ( ( c e. RR+ /\ l e. ( 0 (,) 1 ) ) /\ A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) ) -> A. x e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` x ) / x ) ) <_ b )
13		simprll	|- ( ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) /\ ( ( c e. RR+ /\ l e. ( 0 (,) 1 ) ) /\ A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) ) -> c e. RR+ )
14		simprlr	|- ( ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) /\ ( ( c e. RR+ /\ l e. ( 0 (,) 1 ) ) /\ A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) ) -> l e. ( 0 (,) 1 ) )
15		eqid	|- ( b + 1 ) = ( b + 1 )
16		eqid	|- ( ( 1 - ( 1 / ( b + 1 ) ) ) x. ( ( l / ( ; 3 2 x. c ) ) / ( ( b + 1 ) ^ 2 ) ) ) = ( ( 1 - ( 1 / ( b + 1 ) ) ) x. ( ( l / ( ; 3 2 x. c ) ) / ( ( b + 1 ) ^ 2 ) ) )
17		simprr	|- ( ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) /\ ( ( c e. RR+ /\ l e. ( 0 (,) 1 ) ) /\ A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) ) -> A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) )
18		breq2	|- ( z = g -> ( y < z <-> y < g ) )
19		oveq2	|- ( z = g -> ( ( 1 + ( l x. e ) ) x. z ) = ( ( 1 + ( l x. e ) ) x. g ) )
20	19	breq1d	|- ( z = g -> ( ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) <-> ( ( 1 + ( l x. e ) ) x. g ) < ( k x. y ) ) )
21	18 20	anbi12d	|- ( z = g -> ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) <-> ( y < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. y ) ) ) )
22		id	|- ( z = g -> z = g )
23	22 19	oveq12d	|- ( z = g -> ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) = ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) )
24	23	raleqdv	|- ( z = g -> ( A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e <-> A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) )
25	21 24	anbi12d	|- ( z = g -> ( ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> ( ( y < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. y ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) )
26	25	cbvrexvw	|- ( E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> E. g e. RR+ ( ( y < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. y ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) )
27		breq1	|- ( y = f -> ( y < g <-> f < g ) )
28		oveq2	|- ( y = f -> ( k x. y ) = ( k x. f ) )
29	28	breq2d	|- ( y = f -> ( ( ( 1 + ( l x. e ) ) x. g ) < ( k x. y ) <-> ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) )
30	27 29	anbi12d	|- ( y = f -> ( ( y < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. y ) ) <-> ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) ) )
31	30	anbi1d	|- ( y = f -> ( ( ( y < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. y ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) )
32	31	rexbidv	|- ( y = f -> ( E. g e. RR+ ( ( y < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. y ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> E. g e. RR+ ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) )
33	26 32	syl5bb	|- ( y = f -> ( E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> E. g e. RR+ ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) )
34	33	cbvralvw	|- ( A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> A. f e. ( r (,) +oo ) E. g e. RR+ ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) )
35		oveq1	|- ( r = x -> ( r (,) +oo ) = ( x (,) +oo ) )
36	35	raleqdv	|- ( r = x -> ( A. f e. ( r (,) +oo ) E. g e. RR+ ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> A. f e. ( x (,) +oo ) E. g e. RR+ ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) )
37	34 36	syl5bb	|- ( r = x -> ( A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> A. f e. ( x (,) +oo ) E. g e. RR+ ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) )
38	37	ralbidv	|- ( r = x -> ( A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. f e. ( x (,) +oo ) E. g e. RR+ ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) )
39	38	cbvrexvw	|- ( E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. f e. ( x (,) +oo ) E. g e. RR+ ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) )
40	39	ralbii	|- ( A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) <-> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. f e. ( x (,) +oo ) E. g e. RR+ ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) )
41	17 40	sylib	|- ( ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) /\ ( ( c e. RR+ /\ l e. ( 0 (,) 1 ) ) /\ A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) ) -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. f e. ( x (,) +oo ) E. g e. RR+ ( ( f < g /\ ( ( 1 + ( l x. e ) ) x. g ) < ( k x. f ) ) /\ A. u e. ( g [,] ( ( 1 + ( l x. e ) ) x. g ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) )
42	1 4 12 13 14 15 16 41	pntleml	|- ( ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) /\ ( ( c e. RR+ /\ l e. ( 0 (,) 1 ) ) /\ A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) ) ) -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1 )
43	42	expr	|- ( ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) /\ ( c e. RR+ /\ l e. ( 0 (,) 1 ) ) ) -> ( A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1 ) )
44	43	rexlimdvva	|- ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) -> ( E. c e. RR+ E. l e. ( 0 (,) 1 ) A. e e. ( 0 (,) 1 ) E. r e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( r (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` u ) / u ) ) <_ e ) -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1 ) )
45	3 44	mpi	|- ( ( b e. RR+ /\ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b ) -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1 )
46	45	rexlimiva	|- ( E. b e. RR+ A. r e. RR+ ( abs ` ( ( ( a e. RR+ |-> ( ( psi ` a ) - a ) ) ` r ) / r ) ) <_ b -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1 )
47	2 46	ax-mp	|- ( x e. RR+ |-> ( ( psi ` x ) / x ) ) ~~>r 1