Metamath Proof Explorer

Theorem pntrmax

Description: There is a bound on the residual valid for all x . (Contributed by Mario Carneiro, 9-Apr-2016)

Ref Expression
Hypothesis pntrval.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion pntrmax 
|- E. c e. RR+ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ c

Proof

Step Hyp Ref Expression
1 pntrval.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 rpssre 
 |-  RR+ C_ RR
3 2 a1i 
 |-  ( T. -> RR+ C_ RR )
4 1red 
 |-  ( T. -> 1 e. RR )
5 1 pntrval 
 |-  ( x e. RR+ -> ( R ` x ) = ( ( psi ` x ) - x ) )
6 rpre 
 |-  ( x e. RR+ -> x e. RR )
7 chpcl 
 |-  ( x e. RR -> ( psi ` x ) e. RR )
8 6 7 syl 
 |-  ( x e. RR+ -> ( psi ` x ) e. RR )
9 8 6 resubcld 
 |-  ( x e. RR+ -> ( ( psi ` x ) - x ) e. RR )
10 5 9 eqeltrd 
 |-  ( x e. RR+ -> ( R ` x ) e. RR )
11 rerpdivcl 
 |-  ( ( ( R ` x ) e. RR /\ x e. RR+ ) -> ( ( R ` x ) / x ) e. RR )
12 10 11 mpancom 
 |-  ( x e. RR+ -> ( ( R ` x ) / x ) e. RR )
13 12 recnd 
 |-  ( x e. RR+ -> ( ( R ` x ) / x ) e. CC )
14 13 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( R ` x ) / x ) e. CC )
15 5 oveq1d 
 |-  ( x e. RR+ -> ( ( R ` x ) / x ) = ( ( ( psi ` x ) - x ) / x ) )
16 8 recnd 
 |-  ( x e. RR+ -> ( psi ` x ) e. CC )
17 rpcn 
 |-  ( x e. RR+ -> x e. CC )
18 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
19 16 17 17 18 divsubdird 
 |-  ( x e. RR+ -> ( ( ( psi ` x ) - x ) / x ) = ( ( ( psi ` x ) / x ) - ( x / x ) ) )
20 17 18 dividd 
 |-  ( x e. RR+ -> ( x / x ) = 1 )
21 20 oveq2d 
 |-  ( x e. RR+ -> ( ( ( psi ` x ) / x ) - ( x / x ) ) = ( ( ( psi ` x ) / x ) - 1 ) )
22 15 19 21 3eqtrd 
 |-  ( x e. RR+ -> ( ( R ` x ) / x ) = ( ( ( psi ` x ) / x ) - 1 ) )
23 22 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( R ` x ) / x ) ) = ( x e. RR+ |-> ( ( ( psi ` x ) / x ) - 1 ) )
24 rerpdivcl 
 |-  ( ( ( psi ` x ) e. RR /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. RR )
25 8 24 mpancom 
 |-  ( x e. RR+ -> ( ( psi ` x ) / x ) e. RR )
26 25 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( psi ` x ) / x ) e. RR )
27 1red 
 |-  ( ( T. /\ x e. RR+ ) -> 1 e. RR )
28 chpo1ub 
 |-  ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1)
29 28 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( psi ` x ) / x ) ) e. O(1) )
30 ax-1cn 
 |-  1 e. CC
31 o1const 
 |-  ( ( RR+ C_ RR /\ 1 e. CC ) -> ( x e. RR+ |-> 1 ) e. O(1) )
32 2 30 31 mp2an 
 |-  ( x e. RR+ |-> 1 ) e. O(1)
33 32 a1i 
 |-  ( T. -> ( x e. RR+ |-> 1 ) e. O(1) )
34 26 27 29 33 o1sub2 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( psi ` x ) / x ) - 1 ) ) e. O(1) )
35 23 34 eqeltrid 
 |-  ( T. -> ( x e. RR+ |-> ( ( R ` x ) / x ) ) e. O(1) )
36 chpcl 
 |-  ( y e. RR -> ( psi ` y ) e. RR )
37 peano2re 
 |-  ( ( psi ` y ) e. RR -> ( ( psi ` y ) + 1 ) e. RR )
38 36 37 syl 
 |-  ( y e. RR -> ( ( psi ` y ) + 1 ) e. RR )
39 38 ad2antrl 
 |-  ( ( T. /\ ( y e. RR /\ 1 <_ y ) ) -> ( ( psi ` y ) + 1 ) e. RR )
40 22 3ad2ant1 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( R ` x ) / x ) = ( ( ( psi ` x ) / x ) - 1 ) )
41 40 fveq2d 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( abs ` ( ( R ` x ) / x ) ) = ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) )
42 1re 
 |-  1 e. RR
43 38 3ad2ant2 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( psi ` y ) + 1 ) e. RR )
44 resubcl 
 |-  ( ( 1 e. RR /\ ( ( psi ` y ) + 1 ) e. RR ) -> ( 1 - ( ( psi ` y ) + 1 ) ) e. RR )
45 42 43 44 sylancr 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( 1 - ( ( psi ` y ) + 1 ) ) e. RR )
46 0red 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> 0 e. RR )
47 25 3ad2ant1 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( psi ` x ) / x ) e. RR )
48 chpge0 
 |-  ( y e. RR -> 0 <_ ( psi ` y ) )
49 48 3ad2ant2 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> 0 <_ ( psi ` y ) )
50 36 3ad2ant2 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( psi ` y ) e. RR )
51 addge02 
 |-  ( ( 1 e. RR /\ ( psi ` y ) e. RR ) -> ( 0 <_ ( psi ` y ) <-> 1 <_ ( ( psi ` y ) + 1 ) ) )
52 42 50 51 sylancr 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( 0 <_ ( psi ` y ) <-> 1 <_ ( ( psi ` y ) + 1 ) ) )
53 49 52 mpbid 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> 1 <_ ( ( psi ` y ) + 1 ) )
54 suble0 
 |-  ( ( 1 e. RR /\ ( ( psi ` y ) + 1 ) e. RR ) -> ( ( 1 - ( ( psi ` y ) + 1 ) ) <_ 0 <-> 1 <_ ( ( psi ` y ) + 1 ) ) )
55 42 43 54 sylancr 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( 1 - ( ( psi ` y ) + 1 ) ) <_ 0 <-> 1 <_ ( ( psi ` y ) + 1 ) ) )
56 53 55 mpbird 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( 1 - ( ( psi ` y ) + 1 ) ) <_ 0 )
57 8 3ad2ant1 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( psi ` x ) e. RR )
58 6 3ad2ant1 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> x e. RR )
59 chpge0 
 |-  ( x e. RR -> 0 <_ ( psi ` x ) )
60 58 59 syl 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> 0 <_ ( psi ` x ) )
61 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
62 61 3ad2ant1 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( x e. RR /\ 0 < x ) )
63 divge0 
 |-  ( ( ( ( psi ` x ) e. RR /\ 0 <_ ( psi ` x ) ) /\ ( x e. RR /\ 0 < x ) ) -> 0 <_ ( ( psi ` x ) / x ) )
64 57 60 62 63 syl21anc 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> 0 <_ ( ( psi ` x ) / x ) )
65 45 46 47 56 64 letrd 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( 1 - ( ( psi ` y ) + 1 ) ) <_ ( ( psi ` x ) / x ) )
66 2re 
 |-  2 e. RR
67 readdcl 
 |-  ( ( ( psi ` y ) e. RR /\ 2 e. RR ) -> ( ( psi ` y ) + 2 ) e. RR )
68 50 66 67 sylancl 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( psi ` y ) + 2 ) e. RR )
69 1red 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> 1 e. RR )
70 58 adantr 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> x e. RR )
71 1red 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> 1 e. RR )
72 66 a1i 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> 2 e. RR )
73 simpr 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> x <_ 1 )
74 1lt2 
 |-  1 < 2
75 74 a1i 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> 1 < 2 )
76 70 71 72 73 75 lelttrd 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> x < 2 )
77 chpeq0 
 |-  ( x e. RR -> ( ( psi ` x ) = 0 <-> x < 2 ) )
78 70 77 syl 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> ( ( psi ` x ) = 0 <-> x < 2 ) )
79 76 78 mpbird 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> ( psi ` x ) = 0 )
80 79 oveq1d 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> ( ( psi ` x ) / x ) = ( 0 / x ) )
81 simp1 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> x e. RR+ )
82 81 rpcnne0d 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( x e. CC /\ x =/= 0 ) )
83 div0 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( 0 / x ) = 0 )
84 82 83 syl 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( 0 / x ) = 0 )
85 84 49 eqbrtrd 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( 0 / x ) <_ ( psi ` y ) )
86 85 adantr 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> ( 0 / x ) <_ ( psi ` y ) )
87 80 86 eqbrtrd 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ x <_ 1 ) -> ( ( psi ` x ) / x ) <_ ( psi ` y ) )
88 47 adantr 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ 1 <_ x ) -> ( ( psi ` x ) / x ) e. RR )
89 57 adantr 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ 1 <_ x ) -> ( psi ` x ) e. RR )
90 50 adantr 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ 1 <_ x ) -> ( psi ` y ) e. RR )
91 0lt1 
 |-  0 < 1
92 91 a1i 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> 0 < 1 )
93 lediv2a 
 |-  ( ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( x e. RR /\ 0 < x ) /\ ( ( psi ` x ) e. RR /\ 0 <_ ( psi ` x ) ) ) /\ 1 <_ x ) -> ( ( psi ` x ) / x ) <_ ( ( psi ` x ) / 1 ) )
94 93 ex 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( x e. RR /\ 0 < x ) /\ ( ( psi ` x ) e. RR /\ 0 <_ ( psi ` x ) ) ) -> ( 1 <_ x -> ( ( psi ` x ) / x ) <_ ( ( psi ` x ) / 1 ) ) )
95 69 92 62 57 60 94 syl212anc 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( 1 <_ x -> ( ( psi ` x ) / x ) <_ ( ( psi ` x ) / 1 ) ) )
96 95 imp 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ 1 <_ x ) -> ( ( psi ` x ) / x ) <_ ( ( psi ` x ) / 1 ) )
97 89 recnd 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ 1 <_ x ) -> ( psi ` x ) e. CC )
98 97 div1d 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ 1 <_ x ) -> ( ( psi ` x ) / 1 ) = ( psi ` x ) )
99 96 98 breqtrd 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ 1 <_ x ) -> ( ( psi ` x ) / x ) <_ ( psi ` x ) )
100 simp2 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> y e. RR )
101 ltle 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x < y -> x <_ y ) )
102 6 101 sylan 
 |-  ( ( x e. RR+ /\ y e. RR ) -> ( x < y -> x <_ y ) )
103 102 3impia 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> x <_ y )
104 chpwordi 
 |-  ( ( x e. RR /\ y e. RR /\ x <_ y ) -> ( psi ` x ) <_ ( psi ` y ) )
105 58 100 103 104 syl3anc 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( psi ` x ) <_ ( psi ` y ) )
106 105 adantr 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ 1 <_ x ) -> ( psi ` x ) <_ ( psi ` y ) )
107 88 89 90 99 106 letrd 
 |-  ( ( ( x e. RR+ /\ y e. RR /\ x < y ) /\ 1 <_ x ) -> ( ( psi ` x ) / x ) <_ ( psi ` y ) )
108 58 69 87 107 lecasei 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( psi ` x ) / x ) <_ ( psi ` y ) )
109 2nn0 
 |-  2 e. NN0
110 nn0addge1 
 |-  ( ( ( psi ` y ) e. RR /\ 2 e. NN0 ) -> ( psi ` y ) <_ ( ( psi ` y ) + 2 ) )
111 50 109 110 sylancl 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( psi ` y ) <_ ( ( psi ` y ) + 2 ) )
112 47 50 68 108 111 letrd 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( psi ` x ) / x ) <_ ( ( psi ` y ) + 2 ) )
113 df-2 
 |-  2 = ( 1 + 1 )
114 113 oveq2i 
 |-  ( ( psi ` y ) + 2 ) = ( ( psi ` y ) + ( 1 + 1 ) )
115 50 recnd 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( psi ` y ) e. CC )
116 30 a1i 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> 1 e. CC )
117 115 116 116 add12d 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( psi ` y ) + ( 1 + 1 ) ) = ( 1 + ( ( psi ` y ) + 1 ) ) )
118 114 117 syl5eq 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( psi ` y ) + 2 ) = ( 1 + ( ( psi ` y ) + 1 ) ) )
119 112 118 breqtrd 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( psi ` x ) / x ) <_ ( 1 + ( ( psi ` y ) + 1 ) ) )
120 47 69 43 absdifled 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) <_ ( ( psi ` y ) + 1 ) <-> ( ( 1 - ( ( psi ` y ) + 1 ) ) <_ ( ( psi ` x ) / x ) /\ ( ( psi ` x ) / x ) <_ ( 1 + ( ( psi ` y ) + 1 ) ) ) ) )
121 65 119 120 mpbir2and 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( abs ` ( ( ( psi ` x ) / x ) - 1 ) ) <_ ( ( psi ` y ) + 1 ) )
122 41 121 eqbrtrd 
 |-  ( ( x e. RR+ /\ y e. RR /\ x < y ) -> ( abs ` ( ( R ` x ) / x ) ) <_ ( ( psi ` y ) + 1 ) )
123 122 3expb 
 |-  ( ( x e. RR+ /\ ( y e. RR /\ x < y ) ) -> ( abs ` ( ( R ` x ) / x ) ) <_ ( ( psi ` y ) + 1 ) )
124 123 adantrlr 
 |-  ( ( x e. RR+ /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( ( R ` x ) / x ) ) <_ ( ( psi ` y ) + 1 ) )
125 124 adantll 
 |-  ( ( ( T. /\ x e. RR+ ) /\ ( ( y e. RR /\ 1 <_ y ) /\ x < y ) ) -> ( abs ` ( ( R ` x ) / x ) ) <_ ( ( psi ` y ) + 1 ) )
126 3 4 14 35 39 125 o1bddrp 
 |-  ( T. -> E. c e. RR+ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ c )
127 126 mptru 
 |-  E. c e. RR+ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ c