fourierdlem79 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem79 40402

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	. . . . . . . 8
2		fourierdlem79.m	. . . . . . . . 9
3		fourierdlem79.p	. . . . . . . . . 10 $/\$ $/\$ ..^
4	3	fourierdlem2 40326	. . . . . . . . 9 $/\$ $/\$ $/\$ ..^
5	2, 4	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ ..^
6	1, 5	mpbid 222	. . . . . . 7 $/\$ $/\$ $/\$ ..^
7	6	simpld 475	. . . . . 6
8		elmapi 7879	. . . . . 6
9	7, 8	syl 17	. . . . 5
10	9	adantr 481	. . . 4 $/\$ ..^
11		fourierdlem79.t	. . . . . . . . 9
12		fourierdlem79.e	. . . . . . . . 9
13		fourierdlem79.l	. . . . . . . . 9
14		fourierdlem79.i	. . . . . . . . 9 ..^
15	3, 2, 1, 11, 12, 13, 14	fourierdlem37 40361	. . . . . . . 8 ..^ $/\$ ..^ ..^
16	15	simpld 475	. . . . . . 7 ..^
17		fzossfz 12488	. . . . . . . 8 ..^
18	17	a1i 11	. . . . . . 7 ..^
19	16, 18	fssd 6057	. . . . . 6
20	19	adantr 481	. . . . 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
28	11, 3, 2, 1, 21, 22, 23, 24, 25, 26, 27	fourierdlem54 40377	. . . . . . . . . . . 12 $/\$ $/\$
29	28	simpld 475	. . . . . . . . . . 11 $/\$
30	29	simprd 479	. . . . . . . . . 10
31	30	adantr 481	. . . . . . . . 9 $/\$ ..^
32	29	simpld 475	. . . . . . . . . . 11
33	32	adantr 481	. . . . . . . . . 10 $/\$ ..^
34	24	fourierdlem2 40326	. . . . . . . . . 10 $/\$ $/\$ $/\$ ..^
35	33, 34	syl 17	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$ $/\$ ..^
36	31, 35	mpbid 222	. . . . . . . 8 $/\$ ..^ $/\$ $/\$ $/\$ ..^
37	36	simpld 475	. . . . . . 7 $/\$ ..^
38		elmapi 7879	. . . . . . 7
39	37, 38	syl 17	. . . . . 6 $/\$ ..^
40		elfzofz 12485	. . . . . . 7 ..^
41	40	adantl 482	. . . . . 6 $/\$ ..^
42	39, 41	ffvelrnd 6360	. . . . 5 $/\$ ..^
43	20, 42	ffvelrnd 6360	. . . 4 $/\$ ..^
44	10, 43	ffvelrnd 6360	. . 3 $/\$ ..^
45	44	rexrd 10089	. 2 $/\$ ..^
46	16	adantr 481	. . . . . 6 $/\$ ..^ ..^
47	46, 42	ffvelrnd 6360	. . . . 5 $/\$ ..^ ..^
48		fzofzp1 12565	. . . . 5 ..^
49	47, 48	syl 17	. . . 4 $/\$ ..^
50	10, 49	ffvelrnd 6360	. . 3 $/\$ ..^
51	50	rexrd 10089	. 2 $/\$ ..^
52	14	a1i 11	. . . . 5 $/\$ ..^ ..^
53		fveq2 6191	. . . . . . . . . 10
54	53	fveq2d 6195	. . . . . . . . 9
55	54	breq2d 4665	. . . . . . . 8
56	55	rabbidv 3189	. . . . . . 7 ..^ ..^
57	56	supeq1d 8352	. . . . . 6 ..^ ..^
58	57	adantl 482	. . . . 5 $/\$ ..^ $/\$ ..^ ..^
59		ltso 10118	. . . . . . 7
60	59	supex 8369	. . . . . 6 ..^
61	60	a1i 11	. . . . 5 $/\$ ..^ ..^
62	52, 58, 42, 61	fvmptd 6288	. . . 4 $/\$ ..^ ..^
63	62	fveq2d 6195	. . 3 $/\$ ..^ ..^
64		simpl 473	. . . . . . 7 $/\$ ..^
65	64, 42	jca 554	. . . . . 6 $/\$ ..^ $/\$
66		eleq1 2689	. . . . . . . . 9
67	66	anbi2d 740	. . . . . . . 8 $/\$ $/\$
68	57, 56	eleq12d 2695	. . . . . . . 8 ..^ ..^ ..^ ..^
69	67, 68	imbi12d 334	. . . . . . 7 $/\$ ..^ ..^ $/\$ ..^ ..^
70	15	simprd 479	. . . . . . . 8 ..^ ..^
71	70	imp 445	. . . . . . 7 $/\$ ..^ ..^
72	69, 71	vtoclg 3266	. . . . . 6 $/\$ ..^ ..^
73	42, 65, 72	sylc 65	. . . . 5 $/\$ ..^ ..^ ..^
74		nfrab1 3122	. . . . . . 7 ..^
75		nfcv 2764	. . . . . . 7
76		nfcv 2764	. . . . . . 7
77	74, 75, 76	nfsup 8357	. . . . . 6 ..^
78		nfcv 2764	. . . . . 6 ..^
79		nfcv 2764	. . . . . . . 8
80	79, 77	nffv 6198	. . . . . . 7 ..^
81		nfcv 2764	. . . . . . 7
82		nfcv 2764	. . . . . . 7
83	80, 81, 82	nfbr 4699	. . . . . 6 ..^
84		fveq2 6191	. . . . . . 7 ..^ ..^
85	84	breq1d 4663	. . . . . 6 ..^ ..^
86	77, 78, 83, 85	elrabf 3360	. . . . 5 ..^ ..^ ..^ ..^ $/\$ ..^
87	73, 86	sylib 208	. . . 4 $/\$ ..^ ..^ ..^ $/\$ ..^
88	87	simprd 479	. . 3 $/\$ ..^ ..^
89	63, 88	eqbrtrd 4675	. 2 $/\$ ..^
90	2	ad2antrr 762	. . . . 5 $/\$ ..^ $/\$
91	1	ad2antrr 762	. . . . 5 $/\$ ..^ $/\$
92	21	ad2antrr 762	. . . . 5 $/\$ ..^ $/\$
93	22	ad2antrr 762	. . . . 5 $/\$ ..^ $/\$
94	23	ad2antrr 762	. . . . 5 $/\$ ..^ $/\$
95		0le1 10551	. . . . . . . 8
96	95	a1i 11	. . . . . . 7
97	2	nnge1d 11063	. . . . . . 7
98		1zzd 11408	. . . . . . . 8
99		0zd 11389	. . . . . . . 8
100	2	nnzd 11481	. . . . . . . 8
101		elfz 12332	. . . . . . . 8 $/\$ $/\$ $/\$
102	98, 99, 100, 101	syl3anc 1326	. . . . . . 7 $/\$
103	96, 97, 102	mpbir2and 957	. . . . . 6
104	103	ad2antrr 762	. . . . 5 $/\$ ..^ $/\$
105		simplr 792	. . . . 5 $/\$ ..^ $/\$ ..^
106		fourierdlem79.z	. . . . . . . 8
107		fzofzp1 12565	. . . . . . . . . . . . . 14 ..^
108	107	adantl 482	. . . . . . . . . . . . 13 $/\$ ..^
109	39, 108	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$ ..^
110	109, 42	resubcld 10458	. . . . . . . . . . 11 $/\$ ..^
111	110	rehalfcld 11279	. . . . . . . . . 10 $/\$ ..^
112	9, 103	ffvelrnd 6360	. . . . . . . . . . . . 13
113	3, 2, 1	fourierdlem11 40335	. . . . . . . . . . . . . 14 $/\$ $/\$
114	113	simp1d 1073	. . . . . . . . . . . . 13
115	112, 114	resubcld 10458	. . . . . . . . . . . 12
116	115	rehalfcld 11279	. . . . . . . . . . 11
117	116	adantr 481	. . . . . . . . . 10 $/\$ ..^
118	111, 117	ifcld 4131	. . . . . . . . 9 $/\$ ..^
119	42, 118	readdcld 10069	. . . . . . . 8 $/\$ ..^
120	106, 119	syl5eqel 2705	. . . . . . 7 $/\$ ..^
121		2re 11090	. . . . . . . . . . . . . 14
122	121	a1i 11	. . . . . . . . . . . . 13 $/\$ ..^
123		elfzoelz 12470	. . . . . . . . . . . . . . . . . 18 ..^
124	123	zred 11482	. . . . . . . . . . . . . . . . 17 ..^
125	124	ltp1d 10954	. . . . . . . . . . . . . . . 16 ..^
126	125	adantl 482	. . . . . . . . . . . . . . 15 $/\$ ..^
127	28	simprd 479	. . . . . . . . . . . . . . . . 17
128	127	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^
129		isorel 6576	. . . . . . . . . . . . . . . 16 $/\$ $/\$
130	128, 41, 108, 129	syl12anc 1324	. . . . . . . . . . . . . . 15 $/\$ ..^
131	126, 130	mpbid 222	. . . . . . . . . . . . . 14 $/\$ ..^
132	42, 109	posdifd 10614	. . . . . . . . . . . . . 14 $/\$ ..^
133	131, 132	mpbid 222	. . . . . . . . . . . . 13 $/\$ ..^
134		2pos 11112	. . . . . . . . . . . . . 14
135	134	a1i 11	. . . . . . . . . . . . 13 $/\$ ..^
136	110, 122, 133, 135	divgt0d 10959	. . . . . . . . . . . 12 $/\$ ..^
137	111, 136	elrpd 11869	. . . . . . . . . . 11 $/\$ ..^
138	121	a1i 11	. . . . . . . . . . . . . 14
139	2	nngt0d 11064	. . . . . . . . . . . . . . . . . 18
140		fzolb 12476	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$
141	99, 100, 139, 140	syl3anbrc 1246	. . . . . . . . . . . . . . . . 17 ..^
142		0re 10040	. . . . . . . . . . . . . . . . . 18
143		eleq1 2689	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^
144	143	anbi2d 740	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ ..^
145		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
146		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
147	146	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21
148	145, 147	breq12d 4666	. . . . . . . . . . . . . . . . . . . 20
149	144, 148	imbi12d 334	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ ..^
150	6	simprd 479	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^
151	150	simprd 479	. . . . . . . . . . . . . . . . . . . 20 ..^
152	151	r19.21bi 2932	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
153	149, 152	vtoclg 3266	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
154	142, 153	ax-mp 5	. . . . . . . . . . . . . . . . 17 $/\$ ..^
155	141, 154	mpdan 702	. . . . . . . . . . . . . . . 16
156	150	simpld 475	. . . . . . . . . . . . . . . . 17 $/\$
157	156	simpld 475	. . . . . . . . . . . . . . . 16
158		0p1e1 11132	. . . . . . . . . . . . . . . . . 18
159	158	fveq2i 6194	. . . . . . . . . . . . . . . . 17
160	159	a1i 11	. . . . . . . . . . . . . . . 16
161	155, 157, 160	3brtr3d 4684	. . . . . . . . . . . . . . 15
162	114, 112	posdifd 10614	. . . . . . . . . . . . . . 15
163	161, 162	mpbid 222	. . . . . . . . . . . . . 14
164	134	a1i 11	. . . . . . . . . . . . . 14
165	115, 138, 163, 164	divgt0d 10959	. . . . . . . . . . . . 13
166	116, 165	elrpd 11869	. . . . . . . . . . . 12
167	166	adantr 481	. . . . . . . . . . 11 $/\$ ..^
168	137, 167	ifcld 4131	. . . . . . . . . 10 $/\$ ..^
169	42, 168	ltaddrpd 11905	. . . . . . . . 9 $/\$ ..^
170	42, 119, 169	ltled 10185	. . . . . . . 8 $/\$ ..^
171	170, 106	syl6breqr 4695	. . . . . . 7 $/\$ ..^
172	42, 111	readdcld 10069	. . . . . . . . 9 $/\$ ..^
173		iftrue 4092	. . . . . . . . . . . . 13
174	173	adantl 482	. . . . . . . . . . . 12 $/\$ ..^ $/\$
175	111	leidd 10594	. . . . . . . . . . . . 13 $/\$ ..^
176	175	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$
177	174, 176	eqbrtrd 4675	. . . . . . . . . . 11 $/\$ ..^ $/\$
178		iffalse 4095	. . . . . . . . . . . . 13
179	178	adantl 482	. . . . . . . . . . . 12 $/\$ ..^ $/\$
180	115	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
181	110	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
182		2rp 11837	. . . . . . . . . . . . . 14
183	182	a1i 11	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
184		simpr 477	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
185	180, 181, 184	nltled 10187	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
186	180, 181, 183, 185	lediv1dd 11930	. . . . . . . . . . . 12 $/\$ ..^ $/\$
187	179, 186	eqbrtrd 4675	. . . . . . . . . . 11 $/\$ ..^ $/\$
188	177, 187	pm2.61dan 832	. . . . . . . . . 10 $/\$ ..^
189	118, 111, 42, 188	leadd2dd 10642	. . . . . . . . 9 $/\$ ..^
190	42	recnd 10068	. . . . . . . . . . . . . . . 16 $/\$ ..^
191	109	recnd 10068	. . . . . . . . . . . . . . . 16 $/\$ ..^
192	190, 191	addcomd 10238	. . . . . . . . . . . . . . 15 $/\$ ..^
193	192	oveq1d 6665	. . . . . . . . . . . . . 14 $/\$ ..^
194	193	oveq1d 6665	. . . . . . . . . . . . 13 $/\$ ..^
195		halfaddsub 11265	. . . . . . . . . . . . . . 15 $/\$ $/\$
196	191, 190, 195	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
197	196	simprd 479	. . . . . . . . . . . . 13 $/\$ ..^
198	194, 197	eqtrd 2656	. . . . . . . . . . . 12 $/\$ ..^
199	190, 191	addcld 10059	. . . . . . . . . . . . . 14 $/\$ ..^
200	199	halfcld 11277	. . . . . . . . . . . . 13 $/\$ ..^
201	111	recnd 10068	. . . . . . . . . . . . 13 $/\$ ..^
202	200, 201, 190	subsub23d 39499	. . . . . . . . . . . 12 $/\$ ..^
203	198, 202	mpbid 222	. . . . . . . . . . 11 $/\$ ..^
204	200, 190, 201	subaddd 10410	. . . . . . . . . . 11 $/\$ ..^
205	203, 204	mpbid 222	. . . . . . . . . 10 $/\$ ..^
206		avglt2 11271	. . . . . . . . . . . 12 $/\$
207	42, 109, 206	syl2anc 693	. . . . . . . . . . 11 $/\$ ..^
208	131, 207	mpbid 222	. . . . . . . . . 10 $/\$ ..^
209	205, 208	eqbrtrd 4675	. . . . . . . . 9 $/\$ ..^
210	119, 172, 109, 189, 209	lelttrd 10195	. . . . . . . 8 $/\$ ..^
211	106, 210	syl5eqbr 4688	. . . . . . 7 $/\$ ..^
212	109	rexrd 10089	. . . . . . . 8 $/\$ ..^
213		elico2 12237	. . . . . . . 8 $/\$ $/\$ $/\$
214	42, 212, 213	syl2anc 693	. . . . . . 7 $/\$ ..^ $/\$ $/\$
215	120, 171, 211, 214	mpbir3and 1245	. . . . . 6 $/\$ ..^
216	215	adantr 481	. . . . 5 $/\$ ..^ $/\$
217	114	ad2antrr 762	. . . . . . . 8 $/\$ ..^ $/\$
218	113	simp2d 1074	. . . . . . . . 9
219	218	ad2antrr 762	. . . . . . . 8 $/\$ ..^ $/\$
220	113	simp3d 1075	. . . . . . . . 9
221	220	ad2antrr 762	. . . . . . . 8 $/\$ ..^ $/\$
222	42	adantr 481	. . . . . . . 8 $/\$ ..^ $/\$
223		simpr 477	. . . . . . . 8 $/\$ ..^ $/\$
224	169, 106	syl6breqr 4695	. . . . . . . . . 10 $/\$ ..^
225	218, 114	resubcld 10458	. . . . . . . . . . . . . 14
226	11, 225	syl5eqel 2705	. . . . . . . . . . . . 13
227	226	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
228	111	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
229	116	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
230	110	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
231	115	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
232	182	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
233		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
234	230, 231, 232, 233	ltdiv1dd 11929	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
235	228, 229, 234	ltled 10185	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
236	174, 235	eqbrtrd 4675	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
237	178	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
238	116	leidd 10594	. . . . . . . . . . . . . . . . 17
239	238	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
240	237, 239	eqbrtrd 4675	. . . . . . . . . . . . . . 15 $/\$
241	240	adantlr 751	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
242	236, 241	pm2.61dan 832	. . . . . . . . . . . . 13 $/\$ ..^
243	225	rehalfcld 11279	. . . . . . . . . . . . . . . 16
244	182	a1i 11	. . . . . . . . . . . . . . . . 17
245	114	rexrd 10089	. . . . . . . . . . . . . . . . . . 19
246	218	rexrd 10089	. . . . . . . . . . . . . . . . . . 19
247	3, 2, 1	fourierdlem15 40339	. . . . . . . . . . . . . . . . . . . 20
248	247, 103	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19
249		iccleub 12229	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
250	245, 246, 248, 249	syl3anc 1326	. . . . . . . . . . . . . . . . . 18
251	112, 218, 114, 250	lesub1dd 10643	. . . . . . . . . . . . . . . . 17
252	115, 225, 244, 251	lediv1dd 11930	. . . . . . . . . . . . . . . 16
253	11	eqcomi 2631	. . . . . . . . . . . . . . . . . 18
254	253	oveq1i 6660	. . . . . . . . . . . . . . . . 17
255	114, 218	posdifd 10614	. . . . . . . . . . . . . . . . . . . . 21
256	220, 255	mpbid 222	. . . . . . . . . . . . . . . . . . . 20
257	256, 11	syl6breqr 4695	. . . . . . . . . . . . . . . . . . 19
258	226, 257	elrpd 11869	. . . . . . . . . . . . . . . . . 18
259		rphalflt 11860	. . . . . . . . . . . . . . . . . 18
260	258, 259	syl 17	. . . . . . . . . . . . . . . . 17
261	254, 260	syl5eqbr 4688	. . . . . . . . . . . . . . . 16
262	116, 243, 226, 252, 261	lelttrd 10195	. . . . . . . . . . . . . . 15
263	116, 226, 262	ltled 10185	. . . . . . . . . . . . . 14
264	263	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^
265	118, 117, 227, 242, 264	letrd 10194	. . . . . . . . . . . 12 $/\$ ..^
266	118, 227, 42, 265	leadd2dd 10642	. . . . . . . . . . 11 $/\$ ..^
267	106, 266	syl5eqbr 4688	. . . . . . . . . 10 $/\$ ..^
268	42	rexrd 10089	. . . . . . . . . . 11 $/\$ ..^
269	42, 227	readdcld 10069	. . . . . . . . . . 11 $/\$ ..^
270		elioc2 12236	. . . . . . . . . . 11 $/\$ $/\$ $/\$
271	268, 269, 270	syl2anc 693	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
272	120, 224, 267, 271	mpbir3and 1245	. . . . . . . . 9 $/\$ ..^
273	272	adantr 481	. . . . . . . 8 $/\$ ..^ $/\$
274	217, 219, 221, 11, 12, 222, 223, 273	fourierdlem26 40350	. . . . . . 7 $/\$ ..^ $/\$
275	106	a1i 11	. . . . . . . . . 10 $/\$ ..^
276	275	oveq1d 6665	. . . . . . . . 9 $/\$ ..^
277	276	oveq2d 6666	. . . . . . . 8 $/\$ ..^
278	277	adantr 481	. . . . . . 7 $/\$ ..^ $/\$
279	118	recnd 10068	. . . . . . . . . 10 $/\$ ..^
280	190, 279	pncan2d 10394	. . . . . . . . 9 $/\$ ..^
281	280	oveq2d 6666	. . . . . . . 8 $/\$ ..^
282	281	adantr 481	. . . . . . 7 $/\$ ..^ $/\$
283	274, 278, 282	3eqtrd 2660	. . . . . 6 $/\$ ..^ $/\$
284	173	oveq2d 6666	. . . . . . . . . 10
285	284	adantl 482	. . . . . . . . 9 $/\$ ..^ $/\$
286	114	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
287	286, 111	readdcld 10069	. . . . . . . . . . 11 $/\$ ..^
288	287	adantr 481	. . . . . . . . . 10 $/\$ ..^ $/\$
289	286, 117	readdcld 10069	. . . . . . . . . . 11 $/\$ ..^
290	289	adantr 481	. . . . . . . . . 10 $/\$ ..^ $/\$
291	112	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$
292	114	ad2antrr 762	. . . . . . . . . . 11 $/\$ ..^ $/\$
293	228, 229, 292, 234	ltadd2dd 10196	. . . . . . . . . 10 $/\$ ..^ $/\$
294	112	recnd 10068	. . . . . . . . . . . . . . . 16
295	114	recnd 10068	. . . . . . . . . . . . . . . 16
296		halfaddsub 11265	. . . . . . . . . . . . . . . 16 $/\$ $/\$
297	294, 295, 296	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$
298	297	simprd 479	. . . . . . . . . . . . . 14
299	298	oveq1d 6665	. . . . . . . . . . . . 13
300	112, 114	readdcld 10069	. . . . . . . . . . . . . . . 16
301	300	rehalfcld 11279	. . . . . . . . . . . . . . 15
302	301	recnd 10068	. . . . . . . . . . . . . 14
303	116	recnd 10068	. . . . . . . . . . . . . 14
304	302, 303	npcand 10396	. . . . . . . . . . . . 13
305	299, 304	eqtr3d 2658	. . . . . . . . . . . 12
306	112, 112	readdcld 10069	. . . . . . . . . . . . . 14
307	114, 112, 112, 161	ltadd2dd 10196	. . . . . . . . . . . . . 14
308	300, 306, 244, 307	ltdiv1dd 11929	. . . . . . . . . . . . 13
309	294	2timesd 11275	. . . . . . . . . . . . . . . 16
310	309	eqcomd 2628	. . . . . . . . . . . . . . 15
311	310	oveq1d 6665	. . . . . . . . . . . . . 14
312		2cnd 11093	. . . . . . . . . . . . . . 15
313		2ne0 11113	. . . . . . . . . . . . . . . 16
314	313	a1i 11	. . . . . . . . . . . . . . 15
315	294, 312, 314	divcan3d 10806	. . . . . . . . . . . . . 14
316	311, 315	eqtrd 2656	. . . . . . . . . . . . 13
317	308, 316	breqtrd 4679	. . . . . . . . . . . 12
318	305, 317	eqbrtrd 4675	. . . . . . . . . . 11
319	318	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$
320	288, 290, 291, 293, 319	lttrd 10198	. . . . . . . . 9 $/\$ ..^ $/\$
321	285, 320	eqbrtrd 4675	. . . . . . . 8 $/\$ ..^ $/\$
322	178	oveq2d 6666	. . . . . . . . . 10
323	322	adantl 482	. . . . . . . . 9 $/\$ ..^ $/\$
324	318	ad2antrr 762	. . . . . . . . 9 $/\$ ..^ $/\$
325	323, 324	eqbrtrd 4675	. . . . . . . 8 $/\$ ..^ $/\$
326	321, 325	pm2.61dan 832	. . . . . . 7 $/\$ ..^
327	326	adantr 481	. . . . . 6 $/\$ ..^ $/\$
328	283, 327	eqbrtrd 4675	. . . . 5 $/\$ ..^ $/\$
329		eqid 2622	. . . . 5
330	11, 3, 90, 91, 92, 93, 94, 24, 25, 26, 27, 12, 104, 105, 216, 328, 329	fourierdlem63 40386	. . . 4 $/\$ ..^ $/\$
331	14	a1i 11	. . . . . . . . 9 $/\$ ..^ $/\$ ..^
332	57	adantl 482	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$ ..^ ..^
333	60	a1i 11	. . . . . . . . 9 $/\$ ..^ $/\$ ..^
334	331, 332, 222, 333	fvmptd 6288	. . . . . . . 8 $/\$ ..^ $/\$ ..^
335		fveq2 6191	. . . . . . . . . . . . 13
336	13	a1i 11	. . . . . . . . . . . . . 14
337		iftrue 4092	. . . . . . . . . . . . . . 15
338	337	adantl 482	. . . . . . . . . . . . . 14 $/\$
339		ubioc1 12227	. . . . . . . . . . . . . . 15 $/\$ $/\$
340	245, 246, 220, 339	syl3anc 1326	. . . . . . . . . . . . . 14
341	336, 338, 340, 114	fvmptd 6288	. . . . . . . . . . . . 13
342	335, 341	sylan9eqr 2678	. . . . . . . . . . . 12 $/\$
343	342	breq2d 4665	. . . . . . . . . . 11 $/\$
344	343	rabbidv 3189	. . . . . . . . . 10 $/\$ ..^ ..^
345	344	supeq1d 8352	. . . . . . . . 9 $/\$ ..^ ..^
346	345	adantlr 751	. . . . . . . 8 $/\$ ..^ $/\$ ..^ ..^
347		simpl 473	. . . . . . . . . . . . . . . 16 $/\$ ..^
348		elrabi 3359	. . . . . . . . . . . . . . . . 17 ..^ ..^
349	348	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ ..^ ..^
350		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
351	350	breq1d 4663	. . . . . . . . . . . . . . . . . . 19
352	351	elrab 3363	. . . . . . . . . . . . . . . . . 18 ..^ ..^ $/\$
353	352	simprbi 480	. . . . . . . . . . . . . . . . 17 ..^
354	353	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ ..^
355		simp3 1063	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
356	114	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
357	112	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
358	9	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^
359	18	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^
360	358, 359	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^
361	360	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
362	161	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
363		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
364		elfzoelz 12470	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
365	364	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
366		1e0p1 11552	. . . . . . . . . . . . . . . . . . . . . . . . 25
367		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$
368		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$
369	365	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$
370	368, 369	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$
371	367, 370	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
372		0zd 11389	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$
373		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
374	372, 365, 373	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
375	371, 374	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
376	366, 375	syl5eqbr 4688	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
377		eluz2 11693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
378	363, 365, 376, 377	syl3anbrc 1246	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
379	9	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
380		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
381		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
382	381	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
383		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
384		0lt1 10550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
385	384	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
386		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
387	380, 383, 382, 385, 386	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
388	380, 382, 387	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
389	388	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
390	382	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$
391	100	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
392	391	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$
393	364	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
394	393	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$
395		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
396	395	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$
397		elfzolt2 12479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
398	397	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$
399	390, 394, 392, 396, 398	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$
400	390, 392, 399	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
401	381	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$
402		0zd 11389	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$
403	100	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$
404		elfz 12332	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
405	401, 402, 403, 404	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$ $/\$
406	389, 400, 405	mpbir2and 957	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
407	379, 406	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
408	407	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
409	9	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
410		0zd 11389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^ $/\$
411	100	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^ $/\$
412		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
413	412	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^ $/\$
414	410, 411, 413	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$ $/\$ $/\$
415		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
416	412	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
417		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
418	384	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
419		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
420	415, 417, 416, 418, 419	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
421	415, 416, 420	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
422	421	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$
423	413	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^ $/\$
424	391	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^ $/\$
425	393	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ ..^ $/\$
426	416	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$
427		peano2rem 10348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
428	393, 427	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
429	428	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$
430	393	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$
431		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
432	431	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$
433	430	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$
434	426, 429, 430, 432, 433	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$
435	434	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ ..^ $/\$
436	397	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ ..^ $/\$
437	423, 425, 424, 435, 436	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^ $/\$
438	423, 424, 437	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$
439	414, 422, 438	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
440		elfz2 12333	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
441	439, 440	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
442	409, 441	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
443	413	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^ $/\$
444	410, 411, 443	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$ $/\$ $/\$
445	416, 417	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
446	416, 417, 420, 418	addgt0d 10602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
447	415, 445, 446	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
448	447	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$
449	445	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^ $/\$
450	445	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
451		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
452	450, 451	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
453	452	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
454	453	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$
455		peano2re 10209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
456		peano2rem 10348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
457	426, 455, 456	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ $/\$
458		peano2re 10209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
459		peano2rem 10348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
460	429, 458, 459	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ $/\$
461		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ $/\$
462		elfzel2 12340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
463	462	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
464	463, 417	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
465	416, 463, 417, 431	leadd1dd 10641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
466	445, 464, 417, 465	lesub1dd 10643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
467	466	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ $/\$
468	457, 460, 461, 467	leadd1dd 10641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ $/\$
469		peano2zm 11420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
470	364, 469	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ..^
471	470	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ..^
472	471	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
473		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
474	472, 473	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
475	393	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ..^
476	475, 473	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ..^
477	474, 476	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
478	477	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ $/\$
479	468, 478	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$
480	454, 479	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$
481	480	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ ..^ $/\$
482	449, 425, 424, 481, 436	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^ $/\$
483	449, 424, 482	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$
484	444, 448, 483	jca32 558	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$
485		elfz2 12333	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
486	484, 485	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
487	409, 486	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
488		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
489		0zd 11389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ $/\$
490	412	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ $/\$
491	421	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ $/\$
492		eluz2 11693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
493	489, 490, 491, 492	syl3anbrc 1246	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ $/\$
494		elfzoel2 12469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
495	494	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ $/\$
496	495	zred 11482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ $/\$
497	397	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ $/\$
498	426, 430, 496, 434, 497	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ $/\$
499		elfzo2 12473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^ $/\$ $/\$
500	493, 495, 498, 499	syl3anbrc 1246	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ $/\$ ..^
501	500	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$ ..^
502		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
503	502	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$ ..^
504		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
505		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
506	505	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
507	504, 506	breq12d 4666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
508	503, 507	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ ..^
509	508, 152	chvarv 2263	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^
510	488, 501, 509	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
511	442, 487, 510	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
512	511	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
513	378, 408, 512	monoord 12831	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
514	356, 357, 361, 362, 513	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
515	356, 361	ltnled 10184	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
516	514, 515	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
517	516	ex 450	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
518	517	3adant3 1081	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
519	355, 518	mt4d 152	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
520		elfzole1 12478	. . . . . . . . . . . . . . . . . 18 ..^
521	520	3ad2ant2 1083	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
522	393	3ad2ant2 1083	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
523		0red 10041	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
524	522, 523	letri3d 10179	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
525	519, 521, 524	mpbir2and 957	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
526	347, 349, 354, 525	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$ ..^
527		velsn 4193	. . . . . . . . . . . . . . 15
528	526, 527	sylibr 224	. . . . . . . . . . . . . 14 $/\$ ..^
529	528	ralrimiva 2966	. . . . . . . . . . . . 13 ..^
530		dfss3 3592	. . . . . . . . . . . . 13 ..^ ..^
531	529, 530	sylibr 224	. . . . . . . . . . . 12 ..^
532	157, 114	eqeltrd 2701	. . . . . . . . . . . . . . 15
533	532, 157	eqled 10140	. . . . . . . . . . . . . 14
534	145	breq1d 4663	. . . . . . . . . . . . . . 15
535	534	elrab 3363	. . . . . . . . . . . . . 14 ..^ ..^ $/\$
536	141, 533, 535	sylanbrc 698	. . . . . . . . . . . . 13 ..^
537	536	snssd 4340	. . . . . . . . . . . 12 ..^
538	531, 537	eqssd 3620	. . . . . . . . . . 11 ..^
539	538	supeq1d 8352	. . . . . . . . . 10 ..^
540		supsn 8378	. . . . . . . . . . . 12 $/\$
541	59, 142, 540	mp2an 708	. . . . . . . . . . 11
542	541	a1i 11	. . . . . . . . . 10
543	539, 542	eqtrd 2656	. . . . . . . . 9 ..^
544	543	ad2antrr 762	. . . . . . . 8 $/\$ ..^ $/\$ ..^
545	334, 346, 544	3eqtrd 2660	. . . . . . 7 $/\$ ..^ $/\$
546	545	oveq1d 6665	. . . . . 6 $/\$ ..^ $/\$
547	546	fveq2d 6195	. . . . 5 $/\$ ..^ $/\$
548	547, 159	syl6req 2673	. . . 4 $/\$ ..^ $/\$
549	330, 548	breqtrd 4679	. . 3 $/\$ ..^ $/\$
550	65	adantr 481	. . . 4 $/\$ ..^ $/\$ $/\$
551		simplr 792	. . . 4 $/\$ ..^ $/\$ ..^
552	13	a1i 11	. . . . . . . . . . 11 $/\$ ..^ $/\$
553		simpr 477	. . . . . . . . . . . . . . . 16 $/\$
554		neqne 2802	. . . . . . . . . . . . . . . . 17
555	554	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
556	553, 555	eqnetrd 2861	. . . . . . . . . . . . . . 15 $/\$
557	556	neneqd 2799	. . . . . . . . . . . . . 14 $/\$
558	557	iffalsed 4097	. . . . . . . . . . . . 13 $/\$
559	558, 553	eqtrd 2656	. . . . . . . . . . . 12 $/\$
560	559	adantll 750	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
561	114, 218, 220, 11, 12	fourierdlem4 40328	. . . . . . . . . . . . . 14
562	561	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^
563	562, 42	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$ ..^
564	563	adantr 481	. . . . . . . . . . 11 $/\$ ..^ $/\$
565	552, 560, 564, 564	fvmptd 6288	. . . . . . . . . 10 $/\$ ..^ $/\$
566	565	eqcomd 2628	. . . . . . . . 9 $/\$ ..^ $/\$
567	114, 218, 220, 13	fourierdlem17 40341	. . . . . . . . . . . . 13
568	567	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
569	114, 218	iccssred 39727	. . . . . . . . . . . . 13
570	569	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
571	568, 570	fssd 6057	. . . . . . . . . . 11 $/\$ ..^
572	571, 563	ffvelrnd 6360	. . . . . . . . . 10 $/\$ ..^
573	572	adantr 481	. . . . . . . . 9 $/\$ ..^ $/\$
574	566, 573	eqeltrd 2701	. . . . . . . 8 $/\$ ..^ $/\$
575	218	ad2antrr 762	. . . . . . . 8 $/\$ ..^ $/\$
576	245	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
577	218	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
578		elioc2 12236	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
579	576, 577, 578	syl2anc 693	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
580	563, 579	mpbid 222	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
581	580	simp3d 1075	. . . . . . . . 9 $/\$ ..^
582	581	adantr 481	. . . . . . . 8 $/\$ ..^ $/\$
583	554	necomd 2849	. . . . . . . . 9
584	583	adantl 482	. . . . . . . 8 $/\$ ..^ $/\$
585	574, 575, 582, 584	leneltd 10191	. . . . . . 7 $/\$ ..^ $/\$
586	585	adantr 481	. . . . . 6 $/\$ ..^ $/\$ $/\$
587		oveq1 6657	. . . . . . . . . . 11
588	2	nncnd 11036	. . . . . . . . . . . 12
589		1cnd 10056	. . . . . . . . . . . 12
590	588, 589	npcand 10396	. . . . . . . . . . 11
591	587, 590	sylan9eqr 2678	. . . . . . . . . 10 $/\$
592	591	fveq2d 6195	. . . . . . . . 9 $/\$
593	156	simprd 479	. . . . . . . . . 10
594	593	adantr 481	. . . . . . . . 9 $/\$
595	592, 594	eqtr2d 2657	. . . . . . . 8 $/\$
596	595	adantlr 751	. . . . . . 7 $/\$ ..^ $/\$
597	596	adantlr 751	. . . . . 6 $/\$ ..^ $/\$ $/\$
598	586, 597	breqtrd 4679	. . . . 5 $/\$ ..^ $/\$ $/\$
599	566	adantr 481	. . . . . 6 $/\$ ..^ $/\$ $/\$
600		ssrab2 3687	. . . . . . . . . . . . 13 ..^ ..^
601		fzssz 12343	. . . . . . . . . . . . . . 15
602	17, 601	sstri 3612	. . . . . . . . . . . . . 14 ..^
603		zssre 11384	. . . . . . . . . . . . . 14
604	602, 603	sstri 3612	. . . . . . . . . . . . 13 ..^
605	600, 604	sstri 3612	. . . . . . . . . . . 12 ..^
606	605	a1i 11	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$ ..^
607	56	neeq1d 2853	. . . . . . . . . . . . . . 15 ..^ ..^
608	67, 607	imbi12d 334	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ ..^
609	141	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^
610	533	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
611		iftrue 4092	. . . . . . . . . . . . . . . . . . . . 21
612	611	eqcomd 2628	. . . . . . . . . . . . . . . . . . . 20
613	612	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
614	610, 613	breqtrd 4679	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
615	532	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
616	114	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
617	616	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
618	218	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
619		iocssre 12253	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
620	617, 618, 619	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
621	561	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
622	620, 621	sseldd 3604	. . . . . . . . . . . . . . . . . . . . 21 $/\$
623	157	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
624		elioc2 12236	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
625	617, 618, 624	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
626	621, 625	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
627	626	simp2d 1074	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
628	623, 627	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . 21 $/\$
629	615, 622, 628	ltled 10185	. . . . . . . . . . . . . . . . . . . 20 $/\$
630	629	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
631		iffalse 4095	. . . . . . . . . . . . . . . . . . . . 21
632	631	eqcomd 2628	. . . . . . . . . . . . . . . . . . . 20
633	632	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
634	630, 633	breqtrd 4679	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
635	614, 634	pm2.61dan 832	. . . . . . . . . . . . . . . . 17 $/\$
636	13	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$
637		eqeq1 2626	. . . . . . . . . . . . . . . . . . . 20
638		id 22	. . . . . . . . . . . . . . . . . . . 20
639	637, 638	ifbieq2d 4111	. . . . . . . . . . . . . . . . . . 19
640	639	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
641	616, 622	ifcld 4131	. . . . . . . . . . . . . . . . . 18 $/\$
642	636, 640, 621, 641	fvmptd 6288	. . . . . . . . . . . . . . . . 17 $/\$
643	635, 642	breqtrrd 4681	. . . . . . . . . . . . . . . 16 $/\$
644	145	breq1d 4663	. . . . . . . . . . . . . . . . 17
645	644	elrab 3363	. . . . . . . . . . . . . . . 16 ..^ ..^ $/\$
646	609, 643, 645	sylanbrc 698	. . . . . . . . . . . . . . 15 $/\$ ..^
647		ne0i 3921	. . . . . . . . . . . . . . 15 ..^ ..^
648	646, 647	syl 17	. . . . . . . . . . . . . 14 $/\$ ..^
649	608, 648	vtoclg 3266	. . . . . . . . . . . . 13 $/\$ ..^
650	42, 65, 649	sylc 65	. . . . . . . . . . . 12 $/\$ ..^ ..^
651	650	ad2antrr 762	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$ ..^
652	605	a1i 11	. . . . . . . . . . . . 13 $/\$ ..^ ..^
653		fzofi 12773	. . . . . . . . . . . . . . 15 ..^
654		ssfi 8180	. . . . . . . . . . . . . . 15 ..^ $/\$ ..^ ..^ ..^
655	653, 600, 654	mp2an 708	. . . . . . . . . . . . . 14 ..^
656	655	a1i 11	. . . . . . . . . . . . 13 $/\$ ..^ ..^
657		fimaxre2 10969	. . . . . . . . . . . . 13 ..^ $/\$ ..^ ..^
658	652, 656, 657	syl2anc 693	. . . . . . . . . . . 12 $/\$ ..^ ..^
659	658	ad2antrr 762	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$ ..^
660		0red 10041	. . . . . . . . . . . . . . . 16 $/\$ ..^
661	604, 47	sseldi 3601	. . . . . . . . . . . . . . . . 17 $/\$ ..^
662		1red 10055	. . . . . . . . . . . . . . . . 17 $/\$ ..^
663	661, 662	readdcld 10069	. . . . . . . . . . . . . . . 16 $/\$ ..^
664		elfzouz 12474	. . . . . . . . . . . . . . . . . 18 ..^
665		eluzle 11700	. . . . . . . . . . . . . . . . . 18
666	47, 664, 665	3syl 18	. . . . . . . . . . . . . . . . 17 $/\$ ..^
667	384	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ ..^
668	661, 662, 666, 667	addgegt0d 10601	. . . . . . . . . . . . . . . 16 $/\$ ..^
669	660, 663, 668	ltled 10185	. . . . . . . . . . . . . . 15 $/\$ ..^
670	669	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
671	661	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
672		1red 10055	. . . . . . . . . . . . . . . . . 18
673	391, 672	resubcld 10458	. . . . . . . . . . . . . . . . 17
674	673	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
675		1red 10055	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
676		elfzolt2 12479	. . . . . . . . . . . . . . . . . . . 20 ..^
677	47, 676	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
678	601, 43	sseldi 3601	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
679	100	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
680		zltlem1 11430	. . . . . . . . . . . . . . . . . . . 20 $/\$
681	678, 679, 680	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
682	677, 681	mpbid 222	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
683	682	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
684		neqne 2802	. . . . . . . . . . . . . . . . . . 19
685	684	necomd 2849	. . . . . . . . . . . . . . . . . 18
686	685	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
687	671, 674, 683, 686	leneltd 10191	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
688	671, 674, 675, 687	ltadd1dd 10638	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
689	590	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
690	688, 689	breqtrd 4679	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
691	601, 49	sseldi 3601	. . . . . . . . . . . . . . . 16 $/\$ ..^
692	691	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
693		0zd 11389	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
694	100	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
695		elfzo 12472	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^ $/\$
696	692, 693, 694, 695	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ ..^ $/\$
697	670, 690, 696	mpbir2and 957	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
698	697	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$ ..^
699		simpr 477	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
700		fveq2 6191	. . . . . . . . . . . . . 14
701	700	breq1d 4663	. . . . . . . . . . . . 13
702	701	elrab 3363	. . . . . . . . . . . 12 ..^ ..^ $/\$
703	698, 699, 702	sylanbrc 698	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$ ..^
704		suprub 10984	. . . . . . . . . . 11 ..^ $/\$ ..^ $/\$ ..^ $/\$ ..^ ..^
705	606, 651, 659, 703, 704	syl31anc 1329	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$ ..^
706	62	eqcomd 2628	. . . . . . . . . . 11 $/\$ ..^ ..^
707	706	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$ ..^
708	705, 707	breqtrd 4679	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$
709	661	ltp1d 10954	. . . . . . . . . . 11 $/\$ ..^
710	661, 663	ltnled 10184	. . . . . . . . . . 11 $/\$ ..^
711	709, 710	mpbid 222	. . . . . . . . . 10 $/\$ ..^
712	711	ad2antrr 762	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$
713	708, 712	pm2.65da 600	. . . . . . . 8 $/\$ ..^ $/\$
714	572	adantr 481	. . . . . . . . 9 $/\$ ..^ $/\$
715	50	adantr 481	. . . . . . . . 9 $/\$ ..^ $/\$
716	714, 715	ltnled 10184	. . . . . . . 8 $/\$ ..^ $/\$
717	713, 716	mpbird 247	. . . . . . 7 $/\$ ..^ $/\$
718	717	adantlr 751	. . . . . 6 $/\$ ..^ $/\$ $/\$
719	599, 718	eqbrtrd 4675	. . . . 5 $/\$ ..^ $/\$ $/\$
720	598, 719	pm2.61dan 832	. . . 4 $/\$ ..^ $/\$
721	2	3ad2ant1 1082	. . . . . 6 $/\$ ..^ $/\$
722	1	3ad2ant1 1082	. . . . . 6 $/\$ ..^ $/\$
723	21	3ad2ant1 1082	. . . . . 6 $/\$ ..^ $/\$
724	22	3ad2ant1 1082	. . . . . 6 $/\$ ..^ $/\$
725	23	3ad2ant1 1082	. . . . . 6 $/\$ ..^ $/\$
726	49	3adant3 1081	. . . . . 6 $/\$ ..^ $/\$
727		simp2 1062	. . . . . 6 $/\$ ..^ $/\$ ..^
728	42	leidd 10594	. . . . . . . 8 $/\$ ..^
729		elico2 12237	. . . . . . . . 9 $/\$ $/\$ $/\$
730	42, 212, 729	syl2anc 693	. . . . . . . 8 $/\$ ..^ $/\$ $/\$
731	42, 728, 131, 730	mpbir3and 1245	. . . . . . 7 $/\$ ..^
732	731	3adant3 1081	. . . . . 6 $/\$ ..^ $/\$
733		simp3 1063	. . . . . 6 $/\$ ..^ $/\$
734		eqid 2622	. . . . . 6
735	11, 3, 721, 722, 723, 724, 725, 24, 25, 26, 27, 12, 726, 727, 732, 733, 734	fourierdlem63 40386	. . . . 5 $/\$ ..^ $/\$
736	735	3adant1r 1319	. . . 4 $/\$ $/\$ ..^ $/\$
737	550, 551, 720, 736	syl3anc 1326	. . 3 $/\$ ..^ $/\$
738	549, 737	pm2.61dan 832	. 2 $/\$ ..^
739		ioossioo 12265	. 2 $/\$ $/\$ $/\$
740	45, 51, 89, 738, 739	syl22anc 1327	1 $/\$ ..^

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200

cun 3572

wss 3574

c0 3915

cif 4086

csn 4177

cpr 4179 class class class wbr 4653

cmpt 4729

wor 5034

crn 5115

cio 5849

wf 5884

cfv 5888

wiso 5889 (class class class)co 6650

cmap 7857

cfn 7955

csup 8346

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cxr 10073

clt 10074

cle 10075

cmin 10266

cdiv 10684

cn 11020

c2 11070

cz 11377

cuz 11687

crp 11832

cioo 12175

cioc 12176

cico 12177

cicc 12178

cfz 12326 ..^cfzo 12465

cfl 12591

chash 13117

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-cmp 21190

This theorem is referenced by: fourierdlem89 40412 fourierdlem90 40413 fourierdlem91 40414

W3C validator