Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem79 Structured version   Unicode version

Theorem fourierdlem79 31857
 Description: projects every interval of the partition induced by on into a corresponding interval of the partition induced by on . (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem79.t
fourierdlem79.p ..^
fourierdlem79.m
fourierdlem79.q
fourierdlem79.c
fourierdlem79.d
fourierdlem79.cltd
fourierdlem79.o ..^
fourierdlem79.h
fourierdlem79.n
fourierdlem79.s
fourierdlem79.e
fourierdlem79.l
fourierdlem79.z
fourierdlem79.i ..^
Assertion
Ref Expression
fourierdlem79 ..^
Distinct variable groups:   ,,,   ,,,   ,,,   ,   ,,,   ,,   ,   ,,,   ,   ,,,   ,   ,   ,,,   ,   ,   ,   ,   ,,,   ,,   ,,,   ,,   ,   ,,,   ,,   ,   ,,   ,,,,   ,   ,   ,,,   ,   ,   ,,,   ,,   ,,   ,,,   ,
Allowed substitution hints:   (,)   (,)   ()   (,,,)   (,,,)   (,,,,,,,)   (,)   (,)   (,,,,)   (,,)   (,,,,,)   (,,,)   (,,,,,)   (,,)   ()   (,,,,,,,)   (,,,,,)

Proof of Theorem fourierdlem79
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fourierdlem79.q . . . . . . . 8
2 fourierdlem79.m . . . . . . . . 9
3 fourierdlem79.p . . . . . . . . . 10 ..^
43fourierdlem2 31780 . . . . . . . . 9 ..^
52, 4syl 16 . . . . . . . 8 ..^
61, 5mpbid 210 . . . . . . 7 ..^
76simpld 459 . . . . . 6
8 elmapi 7442 . . . . . 6
97, 8syl 16 . . . . 5
109adantr 465 . . . 4 ..^
11 fourierdlem79.t . . . . . . . . 9
12 fourierdlem79.e . . . . . . . . 9
13 fourierdlem79.l . . . . . . . . 9
14 fourierdlem79.i . . . . . . . . 9 ..^
153, 2, 1, 11, 12, 13, 14fourierdlem37 31815 . . . . . . . 8 ..^ ..^ ..^
1615simpld 459 . . . . . . 7 ..^
17 fzossfz 11827 . . . . . . . 8 ..^
1817a1i 11 . . . . . . 7 ..^
1916, 18fssd 5730 . . . . . 6
2019adantr 465 . . . . 5 ..^
21 fourierdlem79.c . . . . . . . . . . . . 13
22 fourierdlem79.d . . . . . . . . . . . . 13
23 fourierdlem79.cltd . . . . . . . . . . . . 13
24 fourierdlem79.o . . . . . . . . . . . . 13 ..^
25 fourierdlem79.h . . . . . . . . . . . . 13
26 fourierdlem79.n . . . . . . . . . . . . 13
27 fourierdlem79.s . . . . . . . . . . . . 13
2811, 3, 2, 1, 21, 22, 23, 24, 25, 26, 27fourierdlem54 31832 . . . . . . . . . . . 12
2928simpld 459 . . . . . . . . . . 11
3029simprd 463 . . . . . . . . . 10
3130adantr 465 . . . . . . . . 9 ..^
3229simpld 459 . . . . . . . . . . 11
3332adantr 465 . . . . . . . . . 10 ..^
3424fourierdlem2 31780 . . . . . . . . . 10 ..^
3533, 34syl 16 . . . . . . . . 9 ..^ ..^
3631, 35mpbid 210 . . . . . . . 8 ..^ ..^
3736simpld 459 . . . . . . 7 ..^
38 elmapi 7442 . . . . . . 7
3937, 38syl 16 . . . . . 6 ..^
40 elfzofz 11824 . . . . . . 7 ..^
4140adantl 466 . . . . . 6 ..^
4239, 41ffvelrnd 6017 . . . . 5 ..^
4320, 42ffvelrnd 6017 . . . 4 ..^
4410, 43ffvelrnd 6017 . . 3 ..^
4544rexrd 9646 . 2 ..^
4616adantr 465 . . . . . 6 ..^ ..^
4746, 42ffvelrnd 6017 . . . . 5 ..^ ..^
48 fzofzp1 11890 . . . . 5 ..^
4947, 48syl 16 . . . 4 ..^
5010, 49ffvelrnd 6017 . . 3 ..^
5150rexrd 9646 . 2 ..^
5214a1i 11 . . . . 5 ..^ ..^
53 fveq2 5856 . . . . . . . . . 10
5453fveq2d 5860 . . . . . . . . 9
5554breq2d 4449 . . . . . . . 8
5655rabbidv 3087 . . . . . . 7 ..^ ..^
5756supeq1d 7908 . . . . . 6 ..^ ..^
5857adantl 466 . . . . 5 ..^ ..^ ..^
59 ltso 9668 . . . . . . 7
6059supex 7925 . . . . . 6 ..^
6160a1i 11 . . . . 5 ..^ ..^
6252, 58, 42, 61fvmptd 5946 . . . 4 ..^ ..^
6362fveq2d 5860 . . 3 ..^ ..^
64 simpl 457 . . . . . . 7 ..^
6564, 42jca 532 . . . . . 6 ..^
66 eleq1 2515 . . . . . . . . 9
6766anbi2d 703 . . . . . . . 8
6857, 56eleq12d 2525 . . . . . . . 8 ..^ ..^ ..^ ..^
6967, 68imbi12d 320 . . . . . . 7 ..^ ..^ ..^ ..^
7015simprd 463 . . . . . . . 8 ..^ ..^
7170imp 429 . . . . . . 7 ..^ ..^
7269, 71vtoclg 3153 . . . . . 6 ..^ ..^
7342, 65, 72sylc 60 . . . . 5 ..^ ..^ ..^
74 nfrab1 3024 . . . . . . 7 ..^
75 nfcv 2605 . . . . . . 7
76 nfcv 2605 . . . . . . 7
7774, 75, 76nfsup 7913 . . . . . 6 ..^
78 nfcv 2605 . . . . . 6 ..^
79 nfcv 2605 . . . . . . . 8
8079, 77nffv 5863 . . . . . . 7 ..^
81 nfcv 2605 . . . . . . 7
82 nfcv 2605 . . . . . . 7
8380, 81, 82nfbr 4481 . . . . . 6 ..^
84 fveq2 5856 . . . . . . 7 ..^ ..^
8584breq1d 4447 . . . . . 6 ..^ ..^
8677, 78, 83, 85elrabf 3241 . . . . 5 ..^ ..^ ..^ ..^ ..^
8773, 86sylib 196 . . . 4 ..^ ..^ ..^ ..^
8887simprd 463 . . 3 ..^ ..^
8963, 88eqbrtrd 4457 . 2 ..^
902ad2antrr 725 . . . . 5 ..^
911ad2antrr 725 . . . . 5 ..^
9221ad2antrr 725 . . . . 5 ..^
9322ad2antrr 725 . . . . 5 ..^
9423ad2antrr 725 . . . . 5 ..^
95 0le1 10083 . . . . . . . 8
9695a1i 11 . . . . . . 7
972nnge1d 10585 . . . . . . 7
98 1zzd 10902 . . . . . . . 8
99 0zd 10883 . . . . . . . 8
1002nnzd 10974 . . . . . . . 8
101 elfz 11688 . . . . . . . 8
10298, 99, 100, 101syl3anc 1229 . . . . . . 7
10396, 97, 102mpbir2and 922 . . . . . 6
104103ad2antrr 725 . . . . 5 ..^
105 simplr 755 . . . . 5 ..^ ..^
106 fourierdlem79.z . . . . . . . 8
107 fzofzp1 11890 . . . . . . . . . . . . . 14 ..^
108107adantl 466 . . . . . . . . . . . . 13 ..^
10939, 108ffvelrnd 6017 . . . . . . . . . . . 12 ..^
110109, 42resubcld 9994 . . . . . . . . . . 11 ..^
111110rehalfcld 10792 . . . . . . . . . 10 ..^
1129, 103ffvelrnd 6017 . . . . . . . . . . . . 13
1133, 2, 1fourierdlem11 31789 . . . . . . . . . . . . . 14
114113simp1d 1009 . . . . . . . . . . . . 13
115112, 114resubcld 9994 . . . . . . . . . . . 12
116115rehalfcld 10792 . . . . . . . . . . 11
117116adantr 465 . . . . . . . . . 10 ..^
118111, 117ifcld 3969 . . . . . . . . 9 ..^
11942, 118readdcld 9626 . . . . . . . 8 ..^
120106, 119syl5eqel 2535 . . . . . . 7 ..^
121 2re 10612 . . . . . . . . . . . . . 14
122121a1i 11 . . . . . . . . . . . . 13 ..^
123 elfzoelz 11810 . . . . . . . . . . . . . . . . . 18 ..^
124123zred 10975 . . . . . . . . . . . . . . . . 17 ..^
125124ltp1d 10483 . . . . . . . . . . . . . . . 16 ..^
126125adantl 466 . . . . . . . . . . . . . . 15 ..^
12728simprd 463 . . . . . . . . . . . . . . . . 17
128127adantr 465 . . . . . . . . . . . . . . . 16 ..^
129 isorel 6207 . . . . . . . . . . . . . . . 16
130128, 41, 108, 129syl12anc 1227 . . . . . . . . . . . . . . 15 ..^
131126, 130mpbid 210 . . . . . . . . . . . . . 14 ..^
13242, 109posdifd 10146 . . . . . . . . . . . . . 14 ..^
133131, 132mpbid 210 . . . . . . . . . . . . 13 ..^
134 2pos 10634 . . . . . . . . . . . . . 14
135134a1i 11 . . . . . . . . . . . . 13 ..^
136110, 122, 133, 135divgt0d 10488 . . . . . . . . . . . 12 ..^
137111, 136elrpd 11264 . . . . . . . . . . 11 ..^
138121a1i 11 . . . . . . . . . . . . . 14
1392nngt0d 10586 . . . . . . . . . . . . . . . . . 18
140 fzolb 11815 . . . . . . . . . . . . . . . . . 18 ..^
14199, 100, 139, 140syl3anbrc 1181 . . . . . . . . . . . . . . . . 17 ..^
142 0re 9599 . . . . . . . . . . . . . . . . . 18
143 eleq1 2515 . . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
144143anbi2d 703 . . . . . . . . . . . . . . . . . . . 20 ..^ ..^
145 fveq2 5856 . . . . . . . . . . . . . . . . . . . . 21
146 oveq1 6288 . . . . . . . . . . . . . . . . . . . . . 22
147146fveq2d 5860 . . . . . . . . . . . . . . . . . . . . 21
148145, 147breq12d 4450 . . . . . . . . . . . . . . . . . . . 20
149144, 148imbi12d 320 . . . . . . . . . . . . . . . . . . 19 ..^ ..^
1506simprd 463 . . . . . . . . . . . . . . . . . . . . 21 ..^
151150simprd 463 . . . . . . . . . . . . . . . . . . . 20 ..^
152151r19.21bi 2812 . . . . . . . . . . . . . . . . . . 19 ..^
153149, 152vtoclg 3153 . . . . . . . . . . . . . . . . . 18 ..^
154142, 153ax-mp 5 . . . . . . . . . . . . . . . . 17 ..^
155141, 154mpdan 668 . . . . . . . . . . . . . . . 16
156150simpld 459 . . . . . . . . . . . . . . . . 17
157156simpld 459 . . . . . . . . . . . . . . . 16
158 0p1e1 10654 . . . . . . . . . . . . . . . . . 18
159158fveq2i 5859 . . . . . . . . . . . . . . . . 17
160159a1i 11 . . . . . . . . . . . . . . . 16
161155, 157, 1603brtr3d 4466 . . . . . . . . . . . . . . 15
162114, 112posdifd 10146 . . . . . . . . . . . . . . 15
163161, 162mpbid 210 . . . . . . . . . . . . . 14
164134a1i 11 . . . . . . . . . . . . . 14
165115, 138, 163, 164divgt0d 10488 . . . . . . . . . . . . 13
166116, 165elrpd 11264 . . . . . . . . . . . 12
167166adantr 465 . . . . . . . . . . 11 ..^
168137, 167ifcld 3969 . . . . . . . . . 10 ..^
16942, 168ltaddrpd 11295 . . . . . . . . 9 ..^
17042, 119, 169ltled 9736 . . . . . . . 8 ..^
171170, 106syl6breqr 4477 . . . . . . 7 ..^
17242, 111readdcld 9626 . . . . . . . . 9 ..^
173 iftrue 3932 . . . . . . . . . . . . 13
174173adantl 466 . . . . . . . . . . . 12 ..^
175111leidd 10126 . . . . . . . . . . . . 13 ..^
176175adantr 465 . . . . . . . . . . . 12 ..^
177174, 176eqbrtrd 4457 . . . . . . . . . . 11 ..^
178 iffalse 3935 . . . . . . . . . . . . 13
179178adantl 466 . . . . . . . . . . . 12 ..^
180115ad2antrr 725 . . . . . . . . . . . . 13 ..^
181110adantr 465 . . . . . . . . . . . . 13 ..^
182 2rp 11235 . . . . . . . . . . . . . 14
183182a1i 11 . . . . . . . . . . . . 13 ..^
184 simpr 461 . . . . . . . . . . . . . 14 ..^
185180, 181, 184nltled 31426 . . . . . . . . . . . . 13 ..^
186180, 181, 183, 185lediv1dd 11320 . . . . . . . . . . . 12 ..^
187179, 186eqbrtrd 4457 . . . . . . . . . . 11 ..^
188177, 187pm2.61dan 791 . . . . . . . . . 10 ..^
189118, 111, 42, 188leadd2dd 10174 . . . . . . . . 9 ..^
19042recnd 9625 . . . . . . . . . . . . . . . 16 ..^
191109recnd 9625 . . . . . . . . . . . . . . . 16 ..^
192190, 191addcomd 9785 . . . . . . . . . . . . . . 15 ..^
193192oveq1d 6296 . . . . . . . . . . . . . 14 ..^
194193oveq1d 6296 . . . . . . . . . . . . 13 ..^
195 halfaddsub 10779 . . . . . . . . . . . . . . 15
196191, 190, 195syl2anc 661 . . . . . . . . . . . . . 14 ..^
197196simprd 463 . . . . . . . . . . . . 13 ..^
198194, 197eqtrd 2484 . . . . . . . . . . . 12 ..^
199190, 191addcld 9618 . . . . . . . . . . . . . 14 ..^
200199halfcld 10790 . . . . . . . . . . . . 13 ..^
201111recnd 9625 . . . . . . . . . . . . 13 ..^
202200, 201, 190subsub23d 31423 . . . . . . . . . . . 12 ..^
203198, 202mpbid 210 . . . . . . . . . . 11 ..^
204200, 190, 201subaddd 9954 . . . . . . . . . . 11 ..^
205203, 204mpbid 210 . . . . . . . . . 10 ..^
206 avglt2 10784 . . . . . . . . . . . 12
20742, 109, 206syl2anc 661 . . . . . . . . . . 11 ..^
208131, 207mpbid 210 . . . . . . . . . 10 ..^
209205, 208eqbrtrd 4457 . . . . . . . . 9 ..^
210119, 172, 109, 189, 209lelttrd 9743 . . . . . . . 8 ..^
211106, 210syl5eqbr 4470 . . . . . . 7 ..^
212109rexrd 9646 . . . . . . . 8 ..^
213 elico2 11598 . . . . . . . 8
21442, 212, 213syl2anc 661 . . . . . . 7 ..^
215120, 171, 211, 214mpbir3and 1180 . . . . . 6 ..^
216215adantr 465 . . . . 5 ..^
217114ad2antrr 725 . . . . . . . 8 ..^
218113simp2d 1010 . . . . . . . . 9
219218ad2antrr 725 . . . . . . . 8 ..^
220113simp3d 1011 . . . . . . . . 9
221220ad2antrr 725 . . . . . . . 8 ..^
22242adantr 465 . . . . . . . 8 ..^
223 simpr 461 . . . . . . . 8 ..^
224169, 106syl6breqr 4477 . . . . . . . . . 10 ..^
225218, 114resubcld 9994 . . . . . . . . . . . . . 14
22611, 225syl5eqel 2535 . . . . . . . . . . . . 13
227226adantr 465 . . . . . . . . . . . 12 ..^
228111adantr 465 . . . . . . . . . . . . . . . 16 ..^
229116ad2antrr 725 . . . . . . . . . . . . . . . 16 ..^
230110adantr 465 . . . . . . . . . . . . . . . . 17 ..^
231115ad2antrr 725 . . . . . . . . . . . . . . . . 17 ..^
232182a1i 11 . . . . . . . . . . . . . . . . 17 ..^
233 simpr 461 . . . . . . . . . . . . . . . . 17 ..^
234230, 231, 232, 233ltdiv1dd 11319 . . . . . . . . . . . . . . . 16 ..^
235228, 229, 234ltled 9736 . . . . . . . . . . . . . . 15 ..^
236174, 235eqbrtrd 4457 . . . . . . . . . . . . . 14 ..^
237178adantl 466 . . . . . . . . . . . . . . . 16
238116leidd 10126 . . . . . . . . . . . . . . . . 17
239238adantr 465 . . . . . . . . . . . . . . . 16
240237, 239eqbrtrd 4457 . . . . . . . . . . . . . . 15
241240adantlr 714 . . . . . . . . . . . . . 14 ..^
242236, 241pm2.61dan 791 . . . . . . . . . . . . 13 ..^
243225rehalfcld 10792 . . . . . . . . . . . . . . . 16
244182a1i 11 . . . . . . . . . . . . . . . . 17
245114rexrd 9646 . . . . . . . . . . . . . . . . . . 19
246218rexrd 9646 . . . . . . . . . . . . . . . . . . 19
2473, 2, 1fourierdlem15 31793 . . . . . . . . . . . . . . . . . . . 20
248247, 103ffvelrnd 6017 . . . . . . . . . . . . . . . . . . 19
249 iccleub 11590 . . . . . . . . . . . . . . . . . . 19
250245, 246, 248, 249syl3anc 1229 . . . . . . . . . . . . . . . . . 18
251112, 218, 114, 250lesub1dd 10175 . . . . . . . . . . . . . . . . 17
252115, 225, 244, 251lediv1dd 11320 . . . . . . . . . . . . . . . 16
25311eqcomi 2456 . . . . . . . . . . . . . . . . . 18
254253oveq1i 6291 . . . . . . . . . . . . . . . . 17
255114, 218posdifd 10146 . . . . . . . . . . . . . . . . . . . . 21
256220, 255mpbid 210 . . . . . . . . . . . . . . . . . . . 20
257256, 11syl6breqr 4477 . . . . . . . . . . . . . . . . . . 19
258226, 257elrpd 11264 . . . . . . . . . . . . . . . . . 18
259 rphalflt 11256 . . . . . . . . . . . . . . . . . 18
260258, 259syl 16 . . . . . . . . . . . . . . . . 17
261254, 260syl5eqbr 4470 . . . . . . . . . . . . . . . 16
262116, 243, 226, 252, 261lelttrd 9743 . . . . . . . . . . . . . . 15
263116, 226, 262ltled 9736 . . . . . . . . . . . . . 14
264263adantr 465 . . . . . . . . . . . . 13 ..^
265118, 117, 227, 242, 264letrd 9742 . . . . . . . . . . . 12 ..^
266118, 227, 42, 265leadd2dd 10174 . . . . . . . . . . 11 ..^
267106, 266syl5eqbr 4470 . . . . . . . . . 10 ..^
26842rexrd 9646 . . . . . . . . . . 11 ..^
26942, 227readdcld 9626 . . . . . . . . . . 11 ..^
270 elioc2 11597 . . . . . . . . . . 11
271268, 269, 270syl2anc 661 . . . . . . . . . 10 ..^
272120, 224, 267, 271mpbir3and 1180 . . . . . . . . 9 ..^
273272adantr 465 . . . . . . . 8 ..^
274217, 219, 221, 11, 12, 222, 223, 273fourierdlem26 31804 . . . . . . 7 ..^
275106a1i 11 . . . . . . . . . 10 ..^
276275oveq1d 6296 . . . . . . . . 9 ..^
277276oveq2d 6297 . . . . . . . 8 ..^
278277adantr 465 . . . . . . 7 ..^
279118recnd 9625 . . . . . . . . . 10 ..^
280190, 279pncan2d 9938 . . . . . . . . 9 ..^
281280oveq2d 6297 . . . . . . . 8 ..^
282281adantr 465 . . . . . . 7 ..^
283274, 278, 2823eqtrd 2488 . . . . . 6 ..^
284173oveq2d 6297 . . . . . . . . . 10
285284adantl 466 . . . . . . . . 9 ..^
286114adantr 465 . . . . . . . . . . . 12 ..^
287286, 111readdcld 9626 . . . . . . . . . . 11 ..^
288287adantr 465 . . . . . . . . . 10 ..^
289286, 117readdcld 9626 . . . . . . . . . . 11 ..^
290289adantr 465 . . . . . . . . . 10 ..^
291112ad2antrr 725 . . . . . . . . . 10 ..^
292114ad2antrr 725 . . . . . . . . . . 11 ..^
293228, 229, 292, 234ltadd2dd 9744 . . . . . . . . . 10 ..^
294112recnd 9625 . . . . . . . . . . . . . . . 16
295114recnd 9625 . . . . . . . . . . . . . . . 16
296 halfaddsub 10779 . . . . . . . . . . . . . . . 16
297294, 295, 296syl2anc 661 . . . . . . . . . . . . . . 15
298297simprd 463 . . . . . . . . . . . . . 14
299298oveq1d 6296 . . . . . . . . . . . . 13
300112, 114readdcld 9626 . . . . . . . . . . . . . . . 16
301300rehalfcld 10792 . . . . . . . . . . . . . . 15
302301recnd 9625 . . . . . . . . . . . . . 14
303116recnd 9625 . . . . . . . . . . . . . 14
304302, 303npcand 9940 . . . . . . . . . . . . 13
305299, 304eqtr3d 2486 . . . . . . . . . . . 12
306112, 112readdcld 9626 . . . . . . . . . . . . . 14
307114, 112, 112, 161ltadd2dd 9744 . . . . . . . . . . . . . 14
308300, 306, 244, 307ltdiv1dd 11319 . . . . . . . . . . . . 13
3092942timesd 10788 . . . . . . . . . . . . . . . 16
310309eqcomd 2451 . . . . . . . . . . . . . . 15
311310oveq1d 6296 . . . . . . . . . . . . . 14
312 2cnd 10615 . . . . . . . . . . . . . . 15
313 2ne0 10635 . . . . . . . . . . . . . . . 16
314313a1i 11 . . . . . . . . . . . . . . 15
315294, 312, 314divcan3d 10332 . . . . . . . . . . . . . 14
316311, 315eqtrd 2484 . . . . . . . . . . . . 13
317308, 316breqtrd 4461 . . . . . . . . . . . 12
318305, 317eqbrtrd 4457 . . . . . . . . . . 11
319318ad2antrr 725 . . . . . . . . . 10 ..^
320288, 290, 291, 293, 319lttrd 9746 . . . . . . . . 9 ..^
321285, 320eqbrtrd 4457 . . . . . . . 8 ..^
322178oveq2d 6297 . . . . . . . . . 10
323322adantl 466 . . . . . . . . 9 ..^
324318ad2antrr 725 . . . . . . . . 9 ..^
325323, 324eqbrtrd 4457 . . . . . . . 8 ..^
326321, 325pm2.61dan 791 . . . . . . 7 ..^
327326adantr 465 . . . . . 6 ..^
328283, 327eqbrtrd 4457 . . . . 5 ..^
329 eqid 2443 . . . . 5
33011, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329fourierdlem63 31841 . . . 4 ..^
33114a1i 11 . . . . . . . . 9 ..^ ..^
33257adantl 466 . . . . . . . . 9 ..^ ..^ ..^
33360a1i 11 . . . . . . . . 9 ..^ ..^
334331, 332, 222, 333fvmptd 5946 . . . . . . . 8 ..^ ..^
335 fveq2 5856 . . . . . . . . . . . . 13
33613a1i 11 . . . . . . . . . . . . . 14
337 iftrue 3932 . . . . . . . . . . . . . . 15
338337adantl 466 . . . . . . . . . . . . . 14
339 ubioc1 11588 . . . . . . . . . . . . . . 15
340245, 246, 220, 339syl3anc 1229 . . . . . . . . . . . . . 14
341336, 338, 340, 114fvmptd 5946 . . . . . . . . . . . . 13