fourierdlem79 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem79 31809

Description:

projects every interval of the partition induced by

into a corresponding interval of the partition induced by

(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.

Step	Hyp	Ref	Expression
1		fourierdlem79.q	. . . . . . . . 9
2		fourierdlem79.m	. . . . . . . . . 10
3		fourierdlem79.p	. . . . . . . . . . 11 $/\$ $/\$ ..^
4	3	fourierdlem2 31732	. . . . . . . . . 10 $/\$ $/\$ $/\$ ..^
5	2, 4	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ ..^
6	1, 5	mpbid 210	. . . . . . . 8 $/\$ $/\$ $/\$ ..^
7	6	simpld 459	. . . . . . 7
8		elmapi 7452	. . . . . . 7
9	7, 8	syl 16	. . . . . 6
10	9	adantr 465	. . . . 5 $/\$ ..^
11		fourierdlem79.t	. . . . . . . . . 10
12		fourierdlem79.e	. . . . . . . . . 10
13		fourierdlem79.l	. . . . . . . . . 10
14		fourierdlem79.i	. . . . . . . . . 10 ..^
15	3, 2, 1, 11, 12, 13, 14	fourierdlem37 31767	. . . . . . . . 9 ..^ $/\$ ..^ ..^
16	15	simpld 459	. . . . . . . 8 ..^
17		fzossfz 11826	. . . . . . . . 9 ..^
18	17	a1i 11	. . . . . . . 8 ..^
19		fss 5745	. . . . . . . 8 ..^ $/\$ ..^
20	16, 18, 19	syl2anc 661	. . . . . . 7
21	20	adantr 465	. . . . . 6 $/\$ ..^
22		fourierdlem79.c	. . . . . . . . . . . . . 14
23		fourierdlem79.d	. . . . . . . . . . . . . 14
24		fourierdlem79.cltd	. . . . . . . . . . . . . 14
25		fourierdlem79.o	. . . . . . . . . . . . . 14 $/\$ $/\$ ..^
26		fourierdlem79.h	. . . . . . . . . . . . . 14
27		fourierdlem79.n	. . . . . . . . . . . . . 14
28		fourierdlem79.s	. . . . . . . . . . . . . 14
29	11, 3, 2, 1, 22, 23, 24, 25, 26, 27, 28	fourierdlem54 31784	. . . . . . . . . . . . 13 $/\$ $/\$
30	29	simpld 459	. . . . . . . . . . . 12 $/\$
31	30	simprd 463	. . . . . . . . . . 11
32	31	adantr 465	. . . . . . . . . 10 $/\$ ..^
33	30	simpld 459	. . . . . . . . . . . 12
34	33	adantr 465	. . . . . . . . . . 11 $/\$ ..^
35	25	fourierdlem2 31732	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ..^
36	34, 35	syl 16	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$ $/\$ ..^
37	32, 36	mpbid 210	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$ $/\$ ..^
38	37	simpld 459	. . . . . . . 8 $/\$ ..^
39		elmapi 7452	. . . . . . . 8
40	38, 39	syl 16	. . . . . . 7 $/\$ ..^
41		elfzofz 11823	. . . . . . . 8 ..^
42	41	adantl 466	. . . . . . 7 $/\$ ..^
43	40, 42	ffvelrnd 6033	. . . . . 6 $/\$ ..^
44	21, 43	ffvelrnd 6033	. . . . 5 $/\$ ..^
45	10, 44	ffvelrnd 6033	. . . 4 $/\$ ..^
46	45	rexrd 9655	. . 3 $/\$ ..^
47	16	adantr 465	. . . . . . 7 $/\$ ..^ ..^
48	47, 43	ffvelrnd 6033	. . . . . 6 $/\$ ..^ ..^
49		fzofzp1 11889	. . . . . 6 ..^
50	48, 49	syl 16	. . . . 5 $/\$ ..^
51	10, 50	ffvelrnd 6033	. . . 4 $/\$ ..^
52	51	rexrd 9655	. . 3 $/\$ ..^
53	46, 52	jca 532	. 2 $/\$ ..^ $/\$
54	14	a1i 11	. . . . . 6 $/\$ ..^ ..^
55		fveq2 5872	. . . . . . . . . . 11
56	55	fveq2d 5876	. . . . . . . . . 10
57	56	breq2d 4465	. . . . . . . . 9
58	57	rabbidv 3110	. . . . . . . 8 ..^ ..^
59	58	supeq1d 7918	. . . . . . 7 ..^ ..^
60	59	adantl 466	. . . . . 6 $/\$ ..^ $/\$ ..^ ..^
61		ltso 9677	. . . . . . . 8
62	61	supex 7935	. . . . . . 7 ..^
63	62	a1i 11	. . . . . 6 $/\$ ..^ ..^
64	54, 60, 43, 63	fvmptd 5962	. . . . 5 $/\$ ..^ ..^
65	64	fveq2d 5876	. . . 4 $/\$ ..^ ..^
66		simpl 457	. . . . . . . 8 $/\$ ..^
67	66, 43	jca 532	. . . . . . 7 $/\$ ..^ $/\$
68		eleq1 2539	. . . . . . . . . 10
69	68	anbi2d 703	. . . . . . . . 9 $/\$ $/\$
70	59, 58	eleq12d 2549	. . . . . . . . 9 ..^ ..^ ..^ ..^
71	69, 70	imbi12d 320	. . . . . . . 8 $/\$ ..^ ..^ $/\$ ..^ ..^
72	15	simprd 463	. . . . . . . . 9 ..^ ..^
73	72	imp 429	. . . . . . . 8 $/\$ ..^ ..^
74	71, 73	vtoclg 3176	. . . . . . 7 $/\$ ..^ ..^
75	43, 67, 74	sylc 60	. . . . . 6 $/\$ ..^ ..^ ..^
76		nfrab1 3047	. . . . . . . 8 ..^
77		nfcv 2629	. . . . . . . 8
78		nfcv 2629	. . . . . . . 8
79	76, 77, 78	nfsup 7923	. . . . . . 7 ..^
80		nfcv 2629	. . . . . . 7 ..^
81		nfcv 2629	. . . . . . . . 9
82	81, 79	nffv 5879	. . . . . . . 8 ..^
83		nfcv 2629	. . . . . . . 8
84		nfcv 2629	. . . . . . . 8
85	82, 83, 84	nfbr 4497	. . . . . . 7 ..^
86		fveq2 5872	. . . . . . . 8 ..^ ..^
87	86	breq1d 4463	. . . . . . 7 ..^ ..^
88	79, 80, 85, 87	elrabf 3264	. . . . . 6 ..^ ..^ ..^ ..^ $/\$ ..^
89	75, 88	sylib 196	. . . . 5 $/\$ ..^ ..^ ..^ $/\$ ..^
90	89	simprd 463	. . . 4 $/\$ ..^ ..^
91	65, 90	eqbrtrd 4473	. . 3 $/\$ ..^
92	2	ad2antrr 725	. . . . . 6 $/\$ ..^ $/\$
93	1	ad2antrr 725	. . . . . 6 $/\$ ..^ $/\$
94	22	ad2antrr 725	. . . . . 6 $/\$ ..^ $/\$
95	23	ad2antrr 725	. . . . . 6 $/\$ ..^ $/\$
96	24	ad2antrr 725	. . . . . 6 $/\$ ..^ $/\$
97		0re 9608	. . . . . . . . . . 11
98		1re 9607	. . . . . . . . . . 11
99		0lt1 10087	. . . . . . . . . . 11
100	97, 98, 99	ltleii 9719	. . . . . . . . . 10
101	100	a1i 11	. . . . . . . . 9
102	2	nnge1d 10590	. . . . . . . . 9
103	101, 102	jca 532	. . . . . . . 8 $/\$
104		1z 10906	. . . . . . . . . 10
105	104	a1i 11	. . . . . . . . 9
106		0z 10887	. . . . . . . . . 10
107	106	a1i 11	. . . . . . . . 9
108	2	nnzd 10977	. . . . . . . . 9
109		elfz 11690	. . . . . . . . 9 $/\$ $/\$ $/\$
110	105, 107, 108, 109	syl3anc 1228	. . . . . . . 8 $/\$
111	103, 110	mpbird 232	. . . . . . 7
112	111	ad2antrr 725	. . . . . 6 $/\$ ..^ $/\$
113		simpr 461	. . . . . . 7 $/\$ ..^ ..^
114	113	adantr 465	. . . . . 6 $/\$ ..^ $/\$ ..^
115		fourierdlem79.z	. . . . . . . . . 10
116		fzofzp1 11889	. . . . . . . . . . . . . . . . 17 ..^
117	116	adantl 466	. . . . . . . . . . . . . . . 16 $/\$ ..^
118	40, 117	ffvelrnd 6033	. . . . . . . . . . . . . . 15 $/\$ ..^
119	118, 43	jca 532	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
120		resubcl 9895	. . . . . . . . . . . . . 14 $/\$
121	119, 120	syl 16	. . . . . . . . . . . . 13 $/\$ ..^
122		rehalfcl 10777	. . . . . . . . . . . . 13
123	121, 122	syl 16	. . . . . . . . . . . 12 $/\$ ..^
124	9, 111	ffvelrnd 6033	. . . . . . . . . . . . . . 15
125	3, 2, 1	fourierdlem11 31741	. . . . . . . . . . . . . . . 16 $/\$ $/\$
126	125	simp1d 1008	. . . . . . . . . . . . . . 15
127	124, 126	resubcld 9999	. . . . . . . . . . . . . 14
128		2re 10617	. . . . . . . . . . . . . . 15
129	128	a1i 11	. . . . . . . . . . . . . 14
130		2ne0 10640	. . . . . . . . . . . . . . 15
131	130	a1i 11	. . . . . . . . . . . . . 14
132	127, 129, 131	redivcld 10384	. . . . . . . . . . . . 13
133	132	adantr 465	. . . . . . . . . . . 12 $/\$ ..^
134	123, 133	ifcld 3988	. . . . . . . . . . 11 $/\$ ..^
135	43, 134	readdcld 9635	. . . . . . . . . 10 $/\$ ..^
136	115, 135	syl5eqel 2559	. . . . . . . . 9 $/\$ ..^
137	128	a1i 11	. . . . . . . . . . . . . . 15 $/\$ ..^
138		elfzoelz 11809	. . . . . . . . . . . . . . . . . . . 20 ..^
139		zre 10880	. . . . . . . . . . . . . . . . . . . 20
140	138, 139	syl 16	. . . . . . . . . . . . . . . . . . 19 ..^
141		ltp1 10392	. . . . . . . . . . . . . . . . . . 19
142	140, 141	syl 16	. . . . . . . . . . . . . . . . . 18 ..^
143	142	adantl 466	. . . . . . . . . . . . . . . . 17 $/\$ ..^
144	29	simprd 463	. . . . . . . . . . . . . . . . . . 19
145	144	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
146		isorel 6221	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
147	145, 42, 117, 146	syl12anc 1226	. . . . . . . . . . . . . . . . 17 $/\$ ..^
148	143, 147	mpbid 210	. . . . . . . . . . . . . . . 16 $/\$ ..^
149	43, 118	posdifd 10151	. . . . . . . . . . . . . . . 16 $/\$ ..^
150	148, 149	mpbid 210	. . . . . . . . . . . . . . 15 $/\$ ..^
151		2pos 10639	. . . . . . . . . . . . . . . 16
152	151	a1i 11	. . . . . . . . . . . . . . 15 $/\$ ..^
153	121, 137, 150, 152	divgt0d 10493	. . . . . . . . . . . . . 14 $/\$ ..^
154	123, 153	elrpd 11266	. . . . . . . . . . . . 13 $/\$ ..^
155	6	simprd 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^
156	155	simpld 459	. . . . . . . . . . . . . . . . . . . 20 $/\$
157	156	simpld 459	. . . . . . . . . . . . . . . . . . 19
158	157	eqcomd 2475	. . . . . . . . . . . . . . . . . 18
159	2	nngt0d 10591	. . . . . . . . . . . . . . . . . . . . . 22
160	107, 108, 159	3jca 1176	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
161		fzolb 11814	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ $/\$
162	160, 161	sylibr 212	. . . . . . . . . . . . . . . . . . . 20 ..^
163		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
164	163	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ ..^
165		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . 24
166		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . 25
167	166	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . 24
168	165, 167	breq12d 4466	. . . . . . . . . . . . . . . . . . . . . . 23
169	164, 168	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ ..^
170	155	simprd 463	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
171	170	r19.21bi 2836	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
172	169, 171	vtoclg 3176	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^
173	97, 172	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
174	162, 173	mpdan 668	. . . . . . . . . . . . . . . . . . 19
175		1e0p1 11016	. . . . . . . . . . . . . . . . . . . . . 22
176	175	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . 21
177	176	fveq2i 5875	. . . . . . . . . . . . . . . . . . . 20
178	177	a1i 11	. . . . . . . . . . . . . . . . . . 19
179	174, 178	breqtrd 4477	. . . . . . . . . . . . . . . . . 18
180	158, 179	eqbrtrd 4473	. . . . . . . . . . . . . . . . 17
181	126, 124	posdifd 10151	. . . . . . . . . . . . . . . . 17
182	180, 181	mpbid 210	. . . . . . . . . . . . . . . 16
183	151	a1i 11	. . . . . . . . . . . . . . . 16
184	127, 129, 182, 183	divgt0d 10493	. . . . . . . . . . . . . . 15
185	132, 184	elrpd 11266	. . . . . . . . . . . . . 14
186	185	adantr 465	. . . . . . . . . . . . 13 $/\$ ..^
187	154, 186	ifcld 3988	. . . . . . . . . . . 12 $/\$ ..^
188	43, 187	ltaddrpd 11297	. . . . . . . . . . 11 $/\$ ..^
189	43, 135, 188	ltled 9744	. . . . . . . . . 10 $/\$ ..^
190	115	eqcomi 2480	. . . . . . . . . . 11
191	190	a1i 11	. . . . . . . . . 10 $/\$ ..^
192	189, 191	breqtrd 4477	. . . . . . . . 9 $/\$ ..^
193	115	a1i 11	. . . . . . . . . 10 $/\$ ..^
194	43, 123	readdcld 9635	. . . . . . . . . . 11 $/\$ ..^
195		iftrue 3951	. . . . . . . . . . . . . . 15
196	195	adantl 466	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
197	123	leidd 10131	. . . . . . . . . . . . . . 15 $/\$ ..^
198	197	adantr 465	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
199	196, 198	eqbrtrd 4473	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
200		iffalse 3954	. . . . . . . . . . . . . . 15
201	200	adantl 466	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
202		simpr 461	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
203	127	ad2antrr 725	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
204	121	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
205	203, 204	lenltd 9742	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
206	202, 205	mpbird 232	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
207		2rp 11237	. . . . . . . . . . . . . . . . 17
208	207	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
209	203, 204, 208	lediv1d 11310	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
210	206, 209	mpbid 210	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
211	201, 210	eqbrtrd 4473	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
212	199, 211	pm2.61dan 789	. . . . . . . . . . . 12 $/\$ ..^
213	134, 123, 43	leadd2d 10159	. . . . . . . . . . . 12 $/\$ ..^
214	212, 213	mpbid 210	. . . . . . . . . . 11 $/\$ ..^
215	43	recnd 9634	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
216	118	recnd 9634	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
217	215, 216	addcomd 9793	. . . . . . . . . . . . . . . . 17 $/\$ ..^
218	217	oveq1d 6310	. . . . . . . . . . . . . . . 16 $/\$ ..^
219	218	oveq1d 6310	. . . . . . . . . . . . . . 15 $/\$ ..^
220		halfaddsub 10784	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
221	216, 215, 220	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
222	221	simprd 463	. . . . . . . . . . . . . . 15 $/\$ ..^
223	219, 222	eqtrd 2508	. . . . . . . . . . . . . 14 $/\$ ..^
224	215, 216	jca 532	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
225		addcl 9586	. . . . . . . . . . . . . . . . 17 $/\$
226	224, 225	syl 16	. . . . . . . . . . . . . . . 16 $/\$ ..^
227		halfcl 10776	. . . . . . . . . . . . . . . 16
228	226, 227	syl 16	. . . . . . . . . . . . . . 15 $/\$ ..^
229	123	recnd 9634	. . . . . . . . . . . . . . 15 $/\$ ..^
230	228, 229, 215	subsub23d 31374	. . . . . . . . . . . . . 14 $/\$ ..^
231	223, 230	mpbid 210	. . . . . . . . . . . . 13 $/\$ ..^
232	228, 215, 229	subaddd 9960	. . . . . . . . . . . . 13 $/\$ ..^
233	231, 232	mpbid 210	. . . . . . . . . . . 12 $/\$ ..^
234		avglt2 10789	. . . . . . . . . . . . . 14 $/\$
235	43, 118, 234	syl2anc 661	. . . . . . . . . . . . 13 $/\$ ..^
236	148, 235	mpbid 210	. . . . . . . . . . . 12 $/\$ ..^
237	233, 236	eqbrtrd 4473	. . . . . . . . . . 11 $/\$ ..^
238	135, 194, 118, 214, 237	lelttrd 9751	. . . . . . . . . 10 $/\$ ..^
239	193, 238	eqbrtrd 4473	. . . . . . . . 9 $/\$ ..^
240	136, 192, 239	3jca 1176	. . . . . . . 8 $/\$ ..^ $/\$ $/\$
241	118	rexrd 9655	. . . . . . . . 9 $/\$ ..^
242		elico2 11600	. . . . . . . . 9 $/\$ $/\$ $/\$
243	43, 241, 242	syl2anc 661	. . . . . . . 8 $/\$ ..^ $/\$ $/\$
244	240, 243	mpbird 232	. . . . . . 7 $/\$ ..^
245	244	adantr 465	. . . . . 6 $/\$ ..^ $/\$
246	126	ad2antrr 725	. . . . . . . . 9 $/\$ ..^ $/\$
247	125	simp2d 1009	. . . . . . . . . . 11
248	66, 247	syl 16	. . . . . . . . . 10 $/\$ ..^
249	248	adantr 465	. . . . . . . . 9 $/\$ ..^ $/\$
250	125	simp3d 1010	. . . . . . . . . 10
251	250	ad2antrr 725	. . . . . . . . 9 $/\$ ..^ $/\$
252	43	adantr 465	. . . . . . . . 9 $/\$ ..^ $/\$
253		simpr 461	. . . . . . . . 9 $/\$ ..^ $/\$
254	188, 191	breqtrd 4477	. . . . . . . . . . . 12 $/\$ ..^
255	247, 126	resubcld 9999	. . . . . . . . . . . . . . . . 17
256	11, 255	syl5eqel 2559	. . . . . . . . . . . . . . . 16
257	256	adantr 465	. . . . . . . . . . . . . . 15 $/\$ ..^
258	123	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
259	133	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
260		simpr 461	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
261	121	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
262	127	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
263	207	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
264	261, 262, 263	ltdiv1d 11309	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
265	260, 264	mpbid 210	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
266	258, 259, 265	ltled 9744	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
267	196, 266	eqbrtrd 4473	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
268	200	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$
269	132	leidd 10131	. . . . . . . . . . . . . . . . . . 19
270	269	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
271	268, 270	eqbrtrd 4473	. . . . . . . . . . . . . . . . 17 $/\$
272	271	adantlr 714	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
273	267, 272	pm2.61dan 789	. . . . . . . . . . . . . . 15 $/\$ ..^
274	255, 129, 131	redivcld 10384	. . . . . . . . . . . . . . . . . 18
275	126	rexrd 9655	. . . . . . . . . . . . . . . . . . . . 21
276	247	rexrd 9655	. . . . . . . . . . . . . . . . . . . . 21
277	3, 2, 1	fourierdlem15 31745	. . . . . . . . . . . . . . . . . . . . . 22
278	277, 111	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . . 21
279		iccleub 11592	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
280	275, 276, 278, 279	syl3anc 1228	. . . . . . . . . . . . . . . . . . . 20
281	124, 247, 126	lesub1d 10171	. . . . . . . . . . . . . . . . . . . 20
282	280, 281	mpbid 210	. . . . . . . . . . . . . . . . . . 19
283	207	a1i 11	. . . . . . . . . . . . . . . . . . . 20
284	127, 255, 283	lediv1d 11310	. . . . . . . . . . . . . . . . . . 19
285	282, 284	mpbid 210	. . . . . . . . . . . . . . . . . 18
286	11	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . 21
287	286	oveq1i 6305	. . . . . . . . . . . . . . . . . . . 20
288	287	a1i 11	. . . . . . . . . . . . . . . . . . 19
289	126, 247	posdifd 10151	. . . . . . . . . . . . . . . . . . . . . . 23
290	250, 289	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22
291	286	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
292	290, 291	breqtrd 4477	. . . . . . . . . . . . . . . . . . . . 21
293	256, 292	elrpd 11266	. . . . . . . . . . . . . . . . . . . 20
294		rphalflt 11258	. . . . . . . . . . . . . . . . . . . 20
295	293, 294	syl 16	. . . . . . . . . . . . . . . . . . 19
296	288, 295	eqbrtrd 4473	. . . . . . . . . . . . . . . . . 18
297	132, 274, 256, 285, 296	lelttrd 9751	. . . . . . . . . . . . . . . . 17
298	132, 256, 297	ltled 9744	. . . . . . . . . . . . . . . 16
299	298	adantr 465	. . . . . . . . . . . . . . 15 $/\$ ..^
300	134, 133, 257, 273, 299	letrd 9750	. . . . . . . . . . . . . 14 $/\$ ..^
301	134, 257, 43	leadd2d 10159	. . . . . . . . . . . . . 14 $/\$ ..^
302	300, 301	mpbid 210	. . . . . . . . . . . . 13 $/\$ ..^
303	193, 302	eqbrtrd 4473	. . . . . . . . . . . 12 $/\$ ..^
304	136, 254, 303	3jca 1176	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
305	43	rexrd 9655	. . . . . . . . . . . 12 $/\$ ..^
306	43, 257	readdcld 9635	. . . . . . . . . . . 12 $/\$ ..^
307		elioc2 11599	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
308	305, 306, 307	syl2anc 661	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
309	304, 308	mpbird 232	. . . . . . . . . 10 $/\$ ..^
310	309	adantr 465	. . . . . . . . 9 $/\$ ..^ $/\$
311	246, 249, 251, 11, 12, 252, 253, 310	fourierdlem26 31756	. . . . . . . 8 $/\$ ..^ $/\$
312	193	oveq1d 6310	. . . . . . . . . 10 $/\$ ..^
313	312	oveq2d 6311	. . . . . . . . 9 $/\$ ..^
314	313	adantr 465	. . . . . . . 8 $/\$ ..^ $/\$
315	134	recnd 9634	. . . . . . . . . . 11 $/\$ ..^
316	215, 315	pncan2d 9944	. . . . . . . . . 10 $/\$ ..^
317	316	oveq2d 6311	. . . . . . . . 9 $/\$ ..^
318	317	adantr 465	. . . . . . . 8 $/\$ ..^ $/\$
319	311, 314, 318	3eqtrd 2512	. . . . . . 7 $/\$ ..^ $/\$
320	195	oveq2d 6311	. . . . . . . . . . 11
321	320	adantl 466	. . . . . . . . . 10 $/\$ ..^ $/\$
322	66, 126	syl 16	. . . . . . . . . . . . 13 $/\$ ..^
323	322, 123	readdcld 9635	. . . . . . . . . . . 12 $/\$ ..^
324	323	adantr 465	. . . . . . . . . . 11 $/\$ ..^ $/\$
325	322, 133	readdcld 9635	. . . . . . . . . . . 12 $/\$ ..^
326	325	adantr 465	. . . . . . . . . . 11 $/\$ ..^ $/\$
327	124	ad2antrr 725	. . . . . . . . . . 11 $/\$ ..^ $/\$
328	322	adantr 465	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
329	258, 259, 328	ltadd2d 9749	. . . . . . . . . . . 12 $/\$ ..^ $/\$
330	265, 329	mpbid 210	. . . . . . . . . . 11 $/\$ ..^ $/\$
331	124, 126	jca 532	. . . . . . . . . . . . . . . . . . 19 $/\$
332		readdcl 9587	. . . . . . . . . . . . . . . . . . 19 $/\$
333	331, 332	syl 16	. . . . . . . . . . . . . . . . . 18
334		rehalfcl 10777	. . . . . . . . . . . . . . . . . 18
335	333, 334	syl 16	. . . . . . . . . . . . . . . . 17
336	335	recnd 9634	. . . . . . . . . . . . . . . 16
337	132	recnd 9634	. . . . . . . . . . . . . . . 16
338	336, 337	npcand 9946	. . . . . . . . . . . . . . 15
339	338	eqcomd 2475	. . . . . . . . . . . . . 14
340	124	recnd 9634	. . . . . . . . . . . . . . . . 17
341	126	recnd 9634	. . . . . . . . . . . . . . . . 17
342		halfaddsub 10784	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
343	340, 341, 342	syl2anc 661	. . . . . . . . . . . . . . . 16 $/\$
344	343	simprd 463	. . . . . . . . . . . . . . 15
345	344	oveq1d 6310	. . . . . . . . . . . . . 14