Metamath Proof Explorer


Theorem pntrsumo1

Description: A bound on a sum over R . Equation 10.1.16 of Shapiro, p. 403. (Contributed by Mario Carneiro, 25-May-2016)

Ref Expression
Hypothesis pntrval.r R = a + ψ a a
Assertion pntrsumo1 x n = 1 x R n n n + 1 𝑂1

Proof

Step Hyp Ref Expression
1 pntrval.r R = a + ψ a a
2 1re 1
3 elicopnf 1 x 1 +∞ x 1 x
4 2 3 ax-mp x 1 +∞ x 1 x
5 4 simplbi x 1 +∞ x
6 0red x 1 +∞ 0
7 1red x 1 +∞ 1
8 0lt1 0 < 1
9 8 a1i x 1 +∞ 0 < 1
10 4 simprbi x 1 +∞ 1 x
11 6 7 5 9 10 ltletrd x 1 +∞ 0 < x
12 5 11 elrpd x 1 +∞ x +
13 12 ssriv 1 +∞ +
14 13 a1i 1 +∞ +
15 rpssre +
16 14 15 sstrdi 1 +∞
17 16 resmptd x n = 1 x R n n n + 1 1 +∞ = x 1 +∞ n = 1 x R n n n + 1
18 chpcl x ψ x
19 5 18 syl x 1 +∞ ψ x
20 peano2re ψ x ψ x + 1
21 19 20 syl x 1 +∞ ψ x + 1
22 12 rprege0d x 1 +∞ x 0 x
23 flge0nn0 x 0 x x 0
24 22 23 syl x 1 +∞ x 0
25 nn0p1nn x 0 x + 1
26 24 25 syl x 1 +∞ x + 1
27 21 26 nndivred x 1 +∞ ψ x + 1 x + 1
28 27 recnd x 1 +∞ ψ x + 1 x + 1
29 ax-1cn 1
30 subcl ψ x + 1 x + 1 1 ψ x + 1 x + 1 1
31 28 29 30 sylancl x 1 +∞ ψ x + 1 x + 1 1
32 fzfid x 1 x Fin
33 elfznn n 1 x n
34 33 adantl x n 1 x n
35 nnrp n n +
36 1 pntrf R : +
37 36 ffvelrni n + R n
38 35 37 syl n R n
39 peano2nn n n + 1
40 nnmulcl n n + 1 n n + 1
41 39 40 mpdan n n n + 1
42 38 41 nndivred n R n n n + 1
43 34 42 syl x n 1 x R n n n + 1
44 32 43 fsumrecl x n = 1 x R n n n + 1
45 44 recnd x n = 1 x R n n n + 1
46 5 45 syl x 1 +∞ n = 1 x R n n n + 1
47 oveq2 m = n 1 m = 1 n
48 fvoveq1 m = n ψ m 1 = ψ n 1
49 oveq1 m = n m 1 = n 1
50 48 49 oveq12d m = n ψ m 1 m 1 = ψ n 1 n 1
51 47 50 jca m = n 1 m = 1 n ψ m 1 m 1 = ψ n 1 n 1
52 oveq2 m = n + 1 1 m = 1 n + 1
53 fvoveq1 m = n + 1 ψ m 1 = ψ n + 1 - 1
54 oveq1 m = n + 1 m 1 = n + 1 - 1
55 53 54 oveq12d m = n + 1 ψ m 1 m 1 = ψ n + 1 - 1 n + 1 - 1
56 52 55 jca m = n + 1 1 m = 1 n + 1 ψ m 1 m 1 = ψ n + 1 - 1 n + 1 - 1
57 oveq2 m = 1 1 m = 1 1
58 1div1e1 1 1 = 1
59 57 58 eqtrdi m = 1 1 m = 1
60 oveq1 m = 1 m 1 = 1 1
61 1m1e0 1 1 = 0
62 60 61 eqtrdi m = 1 m 1 = 0
63 62 fveq2d m = 1 ψ m 1 = ψ 0
64 2pos 0 < 2
65 0re 0
66 chpeq0 0 ψ 0 = 0 0 < 2
67 65 66 ax-mp ψ 0 = 0 0 < 2
68 64 67 mpbir ψ 0 = 0
69 63 68 eqtrdi m = 1 ψ m 1 = 0
70 69 62 oveq12d m = 1 ψ m 1 m 1 = 0 0
71 0m0e0 0 0 = 0
72 70 71 eqtrdi m = 1 ψ m 1 m 1 = 0
73 59 72 jca m = 1 1 m = 1 ψ m 1 m 1 = 0
74 oveq2 m = x + 1 1 m = 1 x + 1
75 fvoveq1 m = x + 1 ψ m 1 = ψ x + 1 - 1
76 oveq1 m = x + 1 m 1 = x + 1 - 1
77 75 76 oveq12d m = x + 1 ψ m 1 m 1 = ψ x + 1 - 1 x + 1 - 1
78 74 77 jca m = x + 1 1 m = 1 x + 1 ψ m 1 m 1 = ψ x + 1 - 1 x + 1 - 1
79 nnuz = 1
80 26 79 eleqtrdi x 1 +∞ x + 1 1
81 elfznn m 1 x + 1 m
82 81 adantl x 1 +∞ m 1 x + 1 m
83 82 nnrecred x 1 +∞ m 1 x + 1 1 m
84 83 recnd x 1 +∞ m 1 x + 1 1 m
85 82 nnred x 1 +∞ m 1 x + 1 m
86 peano2rem m m 1
87 85 86 syl x 1 +∞ m 1 x + 1 m 1
88 chpcl m 1 ψ m 1
89 87 88 syl x 1 +∞ m 1 x + 1 ψ m 1
90 89 87 resubcld x 1 +∞ m 1 x + 1 ψ m 1 m 1
91 90 recnd x 1 +∞ m 1 x + 1 ψ m 1 m 1
92 51 56 73 78 80 84 91 fsumparts x 1 +∞ n 1 ..^ x + 1 1 n ψ n + 1 - 1 - n + 1 - 1 - ψ n 1 n 1 = 1 x + 1 ψ x + 1 - 1 x + 1 - 1 - 1 0 - n 1 ..^ x + 1 1 n + 1 1 n ψ n + 1 - 1 n + 1 - 1
93 5 flcld x 1 +∞ x
94 fzval3 x 1 x = 1 ..^ x + 1
95 93 94 syl x 1 +∞ 1 x = 1 ..^ x + 1
96 95 eqcomd x 1 +∞ 1 ..^ x + 1 = 1 x
97 33 adantl x 1 +∞ n 1 x n
98 97 nncnd x 1 +∞ n 1 x n
99 pncan n 1 n + 1 - 1 = n
100 98 29 99 sylancl x 1 +∞ n 1 x n + 1 - 1 = n
101 97 nnred x 1 +∞ n 1 x n
102 100 101 eqeltrd x 1 +∞ n 1 x n + 1 - 1
103 chpcl n + 1 - 1 ψ n + 1 - 1
104 102 103 syl x 1 +∞ n 1 x ψ n + 1 - 1
105 104 recnd x 1 +∞ n 1 x ψ n + 1 - 1
106 102 recnd x 1 +∞ n 1 x n + 1 - 1
107 peano2rem n n 1
108 101 107 syl x 1 +∞ n 1 x n 1
109 chpcl n 1 ψ n 1
110 108 109 syl x 1 +∞ n 1 x ψ n 1
111 110 recnd x 1 +∞ n 1 x ψ n 1
112 1cnd x 1 +∞ n 1 x 1
113 98 112 subcld x 1 +∞ n 1 x n 1
114 105 106 111 113 sub4d x 1 +∞ n 1 x ψ n + 1 - 1 - n + 1 - 1 - ψ n 1 n 1 = ψ n + 1 - 1 - ψ n 1 - n + 1 - 1 - n 1
115 vmacl n Λ n
116 97 115 syl x 1 +∞ n 1 x Λ n
117 116 recnd x 1 +∞ n 1 x Λ n
118 nnm1nn0 n n 1 0
119 97 118 syl x 1 +∞ n 1 x n 1 0
120 chpp1 n 1 0 ψ n - 1 + 1 = ψ n 1 + Λ n - 1 + 1
121 119 120 syl x 1 +∞ n 1 x ψ n - 1 + 1 = ψ n 1 + Λ n - 1 + 1
122 npcan n 1 n - 1 + 1 = n
123 98 29 122 sylancl x 1 +∞ n 1 x n - 1 + 1 = n
124 123 100 eqtr4d x 1 +∞ n 1 x n - 1 + 1 = n + 1 - 1
125 124 fveq2d x 1 +∞ n 1 x ψ n - 1 + 1 = ψ n + 1 - 1
126 123 fveq2d x 1 +∞ n 1 x Λ n - 1 + 1 = Λ n
127 126 oveq2d x 1 +∞ n 1 x ψ n 1 + Λ n - 1 + 1 = ψ n 1 + Λ n
128 121 125 127 3eqtr3d x 1 +∞ n 1 x ψ n + 1 - 1 = ψ n 1 + Λ n
129 111 117 128 mvrladdd x 1 +∞ n 1 x ψ n + 1 - 1 ψ n 1 = Λ n
130 peano2cn n n + 1
131 98 130 syl x 1 +∞ n 1 x n + 1
132 131 98 112 nnncan2d x 1 +∞ n 1 x n + 1 - 1 - n 1 = n + 1 - n
133 pncan2 n 1 n + 1 - n = 1
134 98 29 133 sylancl x 1 +∞ n 1 x n + 1 - n = 1
135 132 134 eqtrd x 1 +∞ n 1 x n + 1 - 1 - n 1 = 1
136 129 135 oveq12d x 1 +∞ n 1 x ψ n + 1 - 1 - ψ n 1 - n + 1 - 1 - n 1 = Λ n 1
137 114 136 eqtrd x 1 +∞ n 1 x ψ n + 1 - 1 - n + 1 - 1 - ψ n 1 n 1 = Λ n 1
138 137 oveq2d x 1 +∞ n 1 x 1 n ψ n + 1 - 1 - n + 1 - 1 - ψ n 1 n 1 = 1 n Λ n 1
139 peano2rem Λ n Λ n 1
140 116 139 syl x 1 +∞ n 1 x Λ n 1
141 140 recnd x 1 +∞ n 1 x Λ n 1
142 97 nnne0d x 1 +∞ n 1 x n 0
143 141 98 142 divrec2d x 1 +∞ n 1 x Λ n 1 n = 1 n Λ n 1
144 138 143 eqtr4d x 1 +∞ n 1 x 1 n ψ n + 1 - 1 - n + 1 - 1 - ψ n 1 n 1 = Λ n 1 n
145 96 144 sumeq12rdv x 1 +∞ n 1 ..^ x + 1 1 n ψ n + 1 - 1 - n + 1 - 1 - ψ n 1 n 1 = n = 1 x Λ n 1 n
146 24 nn0cnd x 1 +∞ x
147 pncan x 1 x + 1 - 1 = x
148 146 29 147 sylancl x 1 +∞ x + 1 - 1 = x
149 148 fveq2d x 1 +∞ ψ x + 1 - 1 = ψ x
150 chpfl x ψ x = ψ x
151 5 150 syl x 1 +∞ ψ x = ψ x
152 149 151 eqtrd x 1 +∞ ψ x + 1 - 1 = ψ x
153 152 oveq1d x 1 +∞ ψ x + 1 - 1 x + 1 - 1 = ψ x x + 1 - 1
154 19 recnd x 1 +∞ ψ x
155 26 nncnd x 1 +∞ x + 1
156 1cnd x 1 +∞ 1
157 154 155 156 subsub3d x 1 +∞ ψ x x + 1 - 1 = ψ x + 1 - x + 1
158 153 157 eqtrd x 1 +∞ ψ x + 1 - 1 x + 1 - 1 = ψ x + 1 - x + 1
159 158 oveq2d x 1 +∞ 1 x + 1 ψ x + 1 - 1 x + 1 - 1 = 1 x + 1 ψ x + 1 - x + 1
160 26 nnrecred x 1 +∞ 1 x + 1
161 160 recnd x 1 +∞ 1 x + 1
162 peano2cn ψ x ψ x + 1
163 154 162 syl x 1 +∞ ψ x + 1
164 161 163 155 subdid x 1 +∞ 1 x + 1 ψ x + 1 - x + 1 = 1 x + 1 ψ x + 1 1 x + 1 x + 1
165 26 nnne0d x 1 +∞ x + 1 0
166 163 155 165 divrec2d x 1 +∞ ψ x + 1 x + 1 = 1 x + 1 ψ x + 1
167 166 eqcomd x 1 +∞ 1 x + 1 ψ x + 1 = ψ x + 1 x + 1
168 155 165 recid2d x 1 +∞ 1 x + 1 x + 1 = 1
169 167 168 oveq12d x 1 +∞ 1 x + 1 ψ x + 1 1 x + 1 x + 1 = ψ x + 1 x + 1 1
170 159 164 169 3eqtrd x 1 +∞ 1 x + 1 ψ x + 1 - 1 x + 1 - 1 = ψ x + 1 x + 1 1
171 29 mul01i 1 0 = 0
172 171 a1i x 1 +∞ 1 0 = 0
173 170 172 oveq12d x 1 +∞ 1 x + 1 ψ x + 1 - 1 x + 1 - 1 1 0 = ψ x + 1 x + 1 - 1 - 0
174 31 subid1d x 1 +∞ ψ x + 1 x + 1 - 1 - 0 = ψ x + 1 x + 1 1
175 173 174 eqtrd x 1 +∞ 1 x + 1 ψ x + 1 - 1 x + 1 - 1 1 0 = ψ x + 1 x + 1 1
176 97 41 syl x 1 +∞ n 1 x n n + 1
177 176 nnrecred x 1 +∞ n 1 x 1 n n + 1
178 177 recnd x 1 +∞ n 1 x 1 n n + 1
179 97 38 syl x 1 +∞ n 1 x R n
180 179 recnd x 1 +∞ n 1 x R n
181 178 180 mulneg1d x 1 +∞ n 1 x 1 n n + 1 R n = 1 n n + 1 R n
182 98 112 mulcld x 1 +∞ n 1 x n 1
183 98 131 mulcld x 1 +∞ n 1 x n n + 1
184 176 nnne0d x 1 +∞ n 1 x n n + 1 0
185 131 182 183 184 divsubdird x 1 +∞ n 1 x n + 1 - n 1 n n + 1 = n + 1 n n + 1 n 1 n n + 1
186 98 mulid1d x 1 +∞ n 1 x n 1 = n
187 186 oveq2d x 1 +∞ n 1 x n + 1 - n 1 = n + 1 - n
188 187 134 eqtrd x 1 +∞ n 1 x n + 1 - n 1 = 1
189 188 oveq1d x 1 +∞ n 1 x n + 1 - n 1 n n + 1 = 1 n n + 1
190 131 mulid1d x 1 +∞ n 1 x n + 1 1 = n + 1
191 131 98 mulcomd x 1 +∞ n 1 x n + 1 n = n n + 1
192 190 191 oveq12d x 1 +∞ n 1 x n + 1 1 n + 1 n = n + 1 n n + 1
193 97 39 syl x 1 +∞ n 1 x n + 1
194 193 nnne0d x 1 +∞ n 1 x n + 1 0
195 112 98 131 142 194 divcan5d x 1 +∞ n 1 x n + 1 1 n + 1 n = 1 n
196 192 195 eqtr3d x 1 +∞ n 1 x n + 1 n n + 1 = 1 n
197 112 131 98 194 142 divcan5d x 1 +∞ n 1 x n 1 n n + 1 = 1 n + 1
198 196 197 oveq12d x 1 +∞ n 1 x n + 1 n n + 1 n 1 n n + 1 = 1 n 1 n + 1
199 185 189 198 3eqtr3d x 1 +∞ n 1 x 1 n n + 1 = 1 n 1 n + 1
200 199 negeqd x 1 +∞ n 1 x 1 n n + 1 = 1 n 1 n + 1
201 97 nnrecred x 1 +∞ n 1 x 1 n
202 201 recnd x 1 +∞ n 1 x 1 n
203 193 nnrecred x 1 +∞ n 1 x 1 n + 1
204 203 recnd x 1 +∞ n 1 x 1 n + 1
205 202 204 negsubdi2d x 1 +∞ n 1 x 1 n 1 n + 1 = 1 n + 1 1 n
206 200 205 eqtr2d x 1 +∞ n 1 x 1 n + 1 1 n = 1 n n + 1
207 97 nnrpd x 1 +∞ n 1 x n +
208 100 207 eqeltrd x 1 +∞ n 1 x n + 1 - 1 +
209 1 pntrval n + 1 - 1 + R n + 1 - 1 = ψ n + 1 - 1 n + 1 - 1
210 208 209 syl x 1 +∞ n 1 x R n + 1 - 1 = ψ n + 1 - 1 n + 1 - 1
211 100 fveq2d x 1 +∞ n 1 x R n + 1 - 1 = R n
212 210 211 eqtr3d x 1 +∞ n 1 x ψ n + 1 - 1 n + 1 - 1 = R n
213 206 212 oveq12d x 1 +∞ n 1 x 1 n + 1 1 n ψ n + 1 - 1 n + 1 - 1 = 1 n n + 1 R n
214 180 183 184 divrec2d x 1 +∞ n 1 x R n n n + 1 = 1 n n + 1 R n
215 214 negeqd x 1 +∞ n 1 x R n n n + 1 = 1 n n + 1 R n
216 181 213 215 3eqtr4d x 1 +∞ n 1 x 1 n + 1 1 n ψ n + 1 - 1 n + 1 - 1 = R n n n + 1
217 96 216 sumeq12rdv x 1 +∞ n 1 ..^ x + 1 1 n + 1 1 n ψ n + 1 - 1 n + 1 - 1 = n = 1 x R n n n + 1
218 fzfid x 1 +∞ 1 x Fin
219 97 42 syl x 1 +∞ n 1 x R n n n + 1
220 219 recnd x 1 +∞ n 1 x R n n n + 1
221 218 220 fsumneg x 1 +∞ n = 1 x R n n n + 1 = n = 1 x R n n n + 1
222 217 221 eqtrd x 1 +∞ n 1 ..^ x + 1 1 n + 1 1 n ψ n + 1 - 1 n + 1 - 1 = n = 1 x R n n n + 1
223 175 222 oveq12d x 1 +∞ 1 x + 1 ψ x + 1 - 1 x + 1 - 1 - 1 0 - n 1 ..^ x + 1 1 n + 1 1 n ψ n + 1 - 1 n + 1 - 1 = ψ x + 1 x + 1 - 1 - n = 1 x R n n n + 1
224 92 145 223 3eqtr3d x 1 +∞ n = 1 x Λ n 1 n = ψ x + 1 x + 1 - 1 - n = 1 x R n n n + 1
225 31 46 subnegd x 1 +∞ ψ x + 1 x + 1 - 1 - n = 1 x R n n n + 1 = ψ x + 1 x + 1 - 1 + n = 1 x R n n n + 1
226 224 225 eqtrd x 1 +∞ n = 1 x Λ n 1 n = ψ x + 1 x + 1 - 1 + n = 1 x R n n n + 1
227 31 46 226 mvrladdd x 1 +∞ n = 1 x Λ n 1 n ψ x + 1 x + 1 1 = n = 1 x R n n n + 1
228 227 mpteq2ia x 1 +∞ n = 1 x Λ n 1 n ψ x + 1 x + 1 1 = x 1 +∞ n = 1 x R n n n + 1
229 fzfid x + 1 x Fin
230 33 adantl x + n 1 x n
231 230 115 syl x + n 1 x Λ n
232 231 139 syl x + n 1 x Λ n 1
233 232 230 nndivred x + n 1 x Λ n 1 n
234 229 233 fsumrecl x + n = 1 x Λ n 1 n
235 rpre x + x
236 235 adantl x + x
237 236 18 syl x + ψ x
238 237 20 syl x + ψ x + 1
239 rprege0 x + x 0 x
240 239 23 syl x + x 0
241 240 adantl x + x 0
242 241 25 syl x + x + 1
243 238 242 nndivred x + ψ x + 1 x + 1
244 peano2rem ψ x + 1 x + 1 ψ x + 1 x + 1 1
245 243 244 syl x + ψ x + 1 x + 1 1
246 reex V
247 246 15 ssexi + V
248 247 a1i + V
249 231 230 nndivred x + n 1 x Λ n n
250 249 recnd x + n 1 x Λ n n
251 229 250 fsumcl x + n = 1 x Λ n n
252 relogcl x + log x
253 252 adantl x + log x
254 253 recnd x + log x
255 251 254 subcld x + n = 1 x Λ n n log x
256 230 nnrecred x + n 1 x 1 n
257 229 256 fsumrecl x + n = 1 x 1 n
258 257 253 resubcld x + n = 1 x 1 n log x
259 eqidd x + n = 1 x Λ n n log x = x + n = 1 x Λ n n log x
260 eqidd x + n = 1 x 1 n log x = x + n = 1 x 1 n log x
261 248 255 258 259 260 offval2 x + n = 1 x Λ n n log x f x + n = 1 x 1 n log x = x + n = 1 x Λ n n - log x - n = 1 x 1 n log x
262 256 recnd x + n 1 x 1 n
263 229 250 262 fsumsub x + n = 1 x Λ n n 1 n = n = 1 x Λ n n n = 1 x 1 n
264 231 recnd x + n 1 x Λ n
265 1cnd x + n 1 x 1
266 230 nncnd x + n 1 x n
267 230 nnne0d x + n 1 x n 0
268 264 265 266 267 divsubdird x + n 1 x Λ n 1 n = Λ n n 1 n
269 268 sumeq2dv x + n = 1 x Λ n 1 n = n = 1 x Λ n n 1 n
270 257 recnd x + n = 1 x 1 n
271 251 270 254 nnncan2d x + n = 1 x Λ n n - log x - n = 1 x 1 n log x = n = 1 x Λ n n n = 1 x 1 n
272 263 269 271 3eqtr4rd x + n = 1 x Λ n n - log x - n = 1 x 1 n log x = n = 1 x Λ n 1 n
273 272 mpteq2dva x + n = 1 x Λ n n - log x - n = 1 x 1 n log x = x + n = 1 x Λ n 1 n
274 261 273 eqtrd x + n = 1 x Λ n n log x f x + n = 1 x 1 n log x = x + n = 1 x Λ n 1 n
275 vmadivsum x + n = 1 x Λ n n log x 𝑂1
276 15 a1i +
277 258 recnd x + n = 1 x 1 n log x
278 1red 1
279 harmoniclbnd x + log x n = 1 x 1 n
280 279 adantl x + log x n = 1 x 1 n
281 253 257 280 abssubge0d x + n = 1 x 1 n log x = n = 1 x 1 n log x
282 281 adantrr x + 1 x n = 1 x 1 n log x = n = 1 x 1 n log x
283 235 ad2antrl x + 1 x x
284 simprr x + 1 x 1 x
285 harmonicubnd x 1 x n = 1 x 1 n log x + 1
286 283 284 285 syl2anc x + 1 x n = 1 x 1 n log x + 1
287 1red x + 1
288 257 253 287 lesubadd2d x + n = 1 x 1 n log x 1 n = 1 x 1 n log x + 1
289 288 adantrr x + 1 x n = 1 x 1 n log x 1 n = 1 x 1 n log x + 1
290 286 289 mpbird x + 1 x n = 1 x 1 n log x 1
291 282 290 eqbrtrd x + 1 x n = 1 x 1 n log x 1
292 276 277 278 278 291 elo1d x + n = 1 x 1 n log x 𝑂1
293 o1sub x + n = 1 x Λ n n log x 𝑂1 x + n = 1 x 1 n log x 𝑂1 x + n = 1 x Λ n n log x f x + n = 1 x 1 n log x 𝑂1
294 275 292 293 sylancr x + n = 1 x Λ n n log x f x + n = 1 x 1 n log x 𝑂1
295 274 294 eqeltrrd x + n = 1 x Λ n 1 n 𝑂1
296 243 recnd x + ψ x + 1 x + 1
297 1cnd x + 1
298 237 recnd x + ψ x
299 rpcnne0 x + x x 0
300 299 adantl x + x x 0
301 divdir ψ x 1 x x 0 ψ x + 1 x = ψ x x + 1 x
302 298 297 300 301 syl3anc x + ψ x + 1 x = ψ x x + 1 x
303 302 mpteq2dva x + ψ x + 1 x = x + ψ x x + 1 x
304 simpr x + x +
305 237 304 rerpdivcld x + ψ x x
306 rpreccl x + 1 x +
307 306 adantl x + 1 x +
308 eqidd x + ψ x x = x + ψ x x
309 eqidd x + 1 x = x + 1 x
310 248 305 307 308 309 offval2 x + ψ x x + f x + 1 x = x + ψ x x + 1 x
311 chpo1ub x + ψ x x 𝑂1
312 divrcnv 1 x + 1 x 0
313 29 312 ax-mp x + 1 x 0
314 rlimo1 x + 1 x 0 x + 1 x 𝑂1
315 313 314 mp1i x + 1 x 𝑂1
316 o1add x + ψ x x 𝑂1 x + 1 x 𝑂1 x + ψ x x + f x + 1 x 𝑂1
317 311 315 316 sylancr x + ψ x x + f x + 1 x 𝑂1
318 310 317 eqeltrrd x + ψ x x + 1 x 𝑂1
319 303 318 eqeltrd x + ψ x + 1 x 𝑂1
320 238 304 rerpdivcld x + ψ x + 1 x
321 chpge0 x 0 ψ x
322 236 321 syl x + 0 ψ x
323 237 322 ge0p1rpd x + ψ x + 1 +
324 323 rprege0d x + ψ x + 1 0 ψ x + 1
325 242 nnrpd x + x + 1 +
326 325 rpregt0d x + x + 1 0 < x + 1
327 divge0 ψ x + 1 0 ψ x + 1 x + 1 0 < x + 1 0 ψ x + 1 x + 1
328 324 326 327 syl2anc x + 0 ψ x + 1 x + 1
329 243 328 absidd x + ψ x + 1 x + 1 = ψ x + 1 x + 1
330 320 recnd x + ψ x + 1 x
331 330 abscld x + ψ x + 1 x
332 fllep1 x x x + 1
333 236 332 syl x + x x + 1
334 rpregt0 x + x 0 < x
335 334 adantl x + x 0 < x
336 323 rpregt0d x + ψ x + 1 0 < ψ x + 1
337 lediv2 x 0 < x x + 1 0 < x + 1 ψ x + 1 0 < ψ x + 1 x x + 1 ψ x + 1 x + 1 ψ x + 1 x
338 335 326 336 337 syl3anc x + x x + 1 ψ x + 1 x + 1 ψ x + 1 x
339 333 338 mpbid x + ψ x + 1 x + 1 ψ x + 1 x
340 320 leabsd x + ψ x + 1 x ψ x + 1 x
341 243 320 331 339 340 letrd x + ψ x + 1 x + 1 ψ x + 1 x
342 329 341 eqbrtrd x + ψ x + 1 x + 1 ψ x + 1 x
343 342 adantrr x + 1 x ψ x + 1 x + 1 ψ x + 1 x
344 278 319 320 296 343 o1le x + ψ x + 1 x + 1 𝑂1
345 o1const + 1 x + 1 𝑂1
346 15 29 345 mp2an x + 1 𝑂1
347 346 a1i x + 1 𝑂1
348 296 297 344 347 o1sub2 x + ψ x + 1 x + 1 1 𝑂1
349 234 245 295 348 o1sub2 x + n = 1 x Λ n 1 n ψ x + 1 x + 1 1 𝑂1
350 14 349 o1res2 x 1 +∞ n = 1 x Λ n 1 n ψ x + 1 x + 1 1 𝑂1
351 228 350 eqeltrrid x 1 +∞ n = 1 x R n n n + 1 𝑂1
352 17 351 eqeltrd x n = 1 x R n n n + 1 1 +∞ 𝑂1
353 eqid x n = 1 x R n n n + 1 = x n = 1 x R n n n + 1
354 353 45 fmpti x n = 1 x R n n n + 1 :
355 354 a1i x n = 1 x R n n n + 1 :
356 ssidd
357 355 356 278 o1resb x n = 1 x R n n n + 1 𝑂1 x n = 1 x R n n n + 1 1 +∞ 𝑂1
358 352 357 mpbird x n = 1 x R n n n + 1 𝑂1
359 358 mptru x n = 1 x R n n n + 1 𝑂1