Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pntibndlem2 Structured version   Visualization version   Unicode version

Theorem pntibndlem2 24508
 Description: Lemma for pntibnd 24510. The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
Hypotheses
Ref Expression
pntibnd.r ψ
pntibndlem1.1
pntibndlem1.l
pntibndlem3.2
pntibndlem3.3
pntibndlem3.k
pntibndlem3.c
pntibndlem3.4
pntibndlem3.6
pntibndlem2.10
pntibndlem2.5
pntibndlem2.6 ψ ψ
pntibndlem2.7
pntibndlem2.8
pntibndlem2.9
pntibndlem2.11
Assertion
Ref Expression
pntibndlem2
Distinct variable groups:   ,,,,,   ,,,   ,,,,,   ,,   ,,,   ,,,,   ,   ,,   ,   ,,,   ,
Allowed substitution hints:   (,,,)   (,,)   (,,,,)   (,)   ()   (,,)   (,,,,)   (,)   (,,,)   (,,,,)   (,,,)   (,)

Proof of Theorem pntibndlem2
StepHypRef Expression
1 pntibndlem2.10 . . 3
21nnrpd 11362 . 2
3 pntibndlem2.11 . . . . 5
43simpld 466 . . . 4
54simpld 466 . . 3
6 1red 9676 . . . . . 6
7 ioossre 11721 . . . . . . . 8
8 pntibnd.r . . . . . . . . 9 ψ
9 pntibndlem1.1 . . . . . . . . 9
10 pntibndlem1.l . . . . . . . . 9
118, 9, 10pntibndlem1 24506 . . . . . . . 8
127, 11sseldi 3416 . . . . . . 7
13 pntibndlem3.4 . . . . . . . 8
147, 13sseldi 3416 . . . . . . 7
1512, 14remulcld 9689 . . . . . 6
166, 15readdcld 9688 . . . . 5
171nnred 10646 . . . . 5
1816, 17remulcld 9689 . . . 4
19 2re 10701 . . . . 5
20 remulcl 9642 . . . . 5
2119, 17, 20sylancr 676 . . . 4
22 pntibndlem3.c . . . . . . . . . 10
23 pntibndlem3.3 . . . . . . . . . . . . 13
2423rpred 11364 . . . . . . . . . . . 12
25 remulcl 9642 . . . . . . . . . . . 12
2619, 24, 25sylancr 676 . . . . . . . . . . 11
27 2rp 11330 . . . . . . . . . . . . 13
2827a1i 11 . . . . . . . . . . . 12
2928relogcld 23651 . . . . . . . . . . 11
3026, 29readdcld 9688 . . . . . . . . . 10
3122, 30syl5eqel 2553 . . . . . . . . 9
32 eliooord 11719 . . . . . . . . . . . 12
3313, 32syl 17 . . . . . . . . . . 11
3433simpld 466 . . . . . . . . . 10
3514, 34elrpd 11361 . . . . . . . . 9
3631, 35rerpdivcld 11392 . . . . . . . 8
3736reefcld 14219 . . . . . . 7
38 pnfxr 11435 . . . . . . 7
39 icossre 11740 . . . . . . 7
4037, 38, 39sylancl 675 . . . . . 6
41 pntibndlem2.8 . . . . . 6
4240, 41sseldd 3419 . . . . 5
43 ioossre 11721 . . . . . 6
44 pntibndlem2.9 . . . . . 6
4543, 44sseldi 3416 . . . . 5
4642, 45remulcld 9689 . . . 4
4719a1i 11 . . . . 5
48 eliooord 11719 . . . . . . . . . . . . 13
4911, 48syl 17 . . . . . . . . . . . 12
5049simpld 466 . . . . . . . . . . 11
5112, 50elrpd 11361 . . . . . . . . . 10
5251rpge0d 11368 . . . . . . . . 9
5349simprd 470 . . . . . . . . 9
5435rpge0d 11368 . . . . . . . . 9
5533simprd 470 . . . . . . . . 9
5612, 6, 14, 6, 52, 53, 54, 55ltmul12ad 10570 . . . . . . . 8
57 1t1e1 10780 . . . . . . . 8
5856, 57syl6breq 4435 . . . . . . 7
5915, 6, 6, 58ltadd2dd 9811 . . . . . 6
60 df-2 10690 . . . . . 6
6159, 60syl6breqr 4436 . . . . 5
6216, 47, 2, 61ltmul1dd 11416 . . . 4
634simprd 470 . . . . . 6
6442recnd 9687 . . . . . . 7
6545recnd 9687 . . . . . . 7
66 rpcnne0 11342 . . . . . . . 8
6727, 66mp1i 13 . . . . . . 7
68 div23 10311 . . . . . . 7
6964, 65, 67, 68syl3anc 1292 . . . . . 6
7063, 69breqtrrd 4422 . . . . 5
7117, 46, 28lemuldiv2d 11411 . . . . 5
7270, 71mpbird 240 . . . 4
7318, 21, 46, 62, 72ltletrd 9812 . . 3
74 pntibndlem3.2 . . . . . . . . . . . 12
75 pntibndlem3.k . . . . . . . . . . . 12
768, 9, 10, 74, 23, 75, 22, 13, 9, 1pntibndlem2a 24507 . . . . . . . . . . 11
7776simp1d 1042 . . . . . . . . . 10
782adantr 472 . . . . . . . . . 10
7976simp2d 1043 . . . . . . . . . 10
8077, 78, 79rpgecld 11400 . . . . . . . . 9
818pntrf 24480 . . . . . . . . . 10
8281ffvelrni 6036 . . . . . . . . 9
8380, 82syl 17 . . . . . . . 8
8483, 80rerpdivcld 11392 . . . . . . 7
8584recnd 9687 . . . . . 6
8685abscld 13575 . . . . 5
8781ffvelrni 6036 . . . . . . . . . . . 12
882, 87syl 17 . . . . . . . . . . 11
8988, 1nndivred 10680 . . . . . . . . . 10
9089adantr 472 . . . . . . . . 9
9190recnd 9687 . . . . . . . 8
9285, 91subcld 10005 . . . . . . 7
9392abscld 13575 . . . . . 6
9491abscld 13575 . . . . . 6
9593, 94readdcld 9688 . . . . 5
9614adantr 472 . . . . 5
9785, 91abs2difd 13596 . . . . . 6
9886, 94, 93lesubaddd 10231 . . . . . 6
9997, 98mpbid 215 . . . . 5
10096rehalfcld 10882 . . . . . . 7
10117adantr 472 . . . . . . . . . . . 12
10277, 101resubcld 10068 . . . . . . . . . . 11
103102, 78rerpdivcld 11392 . . . . . . . . . 10
104 3re 10705 . . . . . . . . . . . 12
105104a1i 11 . . . . . . . . . . 11
10686, 105readdcld 9688 . . . . . . . . . 10
107103, 106remulcld 9689 . . . . . . . . 9
108 pntibndlem2.5 . . . . . . . . . . . 12
109108rpred 11364 . . . . . . . . . . 11
110109adantr 472 . . . . . . . . . 10
111 1red 9676 . . . . . . . . . . . 12
112 4nn 10792 . . . . . . . . . . . . . . . . . 18
113 nnrp 11334 . . . . . . . . . . . . . . . . . 18
114112, 113mp1i 13 . . . . . . . . . . . . . . . . 17
11535, 114rpdivcld 11381 . . . . . . . . . . . . . . . 16
116108, 115rpdivcld 11381 . . . . . . . . . . . . . . 15
117116rpred 11364 . . . . . . . . . . . . . 14
118117reefcld 14219 . . . . . . . . . . . . 13
119118adantr 472 . . . . . . . . . . . 12
120 efgt1 14247 . . . . . . . . . . . . . 14
121116, 120syl 17 . . . . . . . . . . . . 13
122121adantr 472 . . . . . . . . . . . 12
123 pntibndlem2.7 . . . . . . . . . . . . . . . 16
124 pntibndlem3.6 . . . . . . . . . . . . . . . . . 18
125124rpred 11364 . . . . . . . . . . . . . . . . 17
126118, 125readdcld 9688 . . . . . . . . . . . . . . . 16
127123, 126syl5eqel 2553 . . . . . . . . . . . . . . 15
128118, 124ltaddrpd 11394 . . . . . . . . . . . . . . . 16
129128, 123syl6breqr 4436 . . . . . . . . . . . . . . 15
130 eliooord 11719 . . . . . . . . . . . . . . . . 17
13144, 130syl 17 . . . . . . . . . . . . . . . 16
132131simpld 466 . . . . . . . . . . . . . . 15
133118, 127, 45, 129, 132lttrd 9813 . . . . . . . . . . . . . 14
134118, 45, 17, 133, 5lttrd 9813 . . . . . . . . . . . . 13
135134adantr 472 . . . . . . . . . . . 12
136111, 119, 101, 122, 135lttrd 9813 . . . . . . . . . . 11
137101, 136rplogcld 23657 . . . . . . . . . 10
138110, 137rerpdivcld 11392 . . . . . . . . 9
139107, 138readdcld 9688 . . . . . . . 8
140 peano2re 9824 . . . . . . . . . . . 12
14186, 140syl 17 . . . . . . . . . . 11
142103, 141remulcld 9689 . . . . . . . . . 10
143 chpcl 24130 . . . . . . . . . . . . 13 ψ
14477, 143syl 17 . . . . . . . . . . . 12 ψ
145 chpcl 24130 . . . . . . . . . . . . 13 ψ
146101, 145syl 17 . . . . . . . . . . . 12 ψ
147144, 146resubcld 10068 . . . . . . . . . . 11 ψ ψ
148147, 78rerpdivcld 11392 . . . . . . . . . 10 ψ ψ
149142, 148readdcld 9688 . . . . . . . . 9 ψ ψ
150103, 86remulcld 9689 . . . . . . . . . . 11
15188adantr 472 . . . . . . . . . . . . . . 15
15283, 151resubcld 10068 . . . . . . . . . . . . . 14
153152recnd 9687 . . . . . . . . . . . . 13
154153abscld 13575 . . . . . . . . . . . 12
155154, 78rerpdivcld 11392 . . . . . . . . . . 11
156150, 155readdcld 9688 . . . . . . . . . 10
157103, 84remulcld 9689 . . . . . . . . . . . . . 14
158157renegcld 10067 . . . . . . . . . . . . 13
159158recnd 9687 . . . . . . . . . . . 12
160152, 78rerpdivcld 11392 . . . . . . . . . . . . 13
161160recnd 9687 . . . . . . . . . . . 12
162159, 161abstrid 13595 . . . . . . . . . . 11
16377recnd 9687 . . . . . . . . . . . . . . . . . . . 20
164101recnd 9687 . . . . . . . . . . . . . . . . . . . 20
16578rpne0d 11369 . . . . . . . . . . . . . . . . . . . 20
166163, 164, 164, 165divsubdird 10444 . . . . . . . . . . . . . . . . . . 19
167164, 165dividd 10403 . . . . . . . . . . . . . . . . . . . 20
168167oveq2d 6324 . . . . . . . . . . . . . . . . . . 19
169166, 168eqtrd 2505 . . . . . . . . . . . . . . . . . 18
170169oveq1d 6323 . . . . . . . . . . . . . . . . 17
17177, 78rerpdivcld 11392 . . . . . . . . . . . . . . . . . . 19
172171recnd 9687 . . . . . . . . . . . . . . . . . 18
173 1cnd 9677 . . . . . . . . . . . . . . . . . 18
174172, 173, 85subdird 10096 . . . . . . . . . . . . . . . . 17
17580rpcnne0d 11373 . . . . . . . . . . . . . . . . . . 19
17678rpcnne0d 11373 . . . . . . . . . . . . . . . . . . 19
17783recnd 9687 . . . . . . . . . . . . . . . . . . 19
178 dmdcan 10339 . . . . . . . . . . . . . . . . . . 19
179175, 176, 177, 178syl3anc 1292 . . . . . . . . . . . . . . . . . 18
18085mulid2d 9679 . . . . . . . . . . . . . . . . . 18
181179, 180oveq12d 6326 . . . . . . . . . . . . . . . . 17
182170, 174, 1813eqtrd 2509 . . . . . . . . . . . . . . . 16
183182negeqd 9889 . . . . . . . . . . . . . . 15
18483, 78rerpdivcld 11392 . . . . . . . . . . . . . . . . 17
185184recnd 9687 . . . . . . . . . . . . . . . 16
186185, 85negsubdi2d 10021 . . . . . . . . . . . . . . 15
187183, 186eqtrd 2505 . . . . . . . . . . . . . 14
188151recnd 9687 . . . . . . . . . . . . . . 15
189177, 188, 164, 165divsubdird 10444 . . . . . . . . . . . . . 14
190187, 189oveq12d 6326 . . . . . . . . . . . . 13
19185, 185, 91npncand 10029 . . . . . . . . . . . . 13
192190, 191eqtrd 2505 . . . . . . . . . . . 12
193192fveq2d 5883 . . . . . . . . . . 11
194157recnd 9687 . . . . . . . . . . . . . 14
195194absnegd 13588 . . . . . . . . . . . . 13
196103recnd 9687 . . . . . . . . . . . . . 14
197196, 85absmuld 13593 . . . . . . . . . . . . 13
19877, 101subge0d 10224 . . . . . . . . . . . . . . . . 17
19979, 198mpbird 240 . . . . . . . . . . . . . . . 16
200102, 78, 199divge0d 11401 . . . . . . . . . . . . . . 15
201103, 200absidd 13561 . . . . . . . . . . . . . 14
202201oveq1d 6323 . . . . . . . . . . . . 13
203195, 197, 2023eqtrd 2509 . . . . . . . . . . . 12
204153, 164, 165absdivd 13594 . . . . . . . . . . . . 13
20578rprege0d 11371 . . . . . . . . . . . . . . 15
206 absid 13436 . . . . . . . . . . . . . . 15
207205, 206syl 17 . . . . . . . . . . . . . 14
208207oveq2d 6324 . . . . . . . . . . . . 13
209204, 208eqtrd 2505 . . . . . . . . . . . 12
210203, 209oveq12d 6326 . . . . . . . . . . 11
211162, 193, 2103brtr3d 4425 . . . . . . . . . 10
212102, 147readdcld 9688 . . . . . . . . . . . . 13 ψ ψ
213212, 78rerpdivcld 11392 . . . . . . . . . . . 12 ψ ψ
214147recnd 9687 . . . . . . . . . . . . . . 15 ψ ψ
215164, 163subcld 10005 . . . . . . . . . . . . . . 15
216214, 215abstrid 13595 . . . . . . . . . . . . . 14 ψ ψ ψ ψ
2178pntrval 24479 . . . . . . . . . . . . . . . . . 18 ψ
21880, 217syl 17 . . . . . . . . . . . . . . . . 17 ψ
2198pntrval 24479 . . . . . . . . . . . . . . . . . 18 ψ
22078, 219syl 17 . . . . . . . . . . . . . . . . 17 ψ
221218, 220oveq12d 6326 . . . . . . . . . . . . . . . 16 ψ ψ
222144recnd 9687 . . . . . . . . . . . . . . . . 17 ψ
223146recnd 9687 . . . . . . . . . . . . . . . . 17 ψ
224 subadd4 9938 . . . . . . . . . . . . . . . . . 18 ψ ψ ψ ψ ψ ψ
225 sub4 9939 . . . . . . . . . . . . . . . . . 18 ψ ψ ψ ψ ψ ψ
226 addsub4 9937 . . . . . . . . . . . . . . . . . . 19 ψ ψ ψ ψ ψ ψ
227226an42s 843 . . . . . . . . . . . . . . . . . 18 ψ ψ ψ ψ ψ ψ
228224, 225, 2273eqtr3d 2513 . . . . . . . . . . . . . . . . 17 ψ ψ ψ ψ ψ ψ
229222, 223, 163, 164, 228syl22anc 1293 . . . . . . . . . . . . . . . 16 ψ ψ ψ ψ
230221, 229eqtr2d 2506 . . . . . . . . . . . . . . 15 ψ ψ
231230fveq2d 5883 . . . . . . . . . . . . . 14 ψ ψ
232 chpwordi 24163 . . . . . . . . . . . . . . . . . 18 ψ ψ
233101, 77, 79, 232syl3anc 1292 . . . . . . . . . . . . . . . . 17 ψ ψ
234146, 144, 233abssubge0d 13570 . . . . . . . . . . . . . . . 16 ψ ψ ψ ψ
235101, 77, 79abssuble0d 13571 . . . . . . . . . . . . . . . 16
236234, 235oveq12d 6326 . . . . . . . . . . . . . . 15 ψ ψ ψ ψ
237102recnd 9687 . . . . . . . . . . . . . . . 16
238214, 237addcomd 9853 . . . . . . . . . . . . . . 15 ψ ψ ψ ψ
239236, 238eqtrd 2505 . . . . . . . . . . . . . 14 ψ ψ ψ ψ
240216, 231, 2393brtr3d 4425 . . . . . . . . . . . . 13 ψ ψ
241154, 212, 78, 240lediv1dd 11419 . . . . . . . . . . . 12 ψ ψ
242155, 213, 150, 241leadd2dd 10249 . . . . . . . . . . 11 ψ ψ
243150recnd 9687 . . . . . . . . . . . . 13
244148recnd 9687 . . . . . . . . . . . . 13 ψ ψ
245243, 196, 244addassd 9683 . . . . . . . . . . . 12 ψ ψ ψ ψ
24686recnd 9687 . . . . . . . . . . . . . . 15
247196, 246, 173adddid 9685 . . . . . . . . . . . . . 14
248196mulid1d 9678 . . . . . . . . . . . . . . 15
249248oveq2d 6324 . . . . . . . . . . . . . 14
250247, 249eqtrd 2505 . . . . . . . . . . . . 13
251250oveq1d 6323 . . . . . . . . . . . 12 ψ ψ ψ ψ
252237, 214, 164, 165divdird 10443 . . . . . . . . . . . . 13 ψ ψ ψ ψ
253252oveq2d 6324 . . . . . . . . . . . 12 ψ ψ ψ ψ
254245, 251, 2533eqtr4d 2515 . . . . . . . . . . 11 ψ ψ ψ ψ
255242, 254breqtrrd 4422 . . . . . . . . . 10 ψ ψ
25693, 156, 149, 211, 255letrd 9809 . . . . . . . . 9 ψ ψ
257 remulcl 9642 . . . . . . . . . . . . 13
25819, 103, 257sylancr 676 . . . . . . . . . . . 12
259258, 138readdcld 9688 . . . . . . . . . . 11
260 remulcl 9642 . . . . . . . . . . . . . . 15
26119, 102, 260sylancr 676 . . . . . . . . . . . . . 14
262101, 137rerpdivcld 11392 . . . . . . . . . . . . . . 15
263110, 262remulcld 9689 . . . . . . . . . . . . . 14
264261, 263readdcld 9688 . . . . . . . . . . . . 13
26518adantr 472 . . . . . . . . . . . . . . . 16
26621adantr 472 . . . . . . . . . . . . . . . 16
26776simp3d 1044 . . . . . . . . . . . . . . . 16
268 ltle 9740 . . . . . . . . . . . . . . . . . . . 20
26916, 19, 268sylancl 675 . . . . . . . . . . . . . . . . . . 19
27061, 269mpd 15 . . . . . . . . . . . . . . . . . 18
271270adantr 472 . . . . . . . . . . . . . . . . 17
27216adantr 472 . . . . . . . . . . . . . . . . . 18
27319a1i 11 . . . . . . . . . . . . . . . . . 18
274272, 273, 78lemul1d 11404 . . . . . . . . . . . . . . . . 17
275271, 274mpbid 215 . . . . . . . . . . . . . . . 16
27677, 265, 266, 267, 275letrd 9809 . . . . . . . . . . . . . . 15
277 elicc2 11724 . . . . . . . . . . . . . . . 16
278101, 266, 277syl2anc 673 . . . . . . . . . . . . . . 15
27977, 79, 276, 278mpbir3and 1213 . . . . . . . . . . . . . 14
280 1re 9660 . . . . . . . . . . . . . . . . . 18
281280rexri 9711 . . . . . . . . . . . . . . . . 17
282 elioopnf 11753 . . . . . . . . . . . . . . . . 17
283281, 282ax-mp 5 . . . . . . . . . . . . . . . 16
284101, 136, 283sylanbrc 677 . . . . . . . . . . . . . . 15
285 pntibndlem2.6 . . . . . . . . . . . . . . . 16 ψ ψ
286285adantr 472 . . . . . . . . . . . . . . 15 ψ ψ
287 id 22 . . . . . . . . . . . . . . . . . 18
288 oveq2 6316 . . . . . . . . . . . . . . . . . 18
289287, 288oveq12d 6326 . . . . . . . . . . . . . . . . 17
290 fveq2 5879 . . . . . . . . . . . . . . . . . . 19 ψ ψ
291290oveq2d 6324 . . . . . . . . . . . . . . . . . 18 ψ ψ ψ ψ
292 oveq2 6316 . . . . . . . . . . . . . . . . . . . 20
293292oveq2d 6324 . . . . . . . . . . . . . . . . . . 19
294 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21
295287, 294oveq12d 6326 . . . . . . . . . . . . . . . . . . . 20
296295oveq2d 6324 . . . . . . . . . . . . . . . . . . 19
297293, 296oveq12d 6326 . . . . . . . . . . . . . . . . . 18
298291, 297breq12d 4408 . . . . . . . . . . . . . . . . 17 ψ ψ ψ ψ
299289, 298raleqbidv 2987 . . . . . . . . . . . . . . . 16 ψ ψ ψ ψ
300299rspcv 3132 . . . . . . . . . . . . . . 15 ψ ψ ψ ψ
301284, 286, 300sylc 61 . . . . . . . . . . . . . 14 ψ ψ
302 fveq2 5879 . . . . . . . . . . . . . . . . 17 ψ ψ
303302oveq1d 6323 . . . . . . . . . . . . . . . 16 ψ ψ ψ ψ
304 oveq1 6315 . . . . . . . . . . . . . . . . . 18
305304oveq2d 6324 . . . . . . . . . . . . . . . . 17
306305oveq1d 6323 . . . . . . . . . . . . . . . 16
307303, 306breq12d 4408 . . . . . . . . . . . . . . 15 ψ ψ ψ ψ
308307rspcv 3132 . . . . . . . . . . . . . 14 ψ ψ ψ ψ
309279, 301, 308sylc 61 . . . . . . . . . . . . 13 ψ ψ
310147, 264, 78, 309lediv1dd 11419 . . . . . . . . . . . 12 ψ ψ
311261recnd 9687 . . . . . . . . . . . . . 14
312108adantr 472 . . . . . . . . . . . . . . . . 17
313312rpred 11364 . . . . . . . . . . . . . . . 16
314313, 262remulcld 9689 . . . . . . . . . . . . . . 15
315314recnd 9687 . . . . . . . . . . . . . 14
316 divdir 10315 . . . . . . . . . . . . . 14
317311, 315, 176, 316syl3anc 1292 . . . . . . . . . . . . 13
318 2cnd 10704 . . . . . . . . . . . . . . 15
319318, 237, 164, 165divassd 10440 . . . . . . . . . . . . . 14
320110recnd 9687 . . . . . . . . . . . . . . . . 17
321137rpcnne0d 11373 . . . . . . . . . . . . . . . . 17
322 div12 10314 . . . . . . . . . . . . . . . . 17
323320, 164, 321, 322syl3anc 1292 . . . . . . . . . . . . . . . 16
324323oveq1d 6323 . . . . . . . . . . . . . . 15
325312, 137rpdivcld 11381 . . . . . . . . . . . . . . . . 17
326325rpcnd 11366 . . . . . . . . . . . . . . . 16
327326, 164, 165divcan3d 10410 . . . . . . . . . . . . . . 15
328324, 327eqtrd 2505 . . . . . . . . . . . . . 14
329319, 328oveq12d 6326 . . . . . . . . . . . . 13
330317, 329eqtrd 2505 . . . . . . . . . . . 12
331310, 330breqtrd 4420 . . . . . . . . . . 11 ψ ψ
332148, 259, 142, 331leadd2dd 10249 . . . . . . . . . 10 ψ ψ
333142recnd 9687 . . . . . . . . . . . 12
334258recnd 9687 . . . . . . . . . . . 12
335138recnd 9687 . . . . . . . . . . . 12
336333, 334, 335addassd 9683 . . . . . . . . . . 11
337 2cn 10702 . . . . . . . . . . . . . . 15
338 mulcom 9643 . . . . . . . . . . . . . . 15
339337, 196, 338sylancr 676 . . . . . . . . . . . . . 14
340339oveq2d 6324 . . . . . . . . . . . . 13
341141recnd 9687 . . . . . . . . . . . . . 14
342196, 341, 318adddid 9685 . . . . . . . . . . . . 13
343246, 173, 318addassd 9683 . . . . . . . . . . . . . . 15
344 1p2e3 10757 . . . . . . . . . . . . . . . 16
345344oveq2i 6319 . . . . . . . . . . . . . . 15
346343, 345syl6eq 2521 . . . . . . . . . . . . . 14
347346oveq2d 6324 . . . . . . . . . . . . 13
348340, 342, 3473eqtr2d 2511 . . . . . . . . . . . 12
349348oveq1d 6323 . . . . . . . . . . 11
350336, 349eqtr3d 2507 . . . . . . . . . 10
351332, 350breqtrd 4420 . . . . . . . . 9 ψ ψ
35293, 149, 139, 256, 351letrd 9809 . . . . . . . 8
353100rehalfcld 10882 . . . . . . . . . 10
35477, 272, 78ledivmul2d 11415 . . . . . . . . . . . . . . . 16
355267, 354mpbird 240 . . . . . . . . . . . . . . 15
356 ax-1cn 9615 . . . . . . . . . . . . . . . 16
35715adantr 472 . . . . . . . . . . . . . . . . 17
358357recnd 9687 . . . . . . . . . . . . . . . 16
359 addcom 9837 . . . . . . . . . . . . . . . 16
360356, 358, 359sylancr 676 . . . . . . . . . . . . . . 15
361355, 360breqtrd 4420 . . . . . . . . . . . . . 14
362171, 111, 357lesubaddd 10231 . . . . . . . . . . . . . 14
363361, 362mpbird 240 . . . . . . . . . . . . 13
364169, 363eqbrtrd 4416 . . . . . . . . . . . 12