Metamath Proof Explorer

Theorem pntibndlem3

Description: Lemma for pntibnd . Package up pntibndlem2 in quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016)

Ref Expression
Hypotheses pntibnd.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntibndlem1.1 
|- ( ph -> A e. RR+ )
pntibndlem1.l 
|- L = ( ( 1 / 4 ) / ( A + 3 ) )
pntibndlem3.2 
|- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
pntibndlem3.3 
|- ( ph -> B e. RR+ )
pntibndlem3.k 
|- K = ( exp ` ( B / ( E / 2 ) ) )
pntibndlem3.c 
|- C = ( ( 2 x. B ) + ( log ` 2 ) )
pntibndlem3.4 
|- ( ph -> E e. ( 0 (,) 1 ) )
pntibndlem3.6 
|- ( ph -> Z e. RR+ )
pntibndlem3.5 
|- ( ph -> A. m e. ( K [,) +oo ) A. v e. ( Z (,) +oo ) E. i e. NN ( ( v < i /\ i <_ ( m x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) )
Assertion pntibndlem3 
|- ( ph -> E. x e. RR+ A. k e. ( ( exp ` ( C / E ) ) [,) +oo ) A. y e. ( x (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) )

Proof

Step Hyp Ref Expression
1 pntibnd.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntibndlem1.1 
 |-  ( ph -> A e. RR+ )
3 pntibndlem1.l 
 |-  L = ( ( 1 / 4 ) / ( A + 3 ) )
4 pntibndlem3.2 
 |-  ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
5 pntibndlem3.3 
 |-  ( ph -> B e. RR+ )
6 pntibndlem3.k 
 |-  K = ( exp ` ( B / ( E / 2 ) ) )
7 pntibndlem3.c 
 |-  C = ( ( 2 x. B ) + ( log ` 2 ) )
8 pntibndlem3.4 
 |-  ( ph -> E e. ( 0 (,) 1 ) )
9 pntibndlem3.6 
 |-  ( ph -> Z e. RR+ )
10 pntibndlem3.5 
 |-  ( ph -> A. m e. ( K [,) +oo ) A. v e. ( Z (,) +oo ) E. i e. NN ( ( v < i /\ i <_ ( m x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) )
11 2re 
 |-  2 e. RR
12 1le2 
 |-  1 <_ 2
13 chpdifbnd 
 |-  ( ( 2 e. RR /\ 1 <_ 2 ) -> E. t e. RR+ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) )
14 11 12 13 mp2an 
 |-  E. t e. RR+ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) )
15 simpr 
 |-  ( ( ph /\ t e. RR+ ) -> t e. RR+ )
16 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
17 16 8 sselid 
 |-  ( ph -> E e. RR )
18 eliooord 
 |-  ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) )
19 8 18 syl 
 |-  ( ph -> ( 0 < E /\ E < 1 ) )
20 19 simpld 
 |-  ( ph -> 0 < E )
21 17 20 elrpd 
 |-  ( ph -> E e. RR+ )
22 21 adantr 
 |-  ( ( ph /\ t e. RR+ ) -> E e. RR+ )
23 4nn 
 |-  4 e. NN
24 nnrp 
 |-  ( 4 e. NN -> 4 e. RR+ )
25 23 24 ax-mp 
 |-  4 e. RR+
26 rpdivcl 
 |-  ( ( E e. RR+ /\ 4 e. RR+ ) -> ( E / 4 ) e. RR+ )
27 22 25 26 sylancl 
 |-  ( ( ph /\ t e. RR+ ) -> ( E / 4 ) e. RR+ )
28 15 27 rpdivcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( t / ( E / 4 ) ) e. RR+ )
29 28 rpred 
 |-  ( ( ph /\ t e. RR+ ) -> ( t / ( E / 4 ) ) e. RR )
30 29 rpefcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( exp ` ( t / ( E / 4 ) ) ) e. RR+ )
31 9 adantr 
 |-  ( ( ph /\ t e. RR+ ) -> Z e. RR+ )
32 30 31 rpaddcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) e. RR+ )
33 32 adantrr 
 |-  ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) -> ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) e. RR+ )
34 breq2 
 |-  ( i = n -> ( v < i <-> v < n ) )
35 breq1 
 |-  ( i = n -> ( i <_ ( ( k / 2 ) x. v ) <-> n <_ ( ( k / 2 ) x. v ) ) )
36 34 35 anbi12d 
 |-  ( i = n -> ( ( v < i /\ i <_ ( ( k / 2 ) x. v ) ) <-> ( v < n /\ n <_ ( ( k / 2 ) x. v ) ) ) )
37 fveq2 
 |-  ( i = n -> ( R ` i ) = ( R ` n ) )
38 id 
 |-  ( i = n -> i = n )
39 37 38 oveq12d 
 |-  ( i = n -> ( ( R ` i ) / i ) = ( ( R ` n ) / n ) )
40 39 fveq2d 
 |-  ( i = n -> ( abs ` ( ( R ` i ) / i ) ) = ( abs ` ( ( R ` n ) / n ) ) )
41 40 breq1d 
 |-  ( i = n -> ( ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) <-> ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) )
42 36 41 anbi12d 
 |-  ( i = n -> ( ( ( v < i /\ i <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) <-> ( ( v < n /\ n <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) )
43 42 cbvrexvw 
 |-  ( E. i e. NN ( ( v < i /\ i <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) <-> E. n e. NN ( ( v < n /\ n <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) )
44 breq1 
 |-  ( v = y -> ( v < n <-> y < n ) )
45 oveq2 
 |-  ( v = y -> ( ( k / 2 ) x. v ) = ( ( k / 2 ) x. y ) )
46 45 breq2d 
 |-  ( v = y -> ( n <_ ( ( k / 2 ) x. v ) <-> n <_ ( ( k / 2 ) x. y ) ) )
47 44 46 anbi12d 
 |-  ( v = y -> ( ( v < n /\ n <_ ( ( k / 2 ) x. v ) ) <-> ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) ) )
48 47 anbi1d 
 |-  ( v = y -> ( ( ( v < n /\ n <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) <-> ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) )
49 48 rexbidv 
 |-  ( v = y -> ( E. n e. NN ( ( v < n /\ n <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) <-> E. n e. NN ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) )
50 43 49 syl5bb 
 |-  ( v = y -> ( E. i e. NN ( ( v < i /\ i <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) <-> E. n e. NN ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) )
51 oveq1 
 |-  ( m = ( k / 2 ) -> ( m x. v ) = ( ( k / 2 ) x. v ) )
52 51 breq2d 
 |-  ( m = ( k / 2 ) -> ( i <_ ( m x. v ) <-> i <_ ( ( k / 2 ) x. v ) ) )
53 52 anbi2d 
 |-  ( m = ( k / 2 ) -> ( ( v < i /\ i <_ ( m x. v ) ) <-> ( v < i /\ i <_ ( ( k / 2 ) x. v ) ) ) )
54 53 anbi1d 
 |-  ( m = ( k / 2 ) -> ( ( ( v < i /\ i <_ ( m x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) <-> ( ( v < i /\ i <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) ) )
55 54 rexbidv 
 |-  ( m = ( k / 2 ) -> ( E. i e. NN ( ( v < i /\ i <_ ( m x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) <-> E. i e. NN ( ( v < i /\ i <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) ) )
56 55 ralbidv 
 |-  ( m = ( k / 2 ) -> ( A. v e. ( Z (,) +oo ) E. i e. NN ( ( v < i /\ i <_ ( m x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) <-> A. v e. ( Z (,) +oo ) E. i e. NN ( ( v < i /\ i <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) ) )
57 10 ad2antrr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> A. m e. ( K [,) +oo ) A. v e. ( Z (,) +oo ) E. i e. NN ( ( v < i /\ i <_ ( m x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) )
58 5 adantr 
 |-  ( ( ph /\ t e. RR+ ) -> B e. RR+ )
59 58 rpred 
 |-  ( ( ph /\ t e. RR+ ) -> B e. RR )
60 remulcl 
 |-  ( ( 2 e. RR /\ B e. RR ) -> ( 2 x. B ) e. RR )
61 11 59 60 sylancr 
 |-  ( ( ph /\ t e. RR+ ) -> ( 2 x. B ) e. RR )
62 2rp 
 |-  2 e. RR+
63 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
64 62 63 ax-mp 
 |-  ( log ` 2 ) e. RR
65 readdcl 
 |-  ( ( ( 2 x. B ) e. RR /\ ( log ` 2 ) e. RR ) -> ( ( 2 x. B ) + ( log ` 2 ) ) e. RR )
66 61 64 65 sylancl 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( 2 x. B ) + ( log ` 2 ) ) e. RR )
67 7 66 eqeltrid 
 |-  ( ( ph /\ t e. RR+ ) -> C e. RR )
68 67 22 rerpdivcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( C / E ) e. RR )
69 68 reefcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( exp ` ( C / E ) ) e. RR )
70 elicopnf 
 |-  ( ( exp ` ( C / E ) ) e. RR -> ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) <-> ( k e. RR /\ ( exp ` ( C / E ) ) <_ k ) ) )
71 69 70 syl 
 |-  ( ( ph /\ t e. RR+ ) -> ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) <-> ( k e. RR /\ ( exp ` ( C / E ) ) <_ k ) ) )
72 71 simprbda 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> k e. RR )
73 72 rehalfcld 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( k / 2 ) e. RR )
74 22 rphalfcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( E / 2 ) e. RR+ )
75 59 74 rerpdivcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( B / ( E / 2 ) ) e. RR )
76 75 reefcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( exp ` ( B / ( E / 2 ) ) ) e. RR )
77 remulcl 
 |-  ( ( ( exp ` ( B / ( E / 2 ) ) ) e. RR /\ 2 e. RR ) -> ( ( exp ` ( B / ( E / 2 ) ) ) x. 2 ) e. RR )
78 76 11 77 sylancl 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( exp ` ( B / ( E / 2 ) ) ) x. 2 ) e. RR )
79 78 adantr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( ( exp ` ( B / ( E / 2 ) ) ) x. 2 ) e. RR )
80 69 adantr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( exp ` ( C / E ) ) e. RR )
81 75 recnd 
 |-  ( ( ph /\ t e. RR+ ) -> ( B / ( E / 2 ) ) e. CC )
82 64 recni 
 |-  ( log ` 2 ) e. CC
83 efadd 
 |-  ( ( ( B / ( E / 2 ) ) e. CC /\ ( log ` 2 ) e. CC ) -> ( exp ` ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) ) = ( ( exp ` ( B / ( E / 2 ) ) ) x. ( exp ` ( log ` 2 ) ) ) )
84 81 82 83 sylancl 
 |-  ( ( ph /\ t e. RR+ ) -> ( exp ` ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) ) = ( ( exp ` ( B / ( E / 2 ) ) ) x. ( exp ` ( log ` 2 ) ) ) )
85 reeflog 
 |-  ( 2 e. RR+ -> ( exp ` ( log ` 2 ) ) = 2 )
86 62 85 ax-mp 
 |-  ( exp ` ( log ` 2 ) ) = 2
87 86 oveq2i 
 |-  ( ( exp ` ( B / ( E / 2 ) ) ) x. ( exp ` ( log ` 2 ) ) ) = ( ( exp ` ( B / ( E / 2 ) ) ) x. 2 )
88 84 87 eqtrdi 
 |-  ( ( ph /\ t e. RR+ ) -> ( exp ` ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) ) = ( ( exp ` ( B / ( E / 2 ) ) ) x. 2 ) )
89 64 a1i 
 |-  ( ( ph /\ t e. RR+ ) -> ( log ` 2 ) e. RR )
90 rerpdivcl 
 |-  ( ( ( log ` 2 ) e. RR /\ E e. RR+ ) -> ( ( log ` 2 ) / E ) e. RR )
91 64 22 90 sylancr 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( log ` 2 ) / E ) e. RR )
92 82 div1i 
 |-  ( ( log ` 2 ) / 1 ) = ( log ` 2 )
93 19 simprd 
 |-  ( ph -> E < 1 )
94 93 adantr 
 |-  ( ( ph /\ t e. RR+ ) -> E < 1 )
95 17 adantr 
 |-  ( ( ph /\ t e. RR+ ) -> E e. RR )
96 1re 
 |-  1 e. RR
97 ltle 
 |-  ( ( E e. RR /\ 1 e. RR ) -> ( E < 1 -> E <_ 1 ) )
98 95 96 97 sylancl 
 |-  ( ( ph /\ t e. RR+ ) -> ( E < 1 -> E <_ 1 ) )
99 94 98 mpd 
 |-  ( ( ph /\ t e. RR+ ) -> E <_ 1 )
100 22 rpregt0d 
 |-  ( ( ph /\ t e. RR+ ) -> ( E e. RR /\ 0 < E ) )
101 1rp 
 |-  1 e. RR+
102 rpregt0 
 |-  ( 1 e. RR+ -> ( 1 e. RR /\ 0 < 1 ) )
103 101 102 mp1i 
 |-  ( ( ph /\ t e. RR+ ) -> ( 1 e. RR /\ 0 < 1 ) )
104 1lt2 
 |-  1 < 2
105 rplogcl 
 |-  ( ( 2 e. RR /\ 1 < 2 ) -> ( log ` 2 ) e. RR+ )
106 11 104 105 mp2an 
 |-  ( log ` 2 ) e. RR+
107 rpregt0 
 |-  ( ( log ` 2 ) e. RR+ -> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
108 106 107 mp1i 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
109 lediv2 
 |-  ( ( ( E e. RR /\ 0 < E ) /\ ( 1 e. RR /\ 0 < 1 ) /\ ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) ) -> ( E <_ 1 <-> ( ( log ` 2 ) / 1 ) <_ ( ( log ` 2 ) / E ) ) )
110 100 103 108 109 syl3anc 
 |-  ( ( ph /\ t e. RR+ ) -> ( E <_ 1 <-> ( ( log ` 2 ) / 1 ) <_ ( ( log ` 2 ) / E ) ) )
111 99 110 mpbid 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( log ` 2 ) / 1 ) <_ ( ( log ` 2 ) / E ) )
112 92 111 eqbrtrrid 
 |-  ( ( ph /\ t e. RR+ ) -> ( log ` 2 ) <_ ( ( log ` 2 ) / E ) )
113 89 91 75 112 leadd2dd 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) <_ ( ( B / ( E / 2 ) ) + ( ( log ` 2 ) / E ) ) )
114 7 oveq1i 
 |-  ( C / E ) = ( ( ( 2 x. B ) + ( log ` 2 ) ) / E )
115 61 recnd 
 |-  ( ( ph /\ t e. RR+ ) -> ( 2 x. B ) e. CC )
116 82 a1i 
 |-  ( ( ph /\ t e. RR+ ) -> ( log ` 2 ) e. CC )
117 rpcnne0 
 |-  ( E e. RR+ -> ( E e. CC /\ E =/= 0 ) )
118 22 117 syl 
 |-  ( ( ph /\ t e. RR+ ) -> ( E e. CC /\ E =/= 0 ) )
119 divdir 
 |-  ( ( ( 2 x. B ) e. CC /\ ( log ` 2 ) e. CC /\ ( E e. CC /\ E =/= 0 ) ) -> ( ( ( 2 x. B ) + ( log ` 2 ) ) / E ) = ( ( ( 2 x. B ) / E ) + ( ( log ` 2 ) / E ) ) )
120 115 116 118 119 syl3anc 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( ( 2 x. B ) + ( log ` 2 ) ) / E ) = ( ( ( 2 x. B ) / E ) + ( ( log ` 2 ) / E ) ) )
121 114 120 syl5eq 
 |-  ( ( ph /\ t e. RR+ ) -> ( C / E ) = ( ( ( 2 x. B ) / E ) + ( ( log ` 2 ) / E ) ) )
122 11 recni 
 |-  2 e. CC
123 59 recnd 
 |-  ( ( ph /\ t e. RR+ ) -> B e. CC )
124 mulcom 
 |-  ( ( 2 e. CC /\ B e. CC ) -> ( 2 x. B ) = ( B x. 2 ) )
125 122 123 124 sylancr 
 |-  ( ( ph /\ t e. RR+ ) -> ( 2 x. B ) = ( B x. 2 ) )
126 125 oveq1d 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( 2 x. B ) / E ) = ( ( B x. 2 ) / E ) )
127 rpcnne0 
 |-  ( 2 e. RR+ -> ( 2 e. CC /\ 2 =/= 0 ) )
128 62 127 mp1i 
 |-  ( ( ph /\ t e. RR+ ) -> ( 2 e. CC /\ 2 =/= 0 ) )
129 divdiv2 
 |-  ( ( B e. CC /\ ( E e. CC /\ E =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( B / ( E / 2 ) ) = ( ( B x. 2 ) / E ) )
130 123 118 128 129 syl3anc 
 |-  ( ( ph /\ t e. RR+ ) -> ( B / ( E / 2 ) ) = ( ( B x. 2 ) / E ) )
131 126 130 eqtr4d 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( 2 x. B ) / E ) = ( B / ( E / 2 ) ) )
132 131 oveq1d 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( ( 2 x. B ) / E ) + ( ( log ` 2 ) / E ) ) = ( ( B / ( E / 2 ) ) + ( ( log ` 2 ) / E ) ) )
133 121 132 eqtrd 
 |-  ( ( ph /\ t e. RR+ ) -> ( C / E ) = ( ( B / ( E / 2 ) ) + ( ( log ` 2 ) / E ) ) )
134 113 133 breqtrrd 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) <_ ( C / E ) )
135 readdcl 
 |-  ( ( ( B / ( E / 2 ) ) e. RR /\ ( log ` 2 ) e. RR ) -> ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) e. RR )
136 75 64 135 sylancl 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) e. RR )
137 efle 
 |-  ( ( ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) e. RR /\ ( C / E ) e. RR ) -> ( ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) <_ ( C / E ) <-> ( exp ` ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) ) <_ ( exp ` ( C / E ) ) ) )
138 136 68 137 syl2anc 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) <_ ( C / E ) <-> ( exp ` ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) ) <_ ( exp ` ( C / E ) ) ) )
139 134 138 mpbid 
 |-  ( ( ph /\ t e. RR+ ) -> ( exp ` ( ( B / ( E / 2 ) ) + ( log ` 2 ) ) ) <_ ( exp ` ( C / E ) ) )
140 88 139 eqbrtrrd 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( exp ` ( B / ( E / 2 ) ) ) x. 2 ) <_ ( exp ` ( C / E ) ) )
141 140 adantr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( ( exp ` ( B / ( E / 2 ) ) ) x. 2 ) <_ ( exp ` ( C / E ) ) )
142 71 simplbda 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( exp ` ( C / E ) ) <_ k )
143 79 80 72 141 142 letrd 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( ( exp ` ( B / ( E / 2 ) ) ) x. 2 ) <_ k )
144 76 adantr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( exp ` ( B / ( E / 2 ) ) ) e. RR )
145 rpregt0 
 |-  ( 2 e. RR+ -> ( 2 e. RR /\ 0 < 2 ) )
146 62 145 mp1i 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( 2 e. RR /\ 0 < 2 ) )
147 lemuldiv 
 |-  ( ( ( exp ` ( B / ( E / 2 ) ) ) e. RR /\ k e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( exp ` ( B / ( E / 2 ) ) ) x. 2 ) <_ k <-> ( exp ` ( B / ( E / 2 ) ) ) <_ ( k / 2 ) ) )
148 144 72 146 147 syl3anc 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( ( ( exp ` ( B / ( E / 2 ) ) ) x. 2 ) <_ k <-> ( exp ` ( B / ( E / 2 ) ) ) <_ ( k / 2 ) ) )
149 143 148 mpbid 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( exp ` ( B / ( E / 2 ) ) ) <_ ( k / 2 ) )
150 6 149 eqbrtrid 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> K <_ ( k / 2 ) )
151 6 144 eqeltrid 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> K e. RR )
152 elicopnf 
 |-  ( K e. RR -> ( ( k / 2 ) e. ( K [,) +oo ) <-> ( ( k / 2 ) e. RR /\ K <_ ( k / 2 ) ) ) )
153 151 152 syl 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( ( k / 2 ) e. ( K [,) +oo ) <-> ( ( k / 2 ) e. RR /\ K <_ ( k / 2 ) ) ) )
154 73 150 153 mpbir2and 
 |-  ( ( ( ph /\ t e. RR+ ) /\ k e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( k / 2 ) e. ( K [,) +oo ) )
155 154 adantrr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> ( k / 2 ) e. ( K [,) +oo ) )
156 155 adantlrr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> ( k / 2 ) e. ( K [,) +oo ) )
157 56 57 156 rspcdva 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> A. v e. ( Z (,) +oo ) E. i e. NN ( ( v < i /\ i <_ ( ( k / 2 ) x. v ) ) /\ ( abs ` ( ( R ` i ) / i ) ) <_ ( E / 2 ) ) )
158 elioore 
 |-  ( y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) -> y e. RR )
159 158 ad2antll 
 |-  ( ( ( ph /\ t e. RR+ ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> y e. RR )
160 31 rpred 
 |-  ( ( ph /\ t e. RR+ ) -> Z e. RR )
161 160 adantr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> Z e. RR )
162 29 reefcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( exp ` ( t / ( E / 4 ) ) ) e. RR )
163 162 160 readdcld 
 |-  ( ( ph /\ t e. RR+ ) -> ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) e. RR )
164 163 adantr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) e. RR )
165 160 30 ltaddrp2d 
 |-  ( ( ph /\ t e. RR+ ) -> Z < ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) )
166 165 adantr 
 |-  ( ( ( ph /\ t e. RR+ ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> Z < ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) )
167 eliooord 
 |-  ( y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) -> ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) < y /\ y < +oo ) )
168 167 simpld 
 |-  ( y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) -> ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) < y )
169 168 ad2antll 
 |-  ( ( ( ph /\ t e. RR+ ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) < y )
170 161 164 159 166 169 lttrd 
 |-  ( ( ( ph /\ t e. RR+ ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> Z < y )
171 161 rexrd 
 |-  ( ( ( ph /\ t e. RR+ ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> Z e. RR* )
172 elioopnf 
 |-  ( Z e. RR* -> ( y e. ( Z (,) +oo ) <-> ( y e. RR /\ Z < y ) ) )
173 171 172 syl 
 |-  ( ( ( ph /\ t e. RR+ ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> ( y e. ( Z (,) +oo ) <-> ( y e. RR /\ Z < y ) ) )
174 159 170 173 mpbir2and 
 |-  ( ( ( ph /\ t e. RR+ ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> y e. ( Z (,) +oo ) )
175 174 adantlrr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> y e. ( Z (,) +oo ) )
176 50 157 175 rspcdva 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) -> E. n e. NN ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) )
177 2 ad2antrr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> A e. RR+ )
178 fveq2 
 |-  ( x = v -> ( R ` x ) = ( R ` v ) )
179 id 
 |-  ( x = v -> x = v )
180 178 179 oveq12d 
 |-  ( x = v -> ( ( R ` x ) / x ) = ( ( R ` v ) / v ) )
181 180 fveq2d 
 |-  ( x = v -> ( abs ` ( ( R ` x ) / x ) ) = ( abs ` ( ( R ` v ) / v ) ) )
182 181 breq1d 
 |-  ( x = v -> ( ( abs ` ( ( R ` x ) / x ) ) <_ A <-> ( abs ` ( ( R ` v ) / v ) ) <_ A ) )
183 182 cbvralvw 
 |-  ( A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A <-> A. v e. RR+ ( abs ` ( ( R ` v ) / v ) ) <_ A )
184 4 183 sylib 
 |-  ( ph -> A. v e. RR+ ( abs ` ( ( R ` v ) / v ) ) <_ A )
185 184 ad2antrr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> A. v e. RR+ ( abs ` ( ( R ` v ) / v ) ) <_ A )
186 5 ad2antrr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> B e. RR+ )
187 8 ad2antrr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> E e. ( 0 (,) 1 ) )
188 9 ad2antrr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> Z e. RR+ )
189 simprrl 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> n e. NN )
190 simplrl 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> t e. RR+ )
191 simplrr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) )
192 eqid 
 |-  ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) = ( ( exp ` ( t / ( E / 4 ) ) ) + Z )
193 simprll 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> k e. ( ( exp ` ( C / E ) ) [,) +oo ) )
194 simprlr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) )
195 simprrr 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) )
196 1 177 3 185 186 6 7 187 188 189 190 191 192 193 194 195 pntibndlem2 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) ) -> 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 ` ( ( R ` u ) / u ) ) <_ E ) )
197 196 anassrs 
 |-  ( ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) ) ) /\ ( n e. NN /\ ( ( y < n /\ n <_ ( ( k / 2 ) x. y ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( E / 2 ) ) ) ) -> 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 ` ( ( R ` u ) / u ) ) <_ E ) )
198 176 197 rexlimddv 
 |-  ( ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) /\ ( k e. ( ( exp ` ( C / E ) ) [,) +oo ) /\ y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) )
199 198 ralrimivva 
 |-  ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) -> A. k e. ( ( exp ` ( C / E ) ) [,) +oo ) A. y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) )
200 oveq1 
 |-  ( x = ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) -> ( x (,) +oo ) = ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +oo ) )
201 200 raleqdv 
 |-  ( x = ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) -> ( A. y e. ( x (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) <-> A. y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) ) )
202 201 ralbidv 
 |-  ( x = ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) -> ( A. k e. ( ( exp ` ( C / E ) ) [,) +oo ) A. y e. ( x (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) <-> A. k e. ( ( exp ` ( C / E ) ) [,) +oo ) A. y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) ) )
203 202 rspcev 
 |-  ( ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) e. RR+ /\ A. k e. ( ( exp ` ( C / E ) ) [,) +oo ) A. y e. ( ( ( exp ` ( t / ( E / 4 ) ) ) + Z ) (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) ) -> E. x e. RR+ A. k e. ( ( exp ` ( C / E ) ) [,) +oo ) A. y e. ( x (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) )
204 33 199 203 syl2anc 
 |-  ( ( ph /\ ( t e. RR+ /\ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) ) ) -> E. x e. RR+ A. k e. ( ( exp ` ( C / E ) ) [,) +oo ) A. y e. ( x (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) )
205 204 rexlimdvaa 
 |-  ( ph -> ( E. t e. RR+ A. v e. ( 1 (,) +oo ) A. w e. ( v [,] ( 2 x. v ) ) ( ( psi ` w ) - ( psi ` v ) ) <_ ( ( 2 x. ( w - v ) ) + ( t x. ( v / ( log ` v ) ) ) ) -> E. x e. RR+ A. k e. ( ( exp ` ( C / E ) ) [,) +oo ) A. y e. ( x (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) ) )
206 14 205 mpi 
 |-  ( ph -> E. x e. RR+ A. k e. ( ( exp ` ( C / E ) ) [,) +oo ) A. y e. ( x (,) +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 ` ( ( R ` u ) / u ) ) <_ E ) )