Metamath Proof Explorer

Theorem pntibndlem2

Description: Lemma for pntibnd . The main work, after eliminating all the 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+ )
pntibndlem2.10 
|- ( ph -> N e. NN )
pntibndlem2.5 
|- ( ph -> T e. RR+ )
pntibndlem2.6 
|- ( ph -> A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( 2 x. x ) ) ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) )
pntibndlem2.7 
|- X = ( ( exp ` ( T / ( E / 4 ) ) ) + Z )
pntibndlem2.8 
|- ( ph -> M e. ( ( exp ` ( C / E ) ) [,) +oo ) )
pntibndlem2.9 
|- ( ph -> Y e. ( X (,) +oo ) )
pntibndlem2.11 
|- ( ph -> ( ( Y < N /\ N <_ ( ( M / 2 ) x. Y ) ) /\ ( abs ` ( ( R ` N ) / N ) ) <_ ( E / 2 ) ) )
Assertion pntibndlem2 
|- ( ph -> E. z e. RR+ ( ( Y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( M 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 pntibndlem2.10 
 |-  ( ph -> N e. NN )
11 pntibndlem2.5 
 |-  ( ph -> T e. RR+ )
12 pntibndlem2.6 
 |-  ( ph -> A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( 2 x. x ) ) ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) )
13 pntibndlem2.7 
 |-  X = ( ( exp ` ( T / ( E / 4 ) ) ) + Z )
14 pntibndlem2.8 
 |-  ( ph -> M e. ( ( exp ` ( C / E ) ) [,) +oo ) )
15 pntibndlem2.9 
 |-  ( ph -> Y e. ( X (,) +oo ) )
16 pntibndlem2.11 
 |-  ( ph -> ( ( Y < N /\ N <_ ( ( M / 2 ) x. Y ) ) /\ ( abs ` ( ( R ` N ) / N ) ) <_ ( E / 2 ) ) )
17 10 nnrpd 
 |-  ( ph -> N e. RR+ )
18 16 simpld 
 |-  ( ph -> ( Y < N /\ N <_ ( ( M / 2 ) x. Y ) ) )
19 18 simpld 
 |-  ( ph -> Y < N )
20 1red 
 |-  ( ph -> 1 e. RR )
21 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
22 1 2 3 pntibndlem1 
 |-  ( ph -> L e. ( 0 (,) 1 ) )
23 21 22 sselid 
 |-  ( ph -> L e. RR )
24 21 8 sselid 
 |-  ( ph -> E e. RR )
25 23 24 remulcld 
 |-  ( ph -> ( L x. E ) e. RR )
26 20 25 readdcld 
 |-  ( ph -> ( 1 + ( L x. E ) ) e. RR )
27 10 nnred 
 |-  ( ph -> N e. RR )
28 26 27 remulcld 
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. N ) e. RR )
29 2re 
 |-  2 e. RR
30 remulcl 
 |-  ( ( 2 e. RR /\ N e. RR ) -> ( 2 x. N ) e. RR )
31 29 27 30 sylancr 
 |-  ( ph -> ( 2 x. N ) e. RR )
32 5 rpred 
 |-  ( ph -> B e. RR )
33 remulcl 
 |-  ( ( 2 e. RR /\ B e. RR ) -> ( 2 x. B ) e. RR )
34 29 32 33 sylancr 
 |-  ( ph -> ( 2 x. B ) e. RR )
35 2rp 
 |-  2 e. RR+
36 35 a1i 
 |-  ( ph -> 2 e. RR+ )
37 36 relogcld 
 |-  ( ph -> ( log ` 2 ) e. RR )
38 34 37 readdcld 
 |-  ( ph -> ( ( 2 x. B ) + ( log ` 2 ) ) e. RR )
39 7 38 eqeltrid 
 |-  ( ph -> C e. RR )
40 eliooord 
 |-  ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) )
41 8 40 syl 
 |-  ( ph -> ( 0 < E /\ E < 1 ) )
42 41 simpld 
 |-  ( ph -> 0 < E )
43 24 42 elrpd 
 |-  ( ph -> E e. RR+ )
44 39 43 rerpdivcld 
 |-  ( ph -> ( C / E ) e. RR )
45 44 reefcld 
 |-  ( ph -> ( exp ` ( C / E ) ) e. RR )
46 pnfxr 
 |-  +oo e. RR*
47 icossre 
 |-  ( ( ( exp ` ( C / E ) ) e. RR /\ +oo e. RR* ) -> ( ( exp ` ( C / E ) ) [,) +oo ) C_ RR )
48 45 46 47 sylancl 
 |-  ( ph -> ( ( exp ` ( C / E ) ) [,) +oo ) C_ RR )
49 48 14 sseldd 
 |-  ( ph -> M e. RR )
50 ioossre 
 |-  ( X (,) +oo ) C_ RR
51 50 15 sselid 
 |-  ( ph -> Y e. RR )
52 49 51 remulcld 
 |-  ( ph -> ( M x. Y ) e. RR )
53 29 a1i 
 |-  ( ph -> 2 e. RR )
54 eliooord 
 |-  ( L e. ( 0 (,) 1 ) -> ( 0 < L /\ L < 1 ) )
55 22 54 syl 
 |-  ( ph -> ( 0 < L /\ L < 1 ) )
56 55 simpld 
 |-  ( ph -> 0 < L )
57 23 56 elrpd 
 |-  ( ph -> L e. RR+ )
58 57 rpge0d 
 |-  ( ph -> 0 <_ L )
59 55 simprd 
 |-  ( ph -> L < 1 )
60 43 rpge0d 
 |-  ( ph -> 0 <_ E )
61 41 simprd 
 |-  ( ph -> E < 1 )
62 23 20 24 20 58 59 60 61 ltmul12ad 
 |-  ( ph -> ( L x. E ) < ( 1 x. 1 ) )
63 1t1e1 
 |-  ( 1 x. 1 ) = 1
64 62 63 breqtrdi 
 |-  ( ph -> ( L x. E ) < 1 )
65 25 20 20 64 ltadd2dd 
 |-  ( ph -> ( 1 + ( L x. E ) ) < ( 1 + 1 ) )
66 df-2 
 |-  2 = ( 1 + 1 )
67 65 66 breqtrrdi 
 |-  ( ph -> ( 1 + ( L x. E ) ) < 2 )
68 26 53 17 67 ltmul1dd 
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. N ) < ( 2 x. N ) )
69 18 simprd 
 |-  ( ph -> N <_ ( ( M / 2 ) x. Y ) )
70 49 recnd 
 |-  ( ph -> M e. CC )
71 51 recnd 
 |-  ( ph -> Y e. CC )
72 rpcnne0 
 |-  ( 2 e. RR+ -> ( 2 e. CC /\ 2 =/= 0 ) )
73 35 72 mp1i 
 |-  ( ph -> ( 2 e. CC /\ 2 =/= 0 ) )
74 div23 
 |-  ( ( M e. CC /\ Y e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( M x. Y ) / 2 ) = ( ( M / 2 ) x. Y ) )
75 70 71 73 74 syl3anc 
 |-  ( ph -> ( ( M x. Y ) / 2 ) = ( ( M / 2 ) x. Y ) )
76 69 75 breqtrrd 
 |-  ( ph -> N <_ ( ( M x. Y ) / 2 ) )
77 27 52 36 lemuldiv2d 
 |-  ( ph -> ( ( 2 x. N ) <_ ( M x. Y ) <-> N <_ ( ( M x. Y ) / 2 ) ) )
78 76 77 mpbird 
 |-  ( ph -> ( 2 x. N ) <_ ( M x. Y ) )
79 28 31 52 68 78 ltletrd 
 |-  ( ph -> ( ( 1 + ( L x. E ) ) x. N ) < ( M x. Y ) )
80 1 2 3 4 5 6 7 8 2 10 pntibndlem2a 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u e. RR /\ N <_ u /\ u <_ ( ( 1 + ( L x. E ) ) x. N ) ) )
81 80 simp1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u e. RR )
82 17 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N e. RR+ )
83 80 simp2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N <_ u )
84 81 82 83 rpgecld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u e. RR+ )
85 1 pntrf 
 |-  R : RR+ --> RR
86 85 ffvelcdmi 
 |-  ( u e. RR+ -> ( R ` u ) e. RR )
87 84 86 syl 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` u ) e. RR )
88 87 84 rerpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) / u ) e. RR )
89 88 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) / u ) e. CC )
90 89 abscld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) / u ) ) e. RR )
91 85 ffvelcdmi 
 |-  ( N e. RR+ -> ( R ` N ) e. RR )
92 17 91 syl 
 |-  ( ph -> ( R ` N ) e. RR )
93 92 10 nndivred 
 |-  ( ph -> ( ( R ` N ) / N ) e. RR )
94 93 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` N ) / N ) e. RR )
95 94 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` N ) / N ) e. CC )
96 89 95 subcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) e. CC )
97 96 abscld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) e. RR )
98 95 abscld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` N ) / N ) ) e. RR )
99 97 98 readdcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) + ( abs ` ( ( R ` N ) / N ) ) ) e. RR )
100 24 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> E e. RR )
101 89 95 abs2difd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) / u ) ) - ( abs ` ( ( R ` N ) / N ) ) ) <_ ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) )
102 90 98 97 lesubaddd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( abs ` ( ( R ` u ) / u ) ) - ( abs ` ( ( R ` N ) / N ) ) ) <_ ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) <-> ( abs ` ( ( R ` u ) / u ) ) <_ ( ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) + ( abs ` ( ( R ` N ) / N ) ) ) ) )
103 101 102 mpbid 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) / u ) ) <_ ( ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) + ( abs ` ( ( R ` N ) / N ) ) ) )
104 100 rehalfcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( E / 2 ) e. RR )
105 27 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N e. RR )
106 81 105 resubcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u - N ) e. RR )
107 106 82 rerpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) / N ) e. RR )
108 3re 
 |-  3 e. RR
109 108 a1i 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 3 e. RR )
110 90 109 readdcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) e. RR )
111 107 110 remulcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) e. RR )
112 11 rpred 
 |-  ( ph -> T e. RR )
113 112 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> T e. RR )
114 1red 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 1 e. RR )
115 4nn 
 |-  4 e. NN
116 nnrp 
 |-  ( 4 e. NN -> 4 e. RR+ )
117 115 116 mp1i 
 |-  ( ph -> 4 e. RR+ )
118 43 117 rpdivcld 
 |-  ( ph -> ( E / 4 ) e. RR+ )
119 11 118 rpdivcld 
 |-  ( ph -> ( T / ( E / 4 ) ) e. RR+ )
120 119 rpred 
 |-  ( ph -> ( T / ( E / 4 ) ) e. RR )
121 120 reefcld 
 |-  ( ph -> ( exp ` ( T / ( E / 4 ) ) ) e. RR )
122 121 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( exp ` ( T / ( E / 4 ) ) ) e. RR )
123 efgt1 
 |-  ( ( T / ( E / 4 ) ) e. RR+ -> 1 < ( exp ` ( T / ( E / 4 ) ) ) )
124 119 123 syl 
 |-  ( ph -> 1 < ( exp ` ( T / ( E / 4 ) ) ) )
125 124 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 1 < ( exp ` ( T / ( E / 4 ) ) ) )
126 9 rpred 
 |-  ( ph -> Z e. RR )
127 121 126 readdcld 
 |-  ( ph -> ( ( exp ` ( T / ( E / 4 ) ) ) + Z ) e. RR )
128 13 127 eqeltrid 
 |-  ( ph -> X e. RR )
129 121 9 ltaddrpd 
 |-  ( ph -> ( exp ` ( T / ( E / 4 ) ) ) < ( ( exp ` ( T / ( E / 4 ) ) ) + Z ) )
130 129 13 breqtrrdi 
 |-  ( ph -> ( exp ` ( T / ( E / 4 ) ) ) < X )
131 eliooord 
 |-  ( Y e. ( X (,) +oo ) -> ( X < Y /\ Y < +oo ) )
132 15 131 syl 
 |-  ( ph -> ( X < Y /\ Y < +oo ) )
133 132 simpld 
 |-  ( ph -> X < Y )
134 121 128 51 130 133 lttrd 
 |-  ( ph -> ( exp ` ( T / ( E / 4 ) ) ) < Y )
135 121 51 27 134 19 lttrd 
 |-  ( ph -> ( exp ` ( T / ( E / 4 ) ) ) < N )
136 135 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( exp ` ( T / ( E / 4 ) ) ) < N )
137 114 122 105 125 136 lttrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 1 < N )
138 105 137 rplogcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( log ` N ) e. RR+ )
139 113 138 rerpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( log ` N ) ) e. RR )
140 111 139 readdcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) e. RR )
141 peano2re 
 |-  ( ( abs ` ( ( R ` u ) / u ) ) e. RR -> ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) e. RR )
142 90 141 syl 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) e. RR )
143 107 142 remulcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) e. RR )
144 chpcl 
 |-  ( u e. RR -> ( psi ` u ) e. RR )
145 81 144 syl 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( psi ` u ) e. RR )
146 chpcl 
 |-  ( N e. RR -> ( psi ` N ) e. RR )
147 105 146 syl 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( psi ` N ) e. RR )
148 145 147 resubcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( psi ` u ) - ( psi ` N ) ) e. RR )
149 148 82 rerpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( psi ` u ) - ( psi ` N ) ) / N ) e. RR )
150 143 149 readdcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) e. RR )
151 107 90 remulcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) e. RR )
152 92 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` N ) e. RR )
153 87 152 resubcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) - ( R ` N ) ) e. RR )
154 153 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) - ( R ` N ) ) e. CC )
155 154 abscld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) - ( R ` N ) ) ) e. RR )
156 155 82 rerpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) e. RR )
157 151 156 readdcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) ) e. RR )
158 107 88 remulcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) e. RR )
159 158 renegcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) e. RR )
160 159 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) e. CC )
161 153 82 rerpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( R ` u ) - ( R ` N ) ) / N ) e. RR )
162 161 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( R ` u ) - ( R ` N ) ) / N ) e. CC )
163 160 162 abstrid 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) + ( ( ( R ` u ) - ( R ` N ) ) / N ) ) ) <_ ( ( abs ` -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) + ( abs ` ( ( ( R ` u ) - ( R ` N ) ) / N ) ) ) )
164 81 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u e. CC )
165 105 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N e. CC )
166 82 rpne0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N =/= 0 )
167 164 165 165 166 divsubdird 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) / N ) = ( ( u / N ) - ( N / N ) ) )
168 165 166 dividd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( N / N ) = 1 )
169 168 oveq2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u / N ) - ( N / N ) ) = ( ( u / N ) - 1 ) )
170 167 169 eqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) / N ) = ( ( u / N ) - 1 ) )
171 170 oveq1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) = ( ( ( u / N ) - 1 ) x. ( ( R ` u ) / u ) ) )
172 81 82 rerpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u / N ) e. RR )
173 172 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u / N ) e. CC )
174 1cnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 1 e. CC )
175 173 174 89 subdird 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u / N ) - 1 ) x. ( ( R ` u ) / u ) ) = ( ( ( u / N ) x. ( ( R ` u ) / u ) ) - ( 1 x. ( ( R ` u ) / u ) ) ) )
176 84 rpcnne0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u e. CC /\ u =/= 0 ) )
177 82 rpcnne0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( N e. CC /\ N =/= 0 ) )
178 87 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` u ) e. CC )
179 dmdcan 
 |-  ( ( ( u e. CC /\ u =/= 0 ) /\ ( N e. CC /\ N =/= 0 ) /\ ( R ` u ) e. CC ) -> ( ( u / N ) x. ( ( R ` u ) / u ) ) = ( ( R ` u ) / N ) )
180 176 177 178 179 syl3anc 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u / N ) x. ( ( R ` u ) / u ) ) = ( ( R ` u ) / N ) )
181 89 mullidd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 1 x. ( ( R ` u ) / u ) ) = ( ( R ` u ) / u ) )
182 180 181 oveq12d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u / N ) x. ( ( R ` u ) / u ) ) - ( 1 x. ( ( R ` u ) / u ) ) ) = ( ( ( R ` u ) / N ) - ( ( R ` u ) / u ) ) )
183 171 175 182 3eqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) = ( ( ( R ` u ) / N ) - ( ( R ` u ) / u ) ) )
184 183 negeqd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) = -u ( ( ( R ` u ) / N ) - ( ( R ` u ) / u ) ) )
185 87 82 rerpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) / N ) e. RR )
186 185 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) / N ) e. CC )
187 186 89 negsubdi2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> -u ( ( ( R ` u ) / N ) - ( ( R ` u ) / u ) ) = ( ( ( R ` u ) / u ) - ( ( R ` u ) / N ) ) )
188 184 187 eqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) = ( ( ( R ` u ) / u ) - ( ( R ` u ) / N ) ) )
189 152 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` N ) e. CC )
190 178 189 165 166 divsubdird 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( R ` u ) - ( R ` N ) ) / N ) = ( ( ( R ` u ) / N ) - ( ( R ` N ) / N ) ) )
191 188 190 oveq12d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) + ( ( ( R ` u ) - ( R ` N ) ) / N ) ) = ( ( ( ( R ` u ) / u ) - ( ( R ` u ) / N ) ) + ( ( ( R ` u ) / N ) - ( ( R ` N ) / N ) ) ) )
192 89 186 95 npncand 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( R ` u ) / u ) - ( ( R ` u ) / N ) ) + ( ( ( R ` u ) / N ) - ( ( R ` N ) / N ) ) ) = ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) )
193 191 192 eqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) + ( ( ( R ` u ) - ( R ` N ) ) / N ) ) = ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) )
194 193 fveq2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) + ( ( ( R ` u ) - ( R ` N ) ) / N ) ) ) = ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) )
195 158 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) e. CC )
196 195 absnegd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) = ( abs ` ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) )
197 107 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) / N ) e. CC )
198 197 89 absmuld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) = ( ( abs ` ( ( u - N ) / N ) ) x. ( abs ` ( ( R ` u ) / u ) ) ) )
199 81 105 subge0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 0 <_ ( u - N ) <-> N <_ u ) )
200 83 199 mpbird 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 0 <_ ( u - N ) )
201 106 82 200 divge0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 0 <_ ( ( u - N ) / N ) )
202 107 201 absidd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( u - N ) / N ) ) = ( ( u - N ) / N ) )
203 202 oveq1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( u - N ) / N ) ) x. ( abs ` ( ( R ` u ) / u ) ) ) = ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) )
204 196 198 203 3eqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) = ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) )
205 154 165 166 absdivd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) - ( R ` N ) ) / N ) ) = ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / ( abs ` N ) ) )
206 82 rprege0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( N e. RR /\ 0 <_ N ) )
207 absid 
 |-  ( ( N e. RR /\ 0 <_ N ) -> ( abs ` N ) = N )
208 206 207 syl 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` N ) = N )
209 208 oveq2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / ( abs ` N ) ) = ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) )
210 205 209 eqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) - ( R ` N ) ) / N ) ) = ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) )
211 204 210 oveq12d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` -u ( ( ( u - N ) / N ) x. ( ( R ` u ) / u ) ) ) + ( abs ` ( ( ( R ` u ) - ( R ` N ) ) / N ) ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) ) )
212 163 194 211 3brtr3d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) <_ ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) ) )
213 106 148 readdcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) + ( ( psi ` u ) - ( psi ` N ) ) ) e. RR )
214 213 82 rerpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) + ( ( psi ` u ) - ( psi ` N ) ) ) / N ) e. RR )
215 148 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( psi ` u ) - ( psi ` N ) ) e. CC )
216 165 164 subcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( N - u ) e. CC )
217 215 216 abstrid 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( psi ` u ) - ( psi ` N ) ) + ( N - u ) ) ) <_ ( ( abs ` ( ( psi ` u ) - ( psi ` N ) ) ) + ( abs ` ( N - u ) ) ) )
218 1 pntrval 
 |-  ( u e. RR+ -> ( R ` u ) = ( ( psi ` u ) - u ) )
219 84 218 syl 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` u ) = ( ( psi ` u ) - u ) )
220 1 pntrval 
 |-  ( N e. RR+ -> ( R ` N ) = ( ( psi ` N ) - N ) )
221 82 220 syl 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( R ` N ) = ( ( psi ` N ) - N ) )
222 219 221 oveq12d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( R ` u ) - ( R ` N ) ) = ( ( ( psi ` u ) - u ) - ( ( psi ` N ) - N ) ) )
223 145 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( psi ` u ) e. CC )
224 147 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( psi ` N ) e. CC )
225 subadd4 
 |-  ( ( ( ( psi ` u ) e. CC /\ ( psi ` N ) e. CC ) /\ ( u e. CC /\ N e. CC ) ) -> ( ( ( psi ` u ) - ( psi ` N ) ) - ( u - N ) ) = ( ( ( psi ` u ) + N ) - ( ( psi ` N ) + u ) ) )
226 sub4 
 |-  ( ( ( ( psi ` u ) e. CC /\ ( psi ` N ) e. CC ) /\ ( u e. CC /\ N e. CC ) ) -> ( ( ( psi ` u ) - ( psi ` N ) ) - ( u - N ) ) = ( ( ( psi ` u ) - u ) - ( ( psi ` N ) - N ) ) )
227 addsub4 
 |-  ( ( ( ( psi ` u ) e. CC /\ N e. CC ) /\ ( ( psi ` N ) e. CC /\ u e. CC ) ) -> ( ( ( psi ` u ) + N ) - ( ( psi ` N ) + u ) ) = ( ( ( psi ` u ) - ( psi ` N ) ) + ( N - u ) ) )
228 227 an42s 
 |-  ( ( ( ( psi ` u ) e. CC /\ ( psi ` N ) e. CC ) /\ ( u e. CC /\ N e. CC ) ) -> ( ( ( psi ` u ) + N ) - ( ( psi ` N ) + u ) ) = ( ( ( psi ` u ) - ( psi ` N ) ) + ( N - u ) ) )
229 225 226 228 3eqtr3d 
 |-  ( ( ( ( psi ` u ) e. CC /\ ( psi ` N ) e. CC ) /\ ( u e. CC /\ N e. CC ) ) -> ( ( ( psi ` u ) - u ) - ( ( psi ` N ) - N ) ) = ( ( ( psi ` u ) - ( psi ` N ) ) + ( N - u ) ) )
230 223 224 164 165 229 syl22anc 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( psi ` u ) - u ) - ( ( psi ` N ) - N ) ) = ( ( ( psi ` u ) - ( psi ` N ) ) + ( N - u ) ) )
231 222 230 eqtr2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( psi ` u ) - ( psi ` N ) ) + ( N - u ) ) = ( ( R ` u ) - ( R ` N ) ) )
232 231 fveq2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( psi ` u ) - ( psi ` N ) ) + ( N - u ) ) ) = ( abs ` ( ( R ` u ) - ( R ` N ) ) ) )
233 106 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u - N ) e. CC )
234 chpwordi 
 |-  ( ( N e. RR /\ u e. RR /\ N <_ u ) -> ( psi ` N ) <_ ( psi ` u ) )
235 105 81 83 234 syl3anc 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( psi ` N ) <_ ( psi ` u ) )
236 147 145 235 abssubge0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( psi ` u ) - ( psi ` N ) ) ) = ( ( psi ` u ) - ( psi ` N ) ) )
237 105 81 83 abssuble0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( N - u ) ) = ( u - N ) )
238 236 237 oveq12d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( psi ` u ) - ( psi ` N ) ) ) + ( abs ` ( N - u ) ) ) = ( ( ( psi ` u ) - ( psi ` N ) ) + ( u - N ) ) )
239 215 233 238 comraddd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( psi ` u ) - ( psi ` N ) ) ) + ( abs ` ( N - u ) ) ) = ( ( u - N ) + ( ( psi ` u ) - ( psi ` N ) ) ) )
240 217 232 239 3brtr3d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) - ( R ` N ) ) ) <_ ( ( u - N ) + ( ( psi ` u ) - ( psi ` N ) ) ) )
241 155 213 82 240 lediv1dd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) <_ ( ( ( u - N ) + ( ( psi ` u ) - ( psi ` N ) ) ) / N ) )
242 156 214 151 241 leadd2dd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) ) <_ ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) + ( ( psi ` u ) - ( psi ` N ) ) ) / N ) ) )
243 151 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) e. CC )
244 149 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( psi ` u ) - ( psi ` N ) ) / N ) e. CC )
245 243 197 244 addassd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( u - N ) / N ) ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) / N ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) ) )
246 90 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) / u ) ) e. CC )
247 197 246 174 adddid 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) / N ) x. 1 ) ) )
248 197 mulridd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. 1 ) = ( ( u - N ) / N ) )
249 248 oveq2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) / N ) x. 1 ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( u - N ) / N ) ) )
250 247 249 eqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( u - N ) / N ) ) )
251 250 oveq1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) = ( ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( u - N ) / N ) ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) )
252 233 215 165 166 divdird 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) + ( ( psi ` u ) - ( psi ` N ) ) ) / N ) = ( ( ( u - N ) / N ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) )
253 252 oveq2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) + ( ( psi ` u ) - ( psi ` N ) ) ) / N ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) / N ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) ) )
254 245 251 253 3eqtr4d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) = ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( ( u - N ) + ( ( psi ` u ) - ( psi ` N ) ) ) / N ) ) )
255 242 254 breqtrrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( abs ` ( ( R ` u ) / u ) ) ) + ( ( abs ` ( ( R ` u ) - ( R ` N ) ) ) / N ) ) <_ ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) )
256 97 157 150 212 255 letrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) <_ ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) )
257 remulcl 
 |-  ( ( 2 e. RR /\ ( ( u - N ) / N ) e. RR ) -> ( 2 x. ( ( u - N ) / N ) ) e. RR )
258 29 107 257 sylancr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. ( ( u - N ) / N ) ) e. RR )
259 258 139 readdcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) e. RR )
260 remulcl 
 |-  ( ( 2 e. RR /\ ( u - N ) e. RR ) -> ( 2 x. ( u - N ) ) e. RR )
261 29 106 260 sylancr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. ( u - N ) ) e. RR )
262 105 138 rerpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( N / ( log ` N ) ) e. RR )
263 113 262 remulcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T x. ( N / ( log ` N ) ) ) e. RR )
264 261 263 readdcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) e. RR )
265 fveq2 
 |-  ( y = u -> ( psi ` y ) = ( psi ` u ) )
266 265 oveq1d 
 |-  ( y = u -> ( ( psi ` y ) - ( psi ` N ) ) = ( ( psi ` u ) - ( psi ` N ) ) )
267 oveq1 
 |-  ( y = u -> ( y - N ) = ( u - N ) )
268 267 oveq2d 
 |-  ( y = u -> ( 2 x. ( y - N ) ) = ( 2 x. ( u - N ) ) )
269 268 oveq1d 
 |-  ( y = u -> ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) = ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) )
270 266 269 breq12d 
 |-  ( y = u -> ( ( ( psi ` y ) - ( psi ` N ) ) <_ ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) <-> ( ( psi ` u ) - ( psi ` N ) ) <_ ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) ) )
271 id 
 |-  ( x = N -> x = N )
272 oveq2 
 |-  ( x = N -> ( 2 x. x ) = ( 2 x. N ) )
273 271 272 oveq12d 
 |-  ( x = N -> ( x [,] ( 2 x. x ) ) = ( N [,] ( 2 x. N ) ) )
274 fveq2 
 |-  ( x = N -> ( psi ` x ) = ( psi ` N ) )
275 274 oveq2d 
 |-  ( x = N -> ( ( psi ` y ) - ( psi ` x ) ) = ( ( psi ` y ) - ( psi ` N ) ) )
276 oveq2 
 |-  ( x = N -> ( y - x ) = ( y - N ) )
277 276 oveq2d 
 |-  ( x = N -> ( 2 x. ( y - x ) ) = ( 2 x. ( y - N ) ) )
278 fveq2 
 |-  ( x = N -> ( log ` x ) = ( log ` N ) )
279 271 278 oveq12d 
 |-  ( x = N -> ( x / ( log ` x ) ) = ( N / ( log ` N ) ) )
280 279 oveq2d 
 |-  ( x = N -> ( T x. ( x / ( log ` x ) ) ) = ( T x. ( N / ( log ` N ) ) ) )
281 277 280 oveq12d 
 |-  ( x = N -> ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) = ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) )
282 275 281 breq12d 
 |-  ( x = N -> ( ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) <-> ( ( psi ` y ) - ( psi ` N ) ) <_ ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) ) )
283 273 282 raleqbidv 
 |-  ( x = N -> ( A. y e. ( x [,] ( 2 x. x ) ) ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) <-> A. y e. ( N [,] ( 2 x. N ) ) ( ( psi ` y ) - ( psi ` N ) ) <_ ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) ) )
284 12 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> A. x e. ( 1 (,) +oo ) A. y e. ( x [,] ( 2 x. x ) ) ( ( psi ` y ) - ( psi ` x ) ) <_ ( ( 2 x. ( y - x ) ) + ( T x. ( x / ( log ` x ) ) ) ) )
285 1xr 
 |-  1 e. RR*
286 elioopnf 
 |-  ( 1 e. RR* -> ( N e. ( 1 (,) +oo ) <-> ( N e. RR /\ 1 < N ) ) )
287 285 286 ax-mp 
 |-  ( N e. ( 1 (,) +oo ) <-> ( N e. RR /\ 1 < N ) )
288 105 137 287 sylanbrc 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> N e. ( 1 (,) +oo ) )
289 283 284 288 rspcdva 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> A. y e. ( N [,] ( 2 x. N ) ) ( ( psi ` y ) - ( psi ` N ) ) <_ ( ( 2 x. ( y - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) )
290 28 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 1 + ( L x. E ) ) x. N ) e. RR )
291 31 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. N ) e. RR )
292 80 simp3d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u <_ ( ( 1 + ( L x. E ) ) x. N ) )
293 ltle 
 |-  ( ( ( 1 + ( L x. E ) ) e. RR /\ 2 e. RR ) -> ( ( 1 + ( L x. E ) ) < 2 -> ( 1 + ( L x. E ) ) <_ 2 ) )
294 26 29 293 sylancl 
 |-  ( ph -> ( ( 1 + ( L x. E ) ) < 2 -> ( 1 + ( L x. E ) ) <_ 2 ) )
295 67 294 mpd 
 |-  ( ph -> ( 1 + ( L x. E ) ) <_ 2 )
296 295 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 1 + ( L x. E ) ) <_ 2 )
297 26 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 1 + ( L x. E ) ) e. RR )
298 29 a1i 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 2 e. RR )
299 297 298 82 lemul1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 1 + ( L x. E ) ) <_ 2 <-> ( ( 1 + ( L x. E ) ) x. N ) <_ ( 2 x. N ) ) )
300 296 299 mpbid 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 1 + ( L x. E ) ) x. N ) <_ ( 2 x. N ) )
301 81 290 291 292 300 letrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u <_ ( 2 x. N ) )
302 elicc2 
 |-  ( ( N e. RR /\ ( 2 x. N ) e. RR ) -> ( u e. ( N [,] ( 2 x. N ) ) <-> ( u e. RR /\ N <_ u /\ u <_ ( 2 x. N ) ) ) )
303 105 291 302 syl2anc 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u e. ( N [,] ( 2 x. N ) ) <-> ( u e. RR /\ N <_ u /\ u <_ ( 2 x. N ) ) ) )
304 81 83 301 303 mpbir3and 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> u e. ( N [,] ( 2 x. N ) ) )
305 270 289 304 rspcdva 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( psi ` u ) - ( psi ` N ) ) <_ ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) )
306 148 264 82 305 lediv1dd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( psi ` u ) - ( psi ` N ) ) / N ) <_ ( ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) / N ) )
307 261 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. ( u - N ) ) e. CC )
308 11 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> T e. RR+ )
309 308 rpred 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> T e. RR )
310 309 262 remulcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T x. ( N / ( log ` N ) ) ) e. RR )
311 310 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T x. ( N / ( log ` N ) ) ) e. CC )
312 divdir 
 |-  ( ( ( 2 x. ( u - N ) ) e. CC /\ ( T x. ( N / ( log ` N ) ) ) e. CC /\ ( N e. CC /\ N =/= 0 ) ) -> ( ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) / N ) = ( ( ( 2 x. ( u - N ) ) / N ) + ( ( T x. ( N / ( log ` N ) ) ) / N ) ) )
313 307 311 177 312 syl3anc 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) / N ) = ( ( ( 2 x. ( u - N ) ) / N ) + ( ( T x. ( N / ( log ` N ) ) ) / N ) ) )
314 2cnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 2 e. CC )
315 314 233 165 166 divassd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( 2 x. ( u - N ) ) / N ) = ( 2 x. ( ( u - N ) / N ) ) )
316 113 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> T e. CC )
317 138 rpcnne0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( log ` N ) e. CC /\ ( log ` N ) =/= 0 ) )
318 div12 
 |-  ( ( T e. CC /\ N e. CC /\ ( ( log ` N ) e. CC /\ ( log ` N ) =/= 0 ) ) -> ( T x. ( N / ( log ` N ) ) ) = ( N x. ( T / ( log ` N ) ) ) )
319 316 165 317 318 syl3anc 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T x. ( N / ( log ` N ) ) ) = ( N x. ( T / ( log ` N ) ) ) )
320 319 oveq1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( T x. ( N / ( log ` N ) ) ) / N ) = ( ( N x. ( T / ( log ` N ) ) ) / N ) )
321 308 138 rpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( log ` N ) ) e. RR+ )
322 321 rpcnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( log ` N ) ) e. CC )
323 322 165 166 divcan3d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( N x. ( T / ( log ` N ) ) ) / N ) = ( T / ( log ` N ) ) )
324 320 323 eqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( T x. ( N / ( log ` N ) ) ) / N ) = ( T / ( log ` N ) ) )
325 315 324 oveq12d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( 2 x. ( u - N ) ) / N ) + ( ( T x. ( N / ( log ` N ) ) ) / N ) ) = ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) )
326 313 325 eqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( 2 x. ( u - N ) ) + ( T x. ( N / ( log ` N ) ) ) ) / N ) = ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) )
327 306 326 breqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( psi ` u ) - ( psi ` N ) ) / N ) <_ ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) )
328 149 259 143 327 leadd2dd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) <_ ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) ) )
329 143 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) e. CC )
330 258 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. ( ( u - N ) / N ) ) e. CC )
331 139 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( log ` N ) ) e. CC )
332 329 330 331 addassd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( 2 x. ( ( u - N ) / N ) ) ) + ( T / ( log ` N ) ) ) = ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) ) )
333 2cn 
 |-  2 e. CC
334 mulcom 
 |-  ( ( 2 e. CC /\ ( ( u - N ) / N ) e. CC ) -> ( 2 x. ( ( u - N ) / N ) ) = ( ( ( u - N ) / N ) x. 2 ) )
335 333 197 334 sylancr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 2 x. ( ( u - N ) / N ) ) = ( ( ( u - N ) / N ) x. 2 ) )
336 335 oveq2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( 2 x. ( ( u - N ) / N ) ) ) = ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( u - N ) / N ) x. 2 ) ) )
337 142 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) e. CC )
338 197 337 314 adddid 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) + 2 ) ) = ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( u - N ) / N ) x. 2 ) ) )
339 246 174 314 addassd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) + 2 ) = ( ( abs ` ( ( R ` u ) / u ) ) + ( 1 + 2 ) ) )
340 1p2e3 
 |-  ( 1 + 2 ) = 3
341 340 oveq2i 
 |-  ( ( abs ` ( ( R ` u ) / u ) ) + ( 1 + 2 ) ) = ( ( abs ` ( ( R ` u ) / u ) ) + 3 )
342 339 341 eqtrdi 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) + 2 ) = ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) )
343 342 oveq2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) + 2 ) ) = ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) )
344 336 338 343 3eqtr2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( 2 x. ( ( u - N ) / N ) ) ) = ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) )
345 344 oveq1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( 2 x. ( ( u - N ) / N ) ) ) + ( T / ( log ` N ) ) ) = ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) )
346 332 345 eqtr3d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( 2 x. ( ( u - N ) / N ) ) + ( T / ( log ` N ) ) ) ) = ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) )
347 328 346 breqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 1 ) ) + ( ( ( psi ` u ) - ( psi ` N ) ) / N ) ) <_ ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) )
348 97 150 140 256 347 letrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) <_ ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) )
349 104 rehalfcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( E / 2 ) / 2 ) e. RR )
350 81 297 82 ledivmul2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u / N ) <_ ( 1 + ( L x. E ) ) <-> u <_ ( ( 1 + ( L x. E ) ) x. N ) ) )
351 292 350 mpbird 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u / N ) <_ ( 1 + ( L x. E ) ) )
352 ax-1cn 
 |-  1 e. CC
353 25 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( L x. E ) e. RR )
354 353 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( L x. E ) e. CC )
355 addcom 
 |-  ( ( 1 e. CC /\ ( L x. E ) e. CC ) -> ( 1 + ( L x. E ) ) = ( ( L x. E ) + 1 ) )
356 352 354 355 sylancr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 1 + ( L x. E ) ) = ( ( L x. E ) + 1 ) )
357 351 356 breqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( u / N ) <_ ( ( L x. E ) + 1 ) )
358 172 114 353 lesubaddd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u / N ) - 1 ) <_ ( L x. E ) <-> ( u / N ) <_ ( ( L x. E ) + 1 ) ) )
359 357 358 mpbird 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u / N ) - 1 ) <_ ( L x. E ) )
360 170 359 eqbrtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( u - N ) / N ) <_ ( L x. E ) )
361 2 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> A e. RR+ )
362 361 rpred 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> A e. RR )
363 fveq2 
 |-  ( x = u -> ( R ` x ) = ( R ` u ) )
364 id 
 |-  ( x = u -> x = u )
365 363 364 oveq12d 
 |-  ( x = u -> ( ( R ` x ) / x ) = ( ( R ` u ) / u ) )
366 365 fveq2d 
 |-  ( x = u -> ( abs ` ( ( R ` x ) / x ) ) = ( abs ` ( ( R ` u ) / u ) ) )
367 366 breq1d 
 |-  ( x = u -> ( ( abs ` ( ( R ` x ) / x ) ) <_ A <-> ( abs ` ( ( R ` u ) / u ) ) <_ A ) )
368 4 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
369 367 368 84 rspcdva 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) / u ) ) <_ A )
370 90 362 109 369 leadd1dd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) <_ ( A + 3 ) )
371 107 201 jca 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) e. RR /\ 0 <_ ( ( u - N ) / N ) ) )
372 3rp 
 |-  3 e. RR+
373 rpaddcl 
 |-  ( ( A e. RR+ /\ 3 e. RR+ ) -> ( A + 3 ) e. RR+ )
374 361 372 373 sylancl 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( A + 3 ) e. RR+ )
375 374 rprege0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( A + 3 ) e. RR /\ 0 <_ ( A + 3 ) ) )
376 lemul12b 
 |-  ( ( ( ( ( ( u - N ) / N ) e. RR /\ 0 <_ ( ( u - N ) / N ) ) /\ ( L x. E ) e. RR ) /\ ( ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) e. RR /\ ( ( A + 3 ) e. RR /\ 0 <_ ( A + 3 ) ) ) ) -> ( ( ( ( u - N ) / N ) <_ ( L x. E ) /\ ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) <_ ( A + 3 ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) <_ ( ( L x. E ) x. ( A + 3 ) ) ) )
377 371 353 110 375 376 syl22anc 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) <_ ( L x. E ) /\ ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) <_ ( A + 3 ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) <_ ( ( L x. E ) x. ( A + 3 ) ) ) )
378 360 370 377 mp2and 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) <_ ( ( L x. E ) x. ( A + 3 ) ) )
379 43 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> E e. RR+ )
380 115 116 mp1i 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 4 e. RR+ )
381 379 380 rpdivcld 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( E / 4 ) e. RR+ )
382 381 rpcnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( E / 4 ) e. CC )
383 374 rpcnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( A + 3 ) e. CC )
384 374 rpne0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( A + 3 ) =/= 0 )
385 382 383 384 divcan1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( E / 4 ) / ( A + 3 ) ) x. ( A + 3 ) ) = ( E / 4 ) )
386 24 recnd 
 |-  ( ph -> E e. CC )
387 386 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> E e. CC )
388 380 rpcnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 4 e. CC )
389 380 rpne0d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 4 =/= 0 )
390 387 388 389 divrec2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( E / 4 ) = ( ( 1 / 4 ) x. E ) )
391 390 oveq1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( E / 4 ) / ( A + 3 ) ) = ( ( ( 1 / 4 ) x. E ) / ( A + 3 ) ) )
392 4cn 
 |-  4 e. CC
393 4ne0 
 |-  4 =/= 0
394 392 393 reccli 
 |-  ( 1 / 4 ) e. CC
395 394 a1i 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( 1 / 4 ) e. CC )
396 395 387 383 384 div23d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( 1 / 4 ) x. E ) / ( A + 3 ) ) = ( ( ( 1 / 4 ) / ( A + 3 ) ) x. E ) )
397 3 oveq1i 
 |-  ( L x. E ) = ( ( ( 1 / 4 ) / ( A + 3 ) ) x. E )
398 396 397 eqtr4di 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( 1 / 4 ) x. E ) / ( A + 3 ) ) = ( L x. E ) )
399 391 398 eqtr2d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( L x. E ) = ( ( E / 4 ) / ( A + 3 ) ) )
400 399 oveq1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( L x. E ) x. ( A + 3 ) ) = ( ( ( E / 4 ) / ( A + 3 ) ) x. ( A + 3 ) ) )
401 2ne0 
 |-  2 =/= 0
402 401 a1i 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> 2 =/= 0 )
403 387 314 314 402 402 divdiv1d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( E / 2 ) / 2 ) = ( E / ( 2 x. 2 ) ) )
404 2t2e4 
 |-  ( 2 x. 2 ) = 4
405 404 oveq2i 
 |-  ( E / ( 2 x. 2 ) ) = ( E / 4 )
406 403 405 eqtrdi 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( E / 2 ) / 2 ) = ( E / 4 ) )
407 385 400 406 3eqtr4d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( L x. E ) x. ( A + 3 ) ) = ( ( E / 2 ) / 2 ) )
408 378 407 breqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) <_ ( ( E / 2 ) / 2 ) )
409 120 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( E / 4 ) ) e. RR )
410 138 rpred 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( log ` N ) e. RR )
411 82 reeflogd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( exp ` ( log ` N ) ) = N )
412 136 411 breqtrrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( exp ` ( T / ( E / 4 ) ) ) < ( exp ` ( log ` N ) ) )
413 eflt 
 |-  ( ( ( T / ( E / 4 ) ) e. RR /\ ( log ` N ) e. RR ) -> ( ( T / ( E / 4 ) ) < ( log ` N ) <-> ( exp ` ( T / ( E / 4 ) ) ) < ( exp ` ( log ` N ) ) ) )
414 409 410 413 syl2anc 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( T / ( E / 4 ) ) < ( log ` N ) <-> ( exp ` ( T / ( E / 4 ) ) ) < ( exp ` ( log ` N ) ) ) )
415 412 414 mpbird 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( E / 4 ) ) < ( log ` N ) )
416 409 410 415 ltled 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( E / 4 ) ) <_ ( log ` N ) )
417 113 381 138 416 lediv23d 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( log ` N ) ) <_ ( E / 4 ) )
418 417 406 breqtrrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( T / ( log ` N ) ) <_ ( ( E / 2 ) / 2 ) )
419 111 139 349 349 408 418 le2addd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) <_ ( ( ( E / 2 ) / 2 ) + ( ( E / 2 ) / 2 ) ) )
420 104 recnd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( E / 2 ) e. CC )
421 420 2halvesd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( E / 2 ) / 2 ) + ( ( E / 2 ) / 2 ) ) = ( E / 2 ) )
422 419 421 breqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( ( ( u - N ) / N ) x. ( ( abs ` ( ( R ` u ) / u ) ) + 3 ) ) + ( T / ( log ` N ) ) ) <_ ( E / 2 ) )
423 97 140 104 348 422 letrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) <_ ( E / 2 ) )
424 16 simprd 
 |-  ( ph -> ( abs ` ( ( R ` N ) / N ) ) <_ ( E / 2 ) )
425 424 adantr 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` N ) / N ) ) <_ ( E / 2 ) )
426 97 98 104 104 423 425 le2addd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) + ( abs ` ( ( R ` N ) / N ) ) ) <_ ( ( E / 2 ) + ( E / 2 ) ) )
427 387 2halvesd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( E / 2 ) + ( E / 2 ) ) = E )
428 426 427 breqtrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( ( abs ` ( ( ( R ` u ) / u ) - ( ( R ` N ) / N ) ) ) + ( abs ` ( ( R ` N ) / N ) ) ) <_ E )
429 90 99 100 103 428 letrd 
 |-  ( ( ph /\ u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ) -> ( abs ` ( ( R ` u ) / u ) ) <_ E )
430 429 ralrimiva 
 |-  ( ph -> A. u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E )
431 19 79 430 jca31 
 |-  ( ph -> ( ( Y < N /\ ( ( 1 + ( L x. E ) ) x. N ) < ( M x. Y ) ) /\ A. u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
432 breq2 
 |-  ( z = N -> ( Y < z <-> Y < N ) )
433 oveq2 
 |-  ( z = N -> ( ( 1 + ( L x. E ) ) x. z ) = ( ( 1 + ( L x. E ) ) x. N ) )
434 433 breq1d 
 |-  ( z = N -> ( ( ( 1 + ( L x. E ) ) x. z ) < ( M x. Y ) <-> ( ( 1 + ( L x. E ) ) x. N ) < ( M x. Y ) ) )
435 432 434 anbi12d 
 |-  ( z = N -> ( ( Y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( M x. Y ) ) <-> ( Y < N /\ ( ( 1 + ( L x. E ) ) x. N ) < ( M x. Y ) ) ) )
436 id 
 |-  ( z = N -> z = N )
437 436 433 oveq12d 
 |-  ( z = N -> ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) = ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) )
438 437 raleqdv 
 |-  ( z = N -> ( A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E <-> A. u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
439 435 438 anbi12d 
 |-  ( z = N -> ( ( ( Y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( M x. Y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) <-> ( ( Y < N /\ ( ( 1 + ( L x. E ) ) x. N ) < ( M x. Y ) ) /\ A. u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) )
440 439 rspcev 
 |-  ( ( N e. RR+ /\ ( ( Y < N /\ ( ( 1 + ( L x. E ) ) x. N ) < ( M x. Y ) ) /\ A. u e. ( N [,] ( ( 1 + ( L x. E ) ) x. N ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) -> E. z e. RR+ ( ( Y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( M x. Y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
441 17 431 440 syl2anc 
 |-  ( ph -> E. z e. RR+ ( ( Y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( M x. Y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )