Metamath Proof Explorer

Theorem pntpbnd1a

Description: Lemma for pntpbnd . (Contributed by Mario Carneiro, 11-Apr-2016) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020)

Ref Expression
Hypotheses pntpbnd.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntpbnd1.e 
|- ( ph -> E e. ( 0 (,) 1 ) )
pntpbnd1.x 
|- X = ( exp ` ( 2 / E ) )
pntpbnd1.y 
|- ( ph -> Y e. ( X (,) +oo ) )
pntpbnd1a.1 
|- ( ph -> N e. NN )
pntpbnd1a.2 
|- ( ph -> ( Y < N /\ N <_ ( K x. Y ) ) )
pntpbnd1a.3 
|- ( ph -> ( abs ` ( R ` N ) ) <_ ( abs ` ( ( R ` ( N + 1 ) ) - ( R ` N ) ) ) )
Assertion pntpbnd1a 
|- ( ph -> ( abs ` ( ( R ` N ) / N ) ) <_ E )

Proof

Step Hyp Ref Expression
1 pntpbnd.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntpbnd1.e 
 |-  ( ph -> E e. ( 0 (,) 1 ) )
3 pntpbnd1.x 
 |-  X = ( exp ` ( 2 / E ) )
4 pntpbnd1.y 
 |-  ( ph -> Y e. ( X (,) +oo ) )
5 pntpbnd1a.1 
 |-  ( ph -> N e. NN )
6 pntpbnd1a.2 
 |-  ( ph -> ( Y < N /\ N <_ ( K x. Y ) ) )
7 pntpbnd1a.3 
 |-  ( ph -> ( abs ` ( R ` N ) ) <_ ( abs ` ( ( R ` ( N + 1 ) ) - ( R ` N ) ) ) )
8 5 nnrpd 
 |-  ( ph -> N e. RR+ )
9 1 pntrf 
 |-  R : RR+ --> RR
10 9 ffvelrni 
 |-  ( N e. RR+ -> ( R ` N ) e. RR )
11 8 10 syl 
 |-  ( ph -> ( R ` N ) e. RR )
12 11 8 rerpdivcld 
 |-  ( ph -> ( ( R ` N ) / N ) e. RR )
13 12 recnd 
 |-  ( ph -> ( ( R ` N ) / N ) e. CC )
14 13 abscld 
 |-  ( ph -> ( abs ` ( ( R ` N ) / N ) ) e. RR )
15 8 relogcld 
 |-  ( ph -> ( log ` N ) e. RR )
16 15 8 rerpdivcld 
 |-  ( ph -> ( ( log ` N ) / N ) e. RR )
17 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
18 17 2 sseldi 
 |-  ( ph -> E e. RR )
19 11 recnd 
 |-  ( ph -> ( R ` N ) e. CC )
20 5 nnred 
 |-  ( ph -> N e. RR )
21 20 recnd 
 |-  ( ph -> N e. CC )
22 5 nnne0d 
 |-  ( ph -> N =/= 0 )
23 19 21 22 absdivd 
 |-  ( ph -> ( abs ` ( ( R ` N ) / N ) ) = ( ( abs ` ( R ` N ) ) / ( abs ` N ) ) )
24 5 nnnn0d 
 |-  ( ph -> N e. NN0 )
25 24 nn0ge0d 
 |-  ( ph -> 0 <_ N )
26 20 25 absidd 
 |-  ( ph -> ( abs ` N ) = N )
27 26 oveq2d 
 |-  ( ph -> ( ( abs ` ( R ` N ) ) / ( abs ` N ) ) = ( ( abs ` ( R ` N ) ) / N ) )
28 23 27 eqtrd 
 |-  ( ph -> ( abs ` ( ( R ` N ) / N ) ) = ( ( abs ` ( R ` N ) ) / N ) )
29 19 abscld 
 |-  ( ph -> ( abs ` ( R ` N ) ) e. RR )
30 5 peano2nnd 
 |-  ( ph -> ( N + 1 ) e. NN )
31 vmacl 
 |-  ( ( N + 1 ) e. NN -> ( Lam ` ( N + 1 ) ) e. RR )
32 30 31 syl 
 |-  ( ph -> ( Lam ` ( N + 1 ) ) e. RR )
33 peano2rem 
 |-  ( ( Lam ` ( N + 1 ) ) e. RR -> ( ( Lam ` ( N + 1 ) ) - 1 ) e. RR )
34 32 33 syl 
 |-  ( ph -> ( ( Lam ` ( N + 1 ) ) - 1 ) e. RR )
35 34 recnd 
 |-  ( ph -> ( ( Lam ` ( N + 1 ) ) - 1 ) e. CC )
36 35 abscld 
 |-  ( ph -> ( abs ` ( ( Lam ` ( N + 1 ) ) - 1 ) ) e. RR )
37 30 nnrpd 
 |-  ( ph -> ( N + 1 ) e. RR+ )
38 1 pntrval 
 |-  ( ( N + 1 ) e. RR+ -> ( R ` ( N + 1 ) ) = ( ( psi ` ( N + 1 ) ) - ( N + 1 ) ) )
39 37 38 syl 
 |-  ( ph -> ( R ` ( N + 1 ) ) = ( ( psi ` ( N + 1 ) ) - ( N + 1 ) ) )
40 1 pntrval 
 |-  ( N e. RR+ -> ( R ` N ) = ( ( psi ` N ) - N ) )
41 8 40 syl 
 |-  ( ph -> ( R ` N ) = ( ( psi ` N ) - N ) )
42 39 41 oveq12d 
 |-  ( ph -> ( ( R ` ( N + 1 ) ) - ( R ` N ) ) = ( ( ( psi ` ( N + 1 ) ) - ( N + 1 ) ) - ( ( psi ` N ) - N ) ) )
43 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
44 20 43 syl 
 |-  ( ph -> ( N + 1 ) e. RR )
45 chpcl 
 |-  ( ( N + 1 ) e. RR -> ( psi ` ( N + 1 ) ) e. RR )
46 44 45 syl 
 |-  ( ph -> ( psi ` ( N + 1 ) ) e. RR )
47 46 recnd 
 |-  ( ph -> ( psi ` ( N + 1 ) ) e. CC )
48 44 recnd 
 |-  ( ph -> ( N + 1 ) e. CC )
49 chpcl 
 |-  ( N e. RR -> ( psi ` N ) e. RR )
50 20 49 syl 
 |-  ( ph -> ( psi ` N ) e. RR )
51 50 recnd 
 |-  ( ph -> ( psi ` N ) e. CC )
52 47 48 51 21 sub4d 
 |-  ( ph -> ( ( ( psi ` ( N + 1 ) ) - ( N + 1 ) ) - ( ( psi ` N ) - N ) ) = ( ( ( psi ` ( N + 1 ) ) - ( psi ` N ) ) - ( ( N + 1 ) - N ) ) )
53 32 recnd 
 |-  ( ph -> ( Lam ` ( N + 1 ) ) e. CC )
54 chpp1 
 |-  ( N e. NN0 -> ( psi ` ( N + 1 ) ) = ( ( psi ` N ) + ( Lam ` ( N + 1 ) ) ) )
55 24 54 syl 
 |-  ( ph -> ( psi ` ( N + 1 ) ) = ( ( psi ` N ) + ( Lam ` ( N + 1 ) ) ) )
56 51 53 55 mvrladdd 
 |-  ( ph -> ( ( psi ` ( N + 1 ) ) - ( psi ` N ) ) = ( Lam ` ( N + 1 ) ) )
57 ax-1cn 
 |-  1 e. CC
58 pncan2 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - N ) = 1 )
59 21 57 58 sylancl 
 |-  ( ph -> ( ( N + 1 ) - N ) = 1 )
60 56 59 oveq12d 
 |-  ( ph -> ( ( ( psi ` ( N + 1 ) ) - ( psi ` N ) ) - ( ( N + 1 ) - N ) ) = ( ( Lam ` ( N + 1 ) ) - 1 ) )
61 42 52 60 3eqtrd 
 |-  ( ph -> ( ( R ` ( N + 1 ) ) - ( R ` N ) ) = ( ( Lam ` ( N + 1 ) ) - 1 ) )
62 61 fveq2d 
 |-  ( ph -> ( abs ` ( ( R ` ( N + 1 ) ) - ( R ` N ) ) ) = ( abs ` ( ( Lam ` ( N + 1 ) ) - 1 ) ) )
63 7 62 breqtrd 
 |-  ( ph -> ( abs ` ( R ` N ) ) <_ ( abs ` ( ( Lam ` ( N + 1 ) ) - 1 ) ) )
64 1red 
 |-  ( ph -> 1 e. RR )
65 64 15 resubcld 
 |-  ( ph -> ( 1 - ( log ` N ) ) e. RR )
66 0red 
 |-  ( ph -> 0 e. RR )
67 2re 
 |-  2 e. RR
68 eliooord 
 |-  ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) )
69 2 68 syl 
 |-  ( ph -> ( 0 < E /\ E < 1 ) )
70 69 simpld 
 |-  ( ph -> 0 < E )
71 18 70 elrpd 
 |-  ( ph -> E e. RR+ )
72 rerpdivcl 
 |-  ( ( 2 e. RR /\ E e. RR+ ) -> ( 2 / E ) e. RR )
73 67 71 72 sylancr 
 |-  ( ph -> ( 2 / E ) e. RR )
74 67 a1i 
 |-  ( ph -> 2 e. RR )
75 1lt2 
 |-  1 < 2
76 75 a1i 
 |-  ( ph -> 1 < 2 )
77 2cn 
 |-  2 e. CC
78 77 div1i 
 |-  ( 2 / 1 ) = 2
79 69 simprd 
 |-  ( ph -> E < 1 )
80 0lt1 
 |-  0 < 1
81 80 a1i 
 |-  ( ph -> 0 < 1 )
82 2pos 
 |-  0 < 2
83 82 a1i 
 |-  ( ph -> 0 < 2 )
84 ltdiv2 
 |-  ( ( ( E e. RR /\ 0 < E ) /\ ( 1 e. RR /\ 0 < 1 ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( E < 1 <-> ( 2 / 1 ) < ( 2 / E ) ) )
85 18 70 64 81 74 83 84 syl222anc 
 |-  ( ph -> ( E < 1 <-> ( 2 / 1 ) < ( 2 / E ) ) )
86 79 85 mpbid 
 |-  ( ph -> ( 2 / 1 ) < ( 2 / E ) )
87 78 86 eqbrtrrid 
 |-  ( ph -> 2 < ( 2 / E ) )
88 64 74 73 76 87 lttrd 
 |-  ( ph -> 1 < ( 2 / E ) )
89 73 rpefcld 
 |-  ( ph -> ( exp ` ( 2 / E ) ) e. RR+ )
90 3 89 eqeltrid 
 |-  ( ph -> X e. RR+ )
91 90 rpred 
 |-  ( ph -> X e. RR )
92 90 rpxrd 
 |-  ( ph -> X e. RR* )
93 elioopnf 
 |-  ( X e. RR* -> ( Y e. ( X (,) +oo ) <-> ( Y e. RR /\ X < Y ) ) )
94 92 93 syl 
 |-  ( ph -> ( Y e. ( X (,) +oo ) <-> ( Y e. RR /\ X < Y ) ) )
95 4 94 mpbid 
 |-  ( ph -> ( Y e. RR /\ X < Y ) )
96 95 simpld 
 |-  ( ph -> Y e. RR )
97 95 simprd 
 |-  ( ph -> X < Y )
98 6 simpld 
 |-  ( ph -> Y < N )
99 91 96 20 97 98 lttrd 
 |-  ( ph -> X < N )
100 3 99 eqbrtrrid 
 |-  ( ph -> ( exp ` ( 2 / E ) ) < N )
101 8 reeflogd 
 |-  ( ph -> ( exp ` ( log ` N ) ) = N )
102 100 101 breqtrrd 
 |-  ( ph -> ( exp ` ( 2 / E ) ) < ( exp ` ( log ` N ) ) )
103 eflt 
 |-  ( ( ( 2 / E ) e. RR /\ ( log ` N ) e. RR ) -> ( ( 2 / E ) < ( log ` N ) <-> ( exp ` ( 2 / E ) ) < ( exp ` ( log ` N ) ) ) )
104 73 15 103 syl2anc 
 |-  ( ph -> ( ( 2 / E ) < ( log ` N ) <-> ( exp ` ( 2 / E ) ) < ( exp ` ( log ` N ) ) ) )
105 102 104 mpbird 
 |-  ( ph -> ( 2 / E ) < ( log ` N ) )
106 64 73 15 88 105 lttrd 
 |-  ( ph -> 1 < ( log ` N ) )
107 64 15 106 ltled 
 |-  ( ph -> 1 <_ ( log ` N ) )
108 1re 
 |-  1 e. RR
109 suble0 
 |-  ( ( 1 e. RR /\ ( log ` N ) e. RR ) -> ( ( 1 - ( log ` N ) ) <_ 0 <-> 1 <_ ( log ` N ) ) )
110 108 15 109 sylancr 
 |-  ( ph -> ( ( 1 - ( log ` N ) ) <_ 0 <-> 1 <_ ( log ` N ) ) )
111 107 110 mpbird 
 |-  ( ph -> ( 1 - ( log ` N ) ) <_ 0 )
112 vmage0 
 |-  ( ( N + 1 ) e. NN -> 0 <_ ( Lam ` ( N + 1 ) ) )
113 30 112 syl 
 |-  ( ph -> 0 <_ ( Lam ` ( N + 1 ) ) )
114 65 66 32 111 113 letrd 
 |-  ( ph -> ( 1 - ( log ` N ) ) <_ ( Lam ` ( N + 1 ) ) )
115 37 relogcld 
 |-  ( ph -> ( log ` ( N + 1 ) ) e. RR )
116 readdcl 
 |-  ( ( 1 e. RR /\ ( log ` N ) e. RR ) -> ( 1 + ( log ` N ) ) e. RR )
117 108 15 116 sylancr 
 |-  ( ph -> ( 1 + ( log ` N ) ) e. RR )
118 vmalelog 
 |-  ( ( N + 1 ) e. NN -> ( Lam ` ( N + 1 ) ) <_ ( log ` ( N + 1 ) ) )
119 30 118 syl 
 |-  ( ph -> ( Lam ` ( N + 1 ) ) <_ ( log ` ( N + 1 ) ) )
120 74 20 remulcld 
 |-  ( ph -> ( 2 x. N ) e. RR )
121 epr 
 |-  _e e. RR+
122 rpmulcl 
 |-  ( ( _e e. RR+ /\ N e. RR+ ) -> ( _e x. N ) e. RR+ )
123 121 8 122 sylancr 
 |-  ( ph -> ( _e x. N ) e. RR+ )
124 123 rpred 
 |-  ( ph -> ( _e x. N ) e. RR )
125 5 nnge1d 
 |-  ( ph -> 1 <_ N )
126 64 20 20 125 leadd2dd 
 |-  ( ph -> ( N + 1 ) <_ ( N + N ) )
127 21 2timesd 
 |-  ( ph -> ( 2 x. N ) = ( N + N ) )
128 126 127 breqtrrd 
 |-  ( ph -> ( N + 1 ) <_ ( 2 x. N ) )
129 ere 
 |-  _e e. RR
130 egt2lt3 
 |-  ( 2 < _e /\ _e < 3 )
131 130 simpli 
 |-  2 < _e
132 67 129 131 ltleii 
 |-  2 <_ _e
133 132 a1i 
 |-  ( ph -> 2 <_ _e )
134 129 a1i 
 |-  ( ph -> _e e. RR )
135 5 nngt0d 
 |-  ( ph -> 0 < N )
136 lemul1 
 |-  ( ( 2 e. RR /\ _e e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( 2 <_ _e <-> ( 2 x. N ) <_ ( _e x. N ) ) )
137 74 134 20 135 136 syl112anc 
 |-  ( ph -> ( 2 <_ _e <-> ( 2 x. N ) <_ ( _e x. N ) ) )
138 133 137 mpbid 
 |-  ( ph -> ( 2 x. N ) <_ ( _e x. N ) )
139 44 120 124 128 138 letrd 
 |-  ( ph -> ( N + 1 ) <_ ( _e x. N ) )
140 37 123 logled 
 |-  ( ph -> ( ( N + 1 ) <_ ( _e x. N ) <-> ( log ` ( N + 1 ) ) <_ ( log ` ( _e x. N ) ) ) )
141 139 140 mpbid 
 |-  ( ph -> ( log ` ( N + 1 ) ) <_ ( log ` ( _e x. N ) ) )
142 relogmul 
 |-  ( ( _e e. RR+ /\ N e. RR+ ) -> ( log ` ( _e x. N ) ) = ( ( log ` _e ) + ( log ` N ) ) )
143 121 8 142 sylancr 
 |-  ( ph -> ( log ` ( _e x. N ) ) = ( ( log ` _e ) + ( log ` N ) ) )
144 loge 
 |-  ( log ` _e ) = 1
145 144 oveq1i 
 |-  ( ( log ` _e ) + ( log ` N ) ) = ( 1 + ( log ` N ) )
146 143 145 eqtrdi 
 |-  ( ph -> ( log ` ( _e x. N ) ) = ( 1 + ( log ` N ) ) )
147 141 146 breqtrd 
 |-  ( ph -> ( log ` ( N + 1 ) ) <_ ( 1 + ( log ` N ) ) )
148 32 115 117 119 147 letrd 
 |-  ( ph -> ( Lam ` ( N + 1 ) ) <_ ( 1 + ( log ` N ) ) )
149 32 64 15 absdifled 
 |-  ( ph -> ( ( abs ` ( ( Lam ` ( N + 1 ) ) - 1 ) ) <_ ( log ` N ) <-> ( ( 1 - ( log ` N ) ) <_ ( Lam ` ( N + 1 ) ) /\ ( Lam ` ( N + 1 ) ) <_ ( 1 + ( log ` N ) ) ) ) )
150 114 148 149 mpbir2and 
 |-  ( ph -> ( abs ` ( ( Lam ` ( N + 1 ) ) - 1 ) ) <_ ( log ` N ) )
151 29 36 15 63 150 letrd 
 |-  ( ph -> ( abs ` ( R ` N ) ) <_ ( log ` N ) )
152 29 15 8 151 lediv1dd 
 |-  ( ph -> ( ( abs ` ( R ` N ) ) / N ) <_ ( ( log ` N ) / N ) )
153 28 152 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( R ` N ) / N ) ) <_ ( ( log ` N ) / N ) )
154 90 relogcld 
 |-  ( ph -> ( log ` X ) e. RR )
155 154 90 rerpdivcld 
 |-  ( ph -> ( ( log ` X ) / X ) e. RR )
156 64 73 88 ltled 
 |-  ( ph -> 1 <_ ( 2 / E ) )
157 efle 
 |-  ( ( 1 e. RR /\ ( 2 / E ) e. RR ) -> ( 1 <_ ( 2 / E ) <-> ( exp ` 1 ) <_ ( exp ` ( 2 / E ) ) ) )
158 108 73 157 sylancr 
 |-  ( ph -> ( 1 <_ ( 2 / E ) <-> ( exp ` 1 ) <_ ( exp ` ( 2 / E ) ) ) )
159 156 158 mpbid 
 |-  ( ph -> ( exp ` 1 ) <_ ( exp ` ( 2 / E ) ) )
160 df-e 
 |-  _e = ( exp ` 1 )
161 159 160 3 3brtr4g 
 |-  ( ph -> _e <_ X )
162 144 107 eqbrtrid 
 |-  ( ph -> ( log ` _e ) <_ ( log ` N ) )
163 logleb 
 |-  ( ( _e e. RR+ /\ N e. RR+ ) -> ( _e <_ N <-> ( log ` _e ) <_ ( log ` N ) ) )
164 121 8 163 sylancr 
 |-  ( ph -> ( _e <_ N <-> ( log ` _e ) <_ ( log ` N ) ) )
165 162 164 mpbird 
 |-  ( ph -> _e <_ N )
166 logdivlt 
 |-  ( ( ( X e. RR /\ _e <_ X ) /\ ( N e. RR /\ _e <_ N ) ) -> ( X < N <-> ( ( log ` N ) / N ) < ( ( log ` X ) / X ) ) )
167 91 161 20 165 166 syl22anc 
 |-  ( ph -> ( X < N <-> ( ( log ` N ) / N ) < ( ( log ` X ) / X ) ) )
168 99 167 mpbid 
 |-  ( ph -> ( ( log ` N ) / N ) < ( ( log ` X ) / X ) )
169 3 fveq2i 
 |-  ( log ` X ) = ( log ` ( exp ` ( 2 / E ) ) )
170 73 relogefd 
 |-  ( ph -> ( log ` ( exp ` ( 2 / E ) ) ) = ( 2 / E ) )
171 169 170 syl5eq 
 |-  ( ph -> ( log ` X ) = ( 2 / E ) )
172 171 oveq1d 
 |-  ( ph -> ( ( log ` X ) / X ) = ( ( 2 / E ) / X ) )
173 2rp 
 |-  2 e. RR+
174 rpdivcl 
 |-  ( ( 2 e. RR+ /\ E e. RR+ ) -> ( 2 / E ) e. RR+ )
175 173 71 174 sylancr 
 |-  ( ph -> ( 2 / E ) e. RR+ )
176 175 rpcnd 
 |-  ( ph -> ( 2 / E ) e. CC )
177 176 sqvald 
 |-  ( ph -> ( ( 2 / E ) ^ 2 ) = ( ( 2 / E ) x. ( 2 / E ) ) )
178 2cnd 
 |-  ( ph -> 2 e. CC )
179 71 rpcnne0d 
 |-  ( ph -> ( E e. CC /\ E =/= 0 ) )
180 div12 
 |-  ( ( ( 2 / E ) e. CC /\ 2 e. CC /\ ( E e. CC /\ E =/= 0 ) ) -> ( ( 2 / E ) x. ( 2 / E ) ) = ( 2 x. ( ( 2 / E ) / E ) ) )
181 176 178 179 180 syl3anc 
 |-  ( ph -> ( ( 2 / E ) x. ( 2 / E ) ) = ( 2 x. ( ( 2 / E ) / E ) ) )
182 177 181 eqtrd 
 |-  ( ph -> ( ( 2 / E ) ^ 2 ) = ( 2 x. ( ( 2 / E ) / E ) ) )
183 182 oveq1d 
 |-  ( ph -> ( ( ( 2 / E ) ^ 2 ) / 2 ) = ( ( 2 x. ( ( 2 / E ) / E ) ) / 2 ) )
184 175 71 rpdivcld 
 |-  ( ph -> ( ( 2 / E ) / E ) e. RR+ )
185 184 rpcnd 
 |-  ( ph -> ( ( 2 / E ) / E ) e. CC )
186 2ne0 
 |-  2 =/= 0
187 186 a1i 
 |-  ( ph -> 2 =/= 0 )
188 185 178 187 divcan3d 
 |-  ( ph -> ( ( 2 x. ( ( 2 / E ) / E ) ) / 2 ) = ( ( 2 / E ) / E ) )
189 183 188 eqtrd 
 |-  ( ph -> ( ( ( 2 / E ) ^ 2 ) / 2 ) = ( ( 2 / E ) / E ) )
190 73 resqcld 
 |-  ( ph -> ( ( 2 / E ) ^ 2 ) e. RR )
191 190 rehalfcld 
 |-  ( ph -> ( ( ( 2 / E ) ^ 2 ) / 2 ) e. RR )
192 1rp 
 |-  1 e. RR+
193 rpaddcl 
 |-  ( ( 1 e. RR+ /\ ( 2 / E ) e. RR+ ) -> ( 1 + ( 2 / E ) ) e. RR+ )
194 192 175 193 sylancr 
 |-  ( ph -> ( 1 + ( 2 / E ) ) e. RR+ )
195 194 rpred 
 |-  ( ph -> ( 1 + ( 2 / E ) ) e. RR )
196 195 191 readdcld 
 |-  ( ph -> ( ( 1 + ( 2 / E ) ) + ( ( ( 2 / E ) ^ 2 ) / 2 ) ) e. RR )
197 191 194 ltaddrp2d 
 |-  ( ph -> ( ( ( 2 / E ) ^ 2 ) / 2 ) < ( ( 1 + ( 2 / E ) ) + ( ( ( 2 / E ) ^ 2 ) / 2 ) ) )
198 efgt1p2 
 |-  ( ( 2 / E ) e. RR+ -> ( ( 1 + ( 2 / E ) ) + ( ( ( 2 / E ) ^ 2 ) / 2 ) ) < ( exp ` ( 2 / E ) ) )
199 175 198 syl 
 |-  ( ph -> ( ( 1 + ( 2 / E ) ) + ( ( ( 2 / E ) ^ 2 ) / 2 ) ) < ( exp ` ( 2 / E ) ) )
200 199 3 breqtrrdi 
 |-  ( ph -> ( ( 1 + ( 2 / E ) ) + ( ( ( 2 / E ) ^ 2 ) / 2 ) ) < X )
201 191 196 91 197 200 lttrd 
 |-  ( ph -> ( ( ( 2 / E ) ^ 2 ) / 2 ) < X )
202 189 201 eqbrtrrd 
 |-  ( ph -> ( ( 2 / E ) / E ) < X )
203 73 71 90 202 ltdiv23d 
 |-  ( ph -> ( ( 2 / E ) / X ) < E )
204 172 203 eqbrtrd 
 |-  ( ph -> ( ( log ` X ) / X ) < E )
205 16 155 18 168 204 lttrd 
 |-  ( ph -> ( ( log ` N ) / N ) < E )
206 16 18 205 ltled 
 |-  ( ph -> ( ( log ` N ) / N ) <_ E )
207 14 16 18 153 206 letrd 
 |-  ( ph -> ( abs ` ( ( R ` N ) / N ) ) <_ E )