fourierdlem112 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem112 40435

Description: Here abbreviations (local definitions) are introduced to prove the fourier 40442 theorem.

is the m_th partial sum of the fourier series. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem112.f
fourierdlem112.d
fourierdlem112.p	$/\$ $/\$ ..^
fourierdlem112.m
fourierdlem112.q
fourierdlem112.n
fourierdlem112.v
fourierdlem112.x
fourierdlem112.xran
fourierdlem112.t
fourierdlem112.fper	$/\$
fourierdlem112.fcn	$/\$ ..^
fourierdlem112.c	$/\$ ..^ lim
fourierdlem112.u	$/\$ ..^ lim
fourierdlem112.fdvcn	$/\$ ..^
fourierdlem112.e	lim
fourierdlem112.i	lim
fourierdlem112.l	lim
fourierdlem112.r	lim
fourierdlem112.a
fourierdlem112.b
fourierdlem112.z
fourierdlem112.23
fourierdlem112.fbd
fourierdlem112.fdvbd
fourierdlem112.25

**Assertion**
Ref	Expression
fourierdlem112	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem fourierdlem112 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem112.23	. . . . 5
2		fveq2 6191	. . . . . . . 8
3		oveq1 6657	. . . . . . . . 9
4	3	fveq2d 6195	. . . . . . . 8
5	2, 4	oveq12d 6668	. . . . . . 7
6		fveq2 6191	. . . . . . . 8
7	3	fveq2d 6195	. . . . . . . 8
8	6, 7	oveq12d 6668	. . . . . . 7
9	5, 8	oveq12d 6668	. . . . . 6
10	9	cbvmptv 4750	. . . . 5
11	1, 10	eqtri 2644	. . . 4
12		seqeq3 12806	. . . 4
13	11, 12	mp1i 13	. . 3
14		nnuz 11723	. . . . 5
15		1zzd 11408	. . . . 5
16		nfv 1843	. . . . . . 7
17		nfcv 2764	. . . . . . . 8
18		nfcv 2764	. . . . . . . . 9
19		nfcv 2764	. . . . . . . . . 10
20		nfcv 2764	. . . . . . . . . 10
21		nfcv 2764	. . . . . . . . . 10
22	19, 20, 21	nfov 6676	. . . . . . . . 9
23	18, 22	nfitg 23541	. . . . . . . 8
24	17, 23	nfmpt 4746	. . . . . . 7
25		nfcv 2764	. . . . . . . . 9
26	25, 22	nfitg 23541	. . . . . . . 8
27	17, 26	nfmpt 4746	. . . . . . 7
28		fourierdlem112.z	. . . . . . . 8
29		fourierdlem112.a	. . . . . . . . . . . . 13
30		nfmpt1 4747	. . . . . . . . . . . . 13
31	29, 30	nfcxfr 2762	. . . . . . . . . . . 12
32		nfcv 2764	. . . . . . . . . . . 12
33	31, 32	nffv 6198	. . . . . . . . . . 11
34		nfcv 2764	. . . . . . . . . . 11
35		nfcv 2764	. . . . . . . . . . 11
36	33, 34, 35	nfov 6676	. . . . . . . . . 10
37		nfcv 2764	. . . . . . . . . 10
38		nfcv 2764	. . . . . . . . . . 11
39	38	nfsum1 14420	. . . . . . . . . 10
40	36, 37, 39	nfov 6676	. . . . . . . . 9
41	17, 40	nfmpt 4746	. . . . . . . 8
42	28, 41	nfcxfr 2762	. . . . . . 7
43		fourierdlem112.f	. . . . . . . 8
44		fourierdlem112.25	. . . . . . . 8
45		eqid 2622	. . . . . . . 8 $/\$ $/\$ ..^ $/\$ $/\$ ..^
46		picn 24211	. . . . . . . . . . . . 13
47	46	2timesi 11147	. . . . . . . . . . . 12
48		fourierdlem112.t	. . . . . . . . . . . 12
49	46, 46	subnegi 10360	. . . . . . . . . . . 12
50	47, 48, 49	3eqtr4i 2654	. . . . . . . . . . 11
51		fourierdlem112.p	. . . . . . . . . . 11 $/\$ $/\$ ..^
52		fourierdlem112.m	. . . . . . . . . . 11
53		fourierdlem112.q	. . . . . . . . . . 11
54		pire 24210	. . . . . . . . . . . . . 14
55	54	a1i 11	. . . . . . . . . . . . 13
56	55	renegcld 10457	. . . . . . . . . . . 12
57	56, 44	readdcld 10069	. . . . . . . . . . 11
58	55, 44	readdcld 10069	. . . . . . . . . . 11
59		negpilt0 39492	. . . . . . . . . . . . . 14
60		pipos 24212	. . . . . . . . . . . . . 14
61	54	renegcli 10342	. . . . . . . . . . . . . . 15
62		0re 10040	. . . . . . . . . . . . . . 15
63	61, 62, 54	lttri 10163	. . . . . . . . . . . . . 14 $/\$
64	59, 60, 63	mp2an 708	. . . . . . . . . . . . 13
65	64	a1i 11	. . . . . . . . . . . 12
66	56, 55, 44, 65	ltadd1dd 10638	. . . . . . . . . . 11
67		oveq1 6657	. . . . . . . . . . . . . . 15
68	67	eleq1d 2686	. . . . . . . . . . . . . 14
69	68	rexbidv 3052	. . . . . . . . . . . . 13
70	69	cbvrabv 3199	. . . . . . . . . . . 12
71	70	uneq2i 3764	. . . . . . . . . . 11
72		fourierdlem112.n	. . . . . . . . . . 11
73		fourierdlem112.v	. . . . . . . . . . 11
74	50, 51, 52, 53, 57, 58, 66, 45, 71, 72, 73	fourierdlem54 40377	. . . . . . . . . 10 $/\$ $/\$ $/\$ ..^ $/\$
75	74	simpld 475	. . . . . . . . 9 $/\$ $/\$ $/\$ ..^
76	75	simpld 475	. . . . . . . 8
77	75	simprd 479	. . . . . . . 8 $/\$ $/\$ ..^
78		fourierdlem112.xran	. . . . . . . 8
79	43	adantr 481	. . . . . . . . 9 $/\$ ..^
80		fveq2 6191	. . . . . . . . . . . . . . . 16
81		oveq1 6657	. . . . . . . . . . . . . . . . 17
82	81	fveq2d 6195	. . . . . . . . . . . . . . . 16
83	80, 82	breq12d 4666	. . . . . . . . . . . . . . 15
84	83	cbvralv 3171	. . . . . . . . . . . . . 14 ..^ ..^
85	84	anbi2i 730	. . . . . . . . . . . . 13 $/\$ $/\$ ..^ $/\$ $/\$ ..^
86	85	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ ..^ $/\$ $/\$ ..^
87	86	rabbiia 3185	. . . . . . . . . . 11 $/\$ $/\$ ..^ $/\$ $/\$ ..^
88	87	mpteq2i 4741	. . . . . . . . . 10 $/\$ $/\$ ..^ $/\$ $/\$ ..^
89	51, 88	eqtri 2644	. . . . . . . . 9 $/\$ $/\$ ..^
90	52	adantr 481	. . . . . . . . 9 $/\$ ..^
91	53	adantr 481	. . . . . . . . 9 $/\$ ..^
92		fourierdlem112.fper	. . . . . . . . . 10 $/\$
93	92	adantlr 751	. . . . . . . . 9 $/\$ ..^ $/\$
94		eleq1 2689	. . . . . . . . . . . . 13 ..^ ..^
95	94	anbi2d 740	. . . . . . . . . . . 12 $/\$ ..^ $/\$ ..^
96		fveq2 6191	. . . . . . . . . . . . . . 15
97	81	fveq2d 6195	. . . . . . . . . . . . . . 15
98	96, 97	oveq12d 6668	. . . . . . . . . . . . . 14
99	98	reseq2d 5396	. . . . . . . . . . . . 13
100	98	oveq1d 6665	. . . . . . . . . . . . 13
101	99, 100	eleq12d 2695	. . . . . . . . . . . 12
102	95, 101	imbi12d 334	. . . . . . . . . . 11 $/\$ ..^ $/\$ ..^
103		fourierdlem112.fcn	. . . . . . . . . . 11 $/\$ ..^
104	102, 103	chvarv 2263	. . . . . . . . . 10 $/\$ ..^
105	104	adantlr 751	. . . . . . . . 9 $/\$ ..^ $/\$ ..^
106	57	adantr 481	. . . . . . . . 9 $/\$ ..^
107	57	rexrd 10089	. . . . . . . . . . 11
108		pnfxr 10092	. . . . . . . . . . . 12
109	108	a1i 11	. . . . . . . . . . 11
110	58	ltpnfd 11955	. . . . . . . . . . 11
111	107, 109, 58, 66, 110	eliood 39720	. . . . . . . . . 10
112	111	adantr 481	. . . . . . . . 9 $/\$ ..^
113		id 22	. . . . . . . . . . 11 ..^ ..^
114	72	oveq2i 6661	. . . . . . . . . . 11 ..^ ..^
115	113, 114	syl6eleq 2711	. . . . . . . . . 10 ..^ ..^
116	115	adantl 482	. . . . . . . . 9 $/\$ ..^ ..^
117	72	oveq2i 6661	. . . . . . . . . . . 12
118		isoeq4 6570	. . . . . . . . . . . 12
119	117, 118	ax-mp 5	. . . . . . . . . . 11
120	119	iotabii 5873	. . . . . . . . . 10
121	73, 120	eqtri 2644	. . . . . . . . 9
122	79, 89, 50, 90, 91, 93, 105, 106, 112, 116, 121	fourierdlem98 40421	. . . . . . . 8 $/\$ ..^
123		fourierdlem112.fbd	. . . . . . . . . 10
124	123	adantr 481	. . . . . . . . 9 $/\$ ..^
125		nfra1 2941	. . . . . . . . . . 11
126		elioore 12205	. . . . . . . . . . . . 13
127		rspa 2930	. . . . . . . . . . . . 13 $/\$
128	126, 127	sylan2 491	. . . . . . . . . . . 12 $/\$
129	128	ex 450	. . . . . . . . . . 11
130	125, 129	ralrimi 2957	. . . . . . . . . 10
131	130	reximi 3011	. . . . . . . . 9
132	124, 131	syl 17	. . . . . . . 8 $/\$ ..^
133		ssid 3624	. . . . . . . . . . . 12
134		dvfre 23714	. . . . . . . . . . . 12 $/\$
135	43, 133, 134	sylancl 694	. . . . . . . . . . 11
136	135	adantr 481	. . . . . . . . . 10 $/\$ ..^
137		eqid 2622	. . . . . . . . . . . . 13
138	54	a1i 11	. . . . . . . . . . . . 13 $/\$ ..^
139	61	a1i 11	. . . . . . . . . . . . 13 $/\$ ..^
140	98	reseq2d 5396	. . . . . . . . . . . . . . . . 17
141	140, 100	eleq12d 2695	. . . . . . . . . . . . . . . 16
142	95, 141	imbi12d 334	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ ..^
143		fourierdlem112.fdvcn	. . . . . . . . . . . . . . 15 $/\$ ..^
144	142, 143	chvarv 2263	. . . . . . . . . . . . . 14 $/\$ ..^
145	144	adantlr 751	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^
146		fourierdlem112.x	. . . . . . . . . . . . . . 15
147	56, 146	readdcld 10069	. . . . . . . . . . . . . 14
148	147	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^
149	147	rexrd 10089	. . . . . . . . . . . . . . 15
150	55, 146	readdcld 10069	. . . . . . . . . . . . . . 15
151	56, 55, 146, 65	ltadd1dd 10638	. . . . . . . . . . . . . . 15
152	150	ltpnfd 11955	. . . . . . . . . . . . . . 15
153	149, 109, 150, 151, 152	eliood 39720	. . . . . . . . . . . . . 14
154	153	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^
155		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
156	155	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21
157	156	eleq1d 2686	. . . . . . . . . . . . . . . . . . . 20
158	157	cbvrexv 3172	. . . . . . . . . . . . . . . . . . 19
159	158	rgenw 2924	. . . . . . . . . . . . . . . . . 18
160		rabbi 3120	. . . . . . . . . . . . . . . . . 18
161	159, 160	mpbi 220	. . . . . . . . . . . . . . . . 17
162	161	uneq2i 3764	. . . . . . . . . . . . . . . 16
163		isoeq5 6571	. . . . . . . . . . . . . . . 16
164	162, 163	ax-mp 5	. . . . . . . . . . . . . . 15
165	164	iotabii 5873	. . . . . . . . . . . . . 14
166	121, 165	eqtri 2644	. . . . . . . . . . . . 13
167		eleq1 2689	. . . . . . . . . . . . . . 15
168		fveq2 6191	. . . . . . . . . . . . . . 15
169	167, 168	ifbieq1d 4109	. . . . . . . . . . . . . 14
170	169	cbvmptv 4750	. . . . . . . . . . . . 13
171	79, 137, 89, 138, 139, 50, 90, 91, 93, 145, 148, 154, 116, 166, 170	fourierdlem97 40420	. . . . . . . . . . . 12 $/\$ ..^
172		cncff 22696	. . . . . . . . . . . 12
173		fdm 6051	. . . . . . . . . . . 12
174	171, 172, 173	3syl 18	. . . . . . . . . . 11 $/\$ ..^
175		ssdmres 5420	. . . . . . . . . . 11
176	174, 175	sylibr 224	. . . . . . . . . 10 $/\$ ..^
177	136, 176	fssresd 6071	. . . . . . . . 9 $/\$ ..^
178		ax-resscn 9993	. . . . . . . . . . 11
179	178	a1i 11	. . . . . . . . . 10 $/\$ ..^
180		cncffvrn 22701	. . . . . . . . . 10 $/\$
181	179, 171, 180	syl2anc 693	. . . . . . . . 9 $/\$ ..^
182	177, 181	mpbird 247	. . . . . . . 8 $/\$ ..^
183		fourierdlem112.fdvbd	. . . . . . . . . . 11
184	183	adantr 481	. . . . . . . . . 10 $/\$ ..^
185		nfv 1843	. . . . . . . . . . . . . 14 $/\$ ..^
186		nfra1 2941	. . . . . . . . . . . . . 14
187	185, 186	nfan 1828	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
188		fvres 6207	. . . . . . . . . . . . . . . . . 18
189	188	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
190	189	fveq2d 6195	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
191	190	adantlr 751	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
192		simplr 792	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
193	176	sselda 3603	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
194	193	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
195		rspa 2930	. . . . . . . . . . . . . . . 16 $/\$
196	192, 194, 195	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
197	191, 196	eqbrtrd 4675	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
198	197	ex 450	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
199	187, 198	ralrimi 2957	. . . . . . . . . . . 12 $/\$ ..^ $/\$
200	199	ex 450	. . . . . . . . . . 11 $/\$ ..^
201	200	reximdv 3016	. . . . . . . . . 10 $/\$ ..^
202	184, 201	mpd 15	. . . . . . . . 9 $/\$ ..^
203		nfra1 2941	. . . . . . . . . . . 12
204	188	eqcomd 2628	. . . . . . . . . . . . . . . 16
205	204	fveq2d 6195	. . . . . . . . . . . . . . 15
206	205	adantl 482	. . . . . . . . . . . . . 14 $/\$
207		rspa 2930	. . . . . . . . . . . . . 14 $/\$
208	206, 207	eqbrtrd 4675	. . . . . . . . . . . . 13 $/\$
209	208	ex 450	. . . . . . . . . . . 12
210	203, 209	ralrimi 2957	. . . . . . . . . . 11
211	210	a1i 11	. . . . . . . . . 10 $/\$ ..^
212	211	reximdv 3016	. . . . . . . . 9 $/\$ ..^
213	202, 212	mpd 15	. . . . . . . 8 $/\$ ..^
214		nfv 1843	. . . . . . . . . . . 12 $/\$ ..^
215		nfcsb1v 3549	. . . . . . . . . . . . 13
216	215	nfel1 2779	. . . . . . . . . . . 12 lim
217	214, 216	nfim 1825	. . . . . . . . . . 11 $/\$ ..^ lim
218		csbeq1a 3542	. . . . . . . . . . . . 13
219	99, 96	oveq12d 6668	. . . . . . . . . . . . 13 lim lim
220	218, 219	eleq12d 2695	. . . . . . . . . . . 12 lim lim
221	95, 220	imbi12d 334	. . . . . . . . . . 11 $/\$ ..^ lim $/\$ ..^ lim
222		fourierdlem112.c	. . . . . . . . . . 11 $/\$ ..^ lim
223	217, 221, 222	chvar 2262	. . . . . . . . . 10 $/\$ ..^ lim
224	223	adantlr 751	. . . . . . . . 9 $/\$ ..^ $/\$ ..^ lim
225	79, 89, 50, 90, 91, 93, 105, 224, 106, 112, 116, 121	fourierdlem96 40419	. . . . . . . 8 $/\$ ..^ ..^ ..^ ..^ lim
226		nfcsb1v 3549	. . . . . . . . . . . . 13
227	226	nfel1 2779	. . . . . . . . . . . 12 lim
228	214, 227	nfim 1825	. . . . . . . . . . 11 $/\$ ..^ lim
229		csbeq1a 3542	. . . . . . . . . . . . 13
230	99, 97	oveq12d 6668	. . . . . . . . . . . . 13 lim lim
231	229, 230	eleq12d 2695	. . . . . . . . . . . 12 lim lim
232	95, 231	imbi12d 334	. . . . . . . . . . 11 $/\$ ..^ lim $/\$ ..^ lim
233		fourierdlem112.u	. . . . . . . . . . 11 $/\$ ..^ lim
234	228, 232, 233	chvar 2262	. . . . . . . . . 10 $/\$ ..^ lim
235	234	adantlr 751	. . . . . . . . 9 $/\$ ..^ $/\$ ..^ lim
236	79, 89, 50, 90, 91, 93, 105, 235, 148, 154, 116, 121	fourierdlem99 40422	. . . . . . . 8 $/\$ ..^ ..^ ..^ ..^ lim
237		eqeq1 2626	. . . . . . . . . 10
238		oveq2 6658	. . . . . . . . . . . . 13
239	238	fveq2d 6195	. . . . . . . . . . . 12
240		breq2 4657	. . . . . . . . . . . . 13
241	240	ifbid 4108	. . . . . . . . . . . 12
242	239, 241	oveq12d 6668	. . . . . . . . . . 11
243		id 22	. . . . . . . . . . 11
244	242, 243	oveq12d 6668	. . . . . . . . . 10
245	237, 244	ifbieq2d 4111	. . . . . . . . 9
246	245	cbvmptv 4750	. . . . . . . 8
247		eqeq1 2626	. . . . . . . . . 10
248		id 22	. . . . . . . . . . 11
249		oveq1 6657	. . . . . . . . . . . . 13
250	249	fveq2d 6195	. . . . . . . . . . . 12
251	250	oveq2d 6666	. . . . . . . . . . 11
252	248, 251	oveq12d 6668	. . . . . . . . . 10
253	247, 252	ifbieq2d 4111	. . . . . . . . 9
254	253	cbvmptv 4750	. . . . . . . 8
255		fveq2 6191	. . . . . . . . . 10
256		fveq2 6191	. . . . . . . . . 10
257	255, 256	oveq12d 6668	. . . . . . . . 9
258	257	cbvmptv 4750	. . . . . . . 8
259		oveq2 6658	. . . . . . . . . 10
260	259	fveq2d 6195	. . . . . . . . 9
261	260	cbvmptv 4750	. . . . . . . 8
262		fveq2 6191	. . . . . . . . . 10
263		fveq2 6191	. . . . . . . . . 10
264	262, 263	oveq12d 6668	. . . . . . . . 9
265	264	cbvmptv 4750	. . . . . . . 8
266		fveq2 6191	. . . . . . . . . . . . 13
267	266	fveq1d 6193	. . . . . . . . . . . 12
268	267	oveq2d 6666	. . . . . . . . . . 11
269	268	adantr 481	. . . . . . . . . 10 $/\$
270	269	itgeq2dv 23548	. . . . . . . . 9
271	270	cbvmptv 4750	. . . . . . . 8
272		oveq1 6657	. . . . . . . . . . . . . . . . . . 19
273	272	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
274	273	fveq2d 6195	. . . . . . . . . . . . . . . . 17
275	274	mpteq2dv 4745	. . . . . . . . . . . . . . . 16
276	275	fveq1d 6193	. . . . . . . . . . . . . . 15
277	276	oveq2d 6666	. . . . . . . . . . . . . 14
278	277	mpteq2dv 4745	. . . . . . . . . . . . 13
279	278	fveq1d 6193	. . . . . . . . . . . 12
280	279	adantr 481	. . . . . . . . . . 11 $/\$
281	280	itgeq2dv 23548	. . . . . . . . . 10
282	281	oveq1d 6665	. . . . . . . . 9
283	282	cbvmptv 4750	. . . . . . . 8
284		fourierdlem112.r	. . . . . . . 8 lim
285		fourierdlem112.l	. . . . . . . 8 lim
286		fourierdlem112.e	. . . . . . . 8 lim
287		fourierdlem112.i	. . . . . . . 8 lim
288		fourierdlem112.d	. . . . . . . . 9
289		oveq1 6657	. . . . . . . . . . . . . 14
290	289	eqeq1d 2624	. . . . . . . . . . . . 13
291		oveq2 6658	. . . . . . . . . . . . . . 15
292	291	fveq2d 6195	. . . . . . . . . . . . . 14
293		oveq1 6657	. . . . . . . . . . . . . . . 16
294	293	fveq2d 6195	. . . . . . . . . . . . . . 15
295	294	oveq2d 6666	. . . . . . . . . . . . . 14
296	292, 295	oveq12d 6668	. . . . . . . . . . . . 13
297	290, 296	ifbieq2d 4111	. . . . . . . . . . . 12
298	297	cbvmptv 4750	. . . . . . . . . . 11
299		simpl 473	. . . . . . . . . . . . . . . 16 $/\$
300	299	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$
301	300	oveq1d 6665	. . . . . . . . . . . . . 14 $/\$
302	301	oveq1d 6665	. . . . . . . . . . . . 13 $/\$
303	299	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$
304	303	oveq1d 6665	. . . . . . . . . . . . . . 15 $/\$
305	304	fveq2d 6195	. . . . . . . . . . . . . 14 $/\$
306	305	oveq1d 6665	. . . . . . . . . . . . 13 $/\$
307	302, 306	ifeq12d 4106	. . . . . . . . . . . 12 $/\$
308	307	mpteq2dva 4744	. . . . . . . . . . 11
309	298, 308	syl5eq 2668	. . . . . . . . . 10
310	309	cbvmptv 4750	. . . . . . . . 9
311	288, 310	eqtri 2644	. . . . . . . 8
312		eqid 2622	. . . . . . . 8
313		eqid 2622	. . . . . . . 8
314		eqid 2622	. . . . . . . 8
315		isoeq1 6567	. . . . . . . . 9
316	315	cbviotav 5857	. . . . . . . 8
317		fveq2 6191	. . . . . . . . . 10
318	317	oveq1d 6665	. . . . . . . . 9
319	318	cbvmptv 4750	. . . . . . . 8
320		eqid 2622	. . . . . . . 8 ..^ ..^
321		fveq2 6191	. . . . . . . . . . . . . 14
322		oveq2 6658	. . . . . . . . . . . . . . 15
323	322	fveq2d 6195	. . . . . . . . . . . . . 14
324	321, 323	oveq12d 6668	. . . . . . . . . . . . 13
325	324	cbvitgv 23543	. . . . . . . . . . . 12
326	325	fveq2i 6194	. . . . . . . . . . 11
327	326	breq1i 4660	. . . . . . . . . 10
328	327	anbi2i 730	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
329	324	cbvitgv 23543	. . . . . . . . . . 11
330	329	fveq2i 6194	. . . . . . . . . 10
331	330	breq1i 4660	. . . . . . . . 9
332	328, 331	anbi12i 733	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
333	43, 44, 45, 76, 77, 78, 122, 132, 182, 213, 225, 236, 246, 254, 258, 261, 265, 271, 283, 284, 285, 286, 287, 311, 312, 313, 314, 316, 319, 320, 332	fourierdlem103 40426	. . . . . . 7
334		nnex 11026	. . . . . . . . . 10
335	334	mptex 6486	. . . . . . . . 9
336	28, 335	eqeltri 2697	. . . . . . . 8
337	336	a1i 11	. . . . . . 7
338	268	adantr 481	. . . . . . . . . 10 $/\$
339	338	itgeq2dv 23548	. . . . . . . . 9
340	339	cbvmptv 4750	. . . . . . . 8
341	279	adantr 481	. . . . . . . . . . 11 $/\$
342	341	itgeq2dv 23548	. . . . . . . . . 10
343	342	oveq1d 6665	. . . . . . . . 9
344	343	cbvmptv 4750	. . . . . . . 8
345		eqid 2622	. . . . . . . 8
346		eqid 2622	. . . . . . . 8
347		eqid 2622	. . . . . . . 8
348		isoeq1 6567	. . . . . . . . 9
349	348	cbviotav 5857	. . . . . . . 8
350		eqid 2622	. . . . . . . 8 ..^ ..^
351	324	cbvitgv 23543	. . . . . . . . . . . 12
352	351	fveq2i 6194	. . . . . . . . . . 11
353	352	breq1i 4660	. . . . . . . . . 10
354	353	anbi2i 730	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
355	324	cbvitgv 23543	. . . . . . . . . . 11
356	355	fveq2i 6194	. . . . . . . . . 10
357	356	breq1i 4660	. . . . . . . . 9
358	354, 357	anbi12i 733	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
359	43, 44, 45, 76, 77, 78, 122, 132, 182, 213, 225, 236, 246, 254, 258, 261, 265, 340, 344, 284, 285, 286, 287, 311, 345, 346, 347, 349, 319, 350, 358	fourierdlem104 40427	. . . . . . 7
360		eqidd 2623	. . . . . . . . 9 $/\$
361	270	adantl 482	. . . . . . . . 9 $/\$ $/\$
362		simpr 477	. . . . . . . . 9 $/\$
363		elioore 12205	. . . . . . . . . . 11
364	43	adantr 481	. . . . . . . . . . . . . 14 $/\$
365	44	adantr 481	. . . . . . . . . . . . . . 15 $/\$
366		simpr 477	. . . . . . . . . . . . . . 15 $/\$
367	365, 366	readdcld 10069	. . . . . . . . . . . . . 14 $/\$
368	364, 367	ffvelrnd 6360	. . . . . . . . . . . . 13 $/\$
369	368	adantlr 751	. . . . . . . . . . . 12 $/\$ $/\$
370	288	dirkerre 40312	. . . . . . . . . . . . 13 $/\$
371	370	adantll 750	. . . . . . . . . . . 12 $/\$ $/\$
372	369, 371	remulcld 10070	. . . . . . . . . . 11 $/\$ $/\$
373	363, 372	sylan2 491	. . . . . . . . . 10 $/\$ $/\$
374		ioossicc 12259	. . . . . . . . . . . . 13
375	61	leidi 10562	. . . . . . . . . . . . . 14
376	62, 54, 60	ltleii 10160	. . . . . . . . . . . . . 14
377		iccss 12241	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
378	61, 54, 375, 376, 377	mp4an 709	. . . . . . . . . . . . 13
379	374, 378	sstri 3612	. . . . . . . . . . . 12
380	379	a1i 11	. . . . . . . . . . 11 $/\$
381		ioombl 23333	. . . . . . . . . . . 12
382	381	a1i 11	. . . . . . . . . . 11 $/\$
383	43	adantr 481	. . . . . . . . . . . . . 14 $/\$
384	44	adantr 481	. . . . . . . . . . . . . . 15 $/\$
385	56, 55	iccssred 39727	. . . . . . . . . . . . . . . 16
386	385	sselda 3603	. . . . . . . . . . . . . . 15 $/\$
387	384, 386	readdcld 10069	. . . . . . . . . . . . . 14 $/\$
388	383, 387	ffvelrnd 6360	. . . . . . . . . . . . 13 $/\$
389	388	adantlr 751	. . . . . . . . . . . 12 $/\$ $/\$
390		iccssre 12255	. . . . . . . . . . . . . . . 16 $/\$
391	61, 54, 390	mp2an 708	. . . . . . . . . . . . . . 15
392	391	sseli 3599	. . . . . . . . . . . . . 14
393	392, 370	sylan2 491	. . . . . . . . . . . . 13 $/\$
394	393	adantll 750	. . . . . . . . . . . 12 $/\$ $/\$
395	389, 394	remulcld 10070	. . . . . . . . . . 11 $/\$ $/\$
396	61	a1i 11	. . . . . . . . . . . 12 $/\$
397	54	a1i 11	. . . . . . . . . . . 12 $/\$
398	43	adantr 481	. . . . . . . . . . . 12 $/\$
399	44	adantr 481	. . . . . . . . . . . 12 $/\$
400	76	adantr 481	. . . . . . . . . . . 12 $/\$
401	77	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ ..^
402	122	adantlr 751	. . . . . . . . . . . 12 $/\$ $/\$ ..^
403	225	adantlr 751	. . . . . . . . . . . 12 $/\$ $/\$ ..^ ..^ ..^ ..^ lim
404	236	adantlr 751	. . . . . . . . . . . 12 $/\$ $/\$ ..^ ..^ ..^ ..^ lim
405	288	dirkercncf 40324	. . . . . . . . . . . . 13
406	405	adantl 482	. . . . . . . . . . . 12 $/\$
407		eqid 2622	. . . . . . . . . . . 12
408	396, 397, 398, 399, 45, 400, 401, 402, 403, 404, 319, 51, 406, 407	fourierdlem84 40407	. . . . . . . . . . 11 $/\$
409	380, 382, 395, 408	iblss 23571	. . . . . . . . . 10 $/\$
410	373, 409	itgcl 23550	. . . . . . . . 9 $/\$
411	360, 361, 362, 410	fvmptd 6288	. . . . . . . 8 $/\$
412	411, 410	eqeltrd 2701	. . . . . . 7 $/\$
413		eqidd 2623	. . . . . . . . 9 $/\$
414	339	adantl 482	. . . . . . . . 9 $/\$ $/\$
415	43	adantr 481	. . . . . . . . . . . . 13 $/\$
416	44	adantr 481	. . . . . . . . . . . . . 14 $/\$
417		elioore 12205	. . . . . . . . . . . . . . 15
418	417	adantl 482	. . . . . . . . . . . . . 14 $/\$
419	416, 418	readdcld 10069	. . . . . . . . . . . . 13 $/\$
420	415, 419	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$
421	420	adantlr 751	. . . . . . . . . . 11 $/\$ $/\$
422	417, 370	sylan2 491	. . . . . . . . . . . 12 $/\$
423	422	adantll 750	. . . . . . . . . . 11 $/\$ $/\$
424	421, 423	remulcld 10070	. . . . . . . . . 10 $/\$ $/\$
425		ioossicc 12259	. . . . . . . . . . . . 13
426	61, 62, 59	ltleii 10160	. . . . . . . . . . . . . 14
427	54	leidi 10562	. . . . . . . . . . . . . 14
428		iccss 12241	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
429	61, 54, 426, 427, 428	mp4an 709	. . . . . . . . . . . . 13
430	425, 429	sstri 3612	. . . . . . . . . . . 12
431	430	a1i 11	. . . . . . . . . . 11 $/\$
432		ioombl 23333	. . . . . . . . . . . 12
433	432	a1i 11	. . . . . . . . . . 11 $/\$
434	431, 433, 395, 408	iblss 23571	. . . . . . . . . 10 $/\$
435	424, 434	itgcl 23550	. . . . . . . . 9 $/\$
436	413, 414, 362, 435	fvmptd 6288	. . . . . . . 8 $/\$
437	436, 435	eqeltrd 2701	. . . . . . 7 $/\$
438		eleq1 2689	. . . . . . . . . . 11
439	438	anbi2d 740	. . . . . . . . . 10 $/\$ $/\$
440		fveq2 6191	. . . . . . . . . . 11
441	270, 339	oveq12d 6668	. . . . . . . . . . 11
442	440, 441	eqeq12d 2637	. . . . . . . . . 10
443	439, 442	imbi12d 334	. . . . . . . . 9 $/\$ $/\$
444		oveq1 6657	. . . . . . . . . . . . . . . . 17
445	444	fveq2d 6195	. . . . . . . . . . . . . . . 16
446	445	oveq2d 6666	. . . . . . . . . . . . . . 15
447	446	adantr 481	. . . . . . . . . . . . . 14 $/\$
448	447	itgeq2dv 23548	. . . . . . . . . . . . 13
449	448	oveq1d 6665	. . . . . . . . . . . 12
450	449	cbvmptv 4750	. . . . . . . . . . 11
451	29, 450	eqtri 2644	. . . . . . . . . 10
452		fourierdlem112.b	. . . . . . . . . . 11
453	444	fveq2d 6195	. . . . . . . . . . . . . . . 16
454	453	oveq2d 6666	. . . . . . . . . . . . . . 15
455	454	adantr 481	. . . . . . . . . . . . . 14 $/\$
456	455	itgeq2dv 23548	. . . . . . . . . . . . 13
457	456	oveq1d 6665	. . . . . . . . . . . 12
458	457	cbvmptv 4750	. . . . . . . . . . 11
459	452, 458	eqtri 2644	. . . . . . . . . 10
460		fveq2 6191	. . . . . . . . . . . . . . . 16
461		oveq1 6657	. . . . . . . . . . . . . . . . 17
462	461	fveq2d 6195	. . . . . . . . . . . . . . . 16
463	460, 462	oveq12d 6668	. . . . . . . . . . . . . . 15
464		fveq2 6191	. . . . . . . . . . . . . . . 16
465	461	fveq2d 6195	. . . . . . . . . . . . . . . 16
466	464, 465	oveq12d 6668	. . . . . . . . . . . . . . 15
467	463, 466	oveq12d 6668	. . . . . . . . . . . . . 14
468	467	cbvsumv 14426	. . . . . . . . . . . . 13
469	468	oveq2i 6661	. . . . . . . . . . . 12
470	469	mpteq2i 4741	. . . . . . . . . . 11
471		oveq2 6658	. . . . . . . . . . . . . . 15
472	471	sumeq1d 14431	. . . . . . . . . . . . . 14
473	472	oveq2d 6666	. . . . . . . . . . . . 13
474	473	cbvmptv 4750	. . . . . . . . . . . 12
475		fveq2 6191	. . . . . . . . . . . . . . . . 17
476		oveq1 6657	. . . . . . . . . . . . . . . . . 18
477	476	fveq2d 6195	. . . . . . . . . . . . . . . . 17
478	475, 477	oveq12d 6668	. . . . . . . . . . . . . . . 16
479		fveq2 6191	. . . . . . . . . . . . . . . . 17
480	476	fveq2d 6195	. . . . . . . . . . . . . . . . 17
481	479, 480	oveq12d 6668	. . . . . . . . . . . . . . . 16
482	478, 481	oveq12d 6668	. . . . . . . . . . . . . . 15
483	482	cbvsumv 14426	. . . . . . . . . . . . . 14
484	483	oveq2i 6661	. . . . . . . . . . . . 13
485	484	mpteq2i 4741	. . . . . . . . . . . 12
486	474, 485	eqtri 2644	. . . . . . . . . . 11
487	28, 470, 486	3eqtri 2648	. . . . . . . . . 10
488		oveq2 6658	. . . . . . . . . . . . 13
489	488	fveq2d 6195	. . . . . . . . . . . 12
490		fveq2 6191	. . . . . . . . . . . 12
491	489, 490	oveq12d 6668	. . . . . . . . . . 11
492	491	cbvmptv 4750	. . . . . . . . . 10
493		eqid 2622	. . . . . . . . . 10 $/\$ $/\$ ..^ $/\$ $/\$ ..^
494		fveq2 6191	. . . . . . . . . . . 12
495	494	oveq1d 6665	. . . . . . . . . . 11
496	495	cbvmptv 4750	. . . . . . . . . 10
497	451, 459, 487, 288, 51, 52, 53, 146, 43, 92, 492, 103, 222, 233, 48, 493, 496	fourierdlem111 40434	. . . . . . . . 9 $/\$
498	443, 497	chvarv 2263	. . . . . . . 8 $/\$
499	411, 436	oveq12d 6668	. . . . . . . 8 $/\$
500	498, 499	eqtr4d 2659	. . . . . . 7 $/\$
501	16, 24, 27, 42, 14, 15, 333, 337, 359, 412, 437, 500	climaddf 39847	. . . . . 6
502		limccl 23639	. . . . . . . 8 lim
503	502, 285	sseldi 3601	. . . . . . 7
504		limccl 23639	. . . . . . . 8 lim
505	504, 284	sseldi 3601	. . . . . . 7
506		2cnd 11093	. . . . . . 7
507		2pos 11112	. . . . . . . . 9
508	507	a1i 11	. . . . . . . 8
509	508	gt0ne0d 10592	. . . . . . 7
510	503, 505, 506, 509	divdird 10839	. . . . . 6
511	501, 510	breqtrrd 4681	. . . . 5
512		0nn0 11307	. . . . . . . 8
513	43	adantr 481	. . . . . . . . . 10 $/\$
514		eqid 2622	. . . . . . . . . 10
515		ioossre 12235	. . . . . . . . . . . . . 14
516	515	a1i 11	. . . . . . . . . . . . 13
517	43, 516	feqresmpt 6250	. . . . . . . . . . . 12
518		ioossicc 12259	. . . . . . . . . . . . . 14
519	518	a1i 11	. . . . . . . . . . . . 13
520		ioombl 23333	. . . . . . . . . . . . . 14
521	520	a1i 11	. . . . . . . . . . . . 13
522	43	adantr 481	. . . . . . . . . . . . . 14 $/\$
523	385	sselda 3603	. . . . . . . . . . . . . 14 $/\$
524	522, 523	ffvelrnd 6360	. . . . . . . . . . . . 13 $/\$
525	43, 385	feqresmpt 6250	. . . . . . . . . . . . . 14
526	178	a1i 11	. . . . . . . . . . . . . . . . 17
527	43, 526	fssd 6057	. . . . . . . . . . . . . . . 16
528	527, 385	fssresd 6071	. . . . . . . . . . . . . . 15
529		ioossicc 12259	. . . . . . . . . . . . . . . . . 18
530	61	rexri 10097	. . . . . . . . . . . . . . . . . . . 20
531	530	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
532	54	rexri 10097	. . . . . . . . . . . . . . . . . . . 20
533	532	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
534	51, 52, 53	fourierdlem15 40339	. . . . . . . . . . . . . . . . . . . 20
535	534	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
536		simpr 477	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ ..^
537	531, 533, 535, 536	fourierdlem8 40332	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
538	529, 537	syl5ss 3614	. . . . . . . . . . . . . . . . 17 $/\$ ..^
539	538	resabs1d 5428	. . . . . . . . . . . . . . . 16 $/\$ ..^
540	539, 103	eqeltrd 2701	. . . . . . . . . . . . . . 15 $/\$ ..^
541	539	eqcomd 2628	. . . . . . . . . . . . . . . . 17 $/\$ ..^
542	541	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ ..^ lim lim
543	222, 542	eleqtrd 2703	. . . . . . . . . . . . . . 15 $/\$ ..^ lim
544	541	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ ..^ lim lim
545	233, 544	eleqtrd 2703	. . . . . . . . . . . . . . 15 $/\$ ..^ lim
546	51, 52, 53, 528, 540, 543, 545	fourierdlem69 40392	. . . . . . . . . . . . . 14
547	525, 546	eqeltrrd 2702	. . . . . . . . . . . . 13
548	519, 521, 524, 547	iblss 23571	. . . . . . . . . . . 12
549	517, 548	eqeltrd 2701	. . . . . . . . . . 11
550	549	adantr 481	. . . . . . . . . 10 $/\$
551		simpr 477	. . . . . . . . . 10 $/\$
552	513, 514, 550, 29, 551	fourierdlem16 40340	. . . . . . . . 9 $/\$ $/\$ $/\$
553	552	simplld 791	. . . . . . . 8 $/\$
554	512, 553	mpan2 707	. . . . . . 7
555	554	rehalfcld 11279	. . . . . 6
556	555	recnd 10068	. . . . 5
557	334	mptex 6486	. . . . . 6
558	557	a1i 11	. . . . 5
559		simpr 477	. . . . . . . 8 $/\$
560	555	adantr 481	. . . . . . . . 9 $/\$
561		fzfid 12772	. . . . . . . . . 10 $/\$
562		simpll 790	. . . . . . . . . . 11 $/\$ $/\$
563		elfznn 12370	. . . . . . . . . . . 12
564	563	adantl 482	. . . . . . . . . . 11 $/\$ $/\$
565		simpl 473	. . . . . . . . . . . . . 14 $/\$
566	362	nnnn0d 11351	. . . . . . . . . . . . . 14 $/\$
567		eleq1 2689	. . . . . . . . . . . . . . . . 17
568	567	anbi2d 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$
569		fveq2 6191	. . . . . . . . . . . . . . . . 17
570	569	eleq1d 2686	. . . . . . . . . . . . . . . 16
571	568, 570	imbi12d 334	. . . . . . . . . . . . . . 15 $/\$ $/\$
572	43	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
573	549	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
574		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$
575	572, 514, 573, 29, 574	fourierdlem16 40340	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
576	575	simplld 791	. . . . . . . . . . . . . . 15 $/\$
577	571, 576	chvarv 2263	. . . . . . . . . . . . . 14 $/\$
578	565, 566, 577	syl2anc 693	. . . . . . . . . . . . 13 $/\$
579	362	nnred 11035	. . . . . . . . . . . . . . 15 $/\$
580	579, 399	remulcld 10070	. . . . . . . . . . . . . 14 $/\$
581	580	recoscld 14874	. . . . . . . . . . . . 13 $/\$
582	578, 581	remulcld 10070	. . . . . . . . . . . 12 $/\$
583		eleq1 2689	. . . . . . . . . . . . . . . 16
584	583	anbi2d 740	. . . . . . . . . . . . . . 15 $/\$ $/\$
585		fveq2 6191	. . . . . . . . . . . . . . . 16
586	585	eleq1d 2686	. . . . . . . . . . . . . . 15
587	584, 586	imbi12d 334	. . . . . . . . . . . . . 14 $/\$ $/\$
588	43	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
589	549	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
590		simpr 477	. . . . . . . . . . . . . . . 16 $/\$
591	588, 514, 589, 452, 590	fourierdlem21 40345	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
592	591	simplld 791	. . . . . . . . . . . . . 14 $/\$
593	587, 592	chvarv 2263	. . . . . . . . . . . . 13 $/\$
594	580	resincld 14873	. . . . . . . . . . . . 13 $/\$
595	593, 594	remulcld 10070	. . . . . . . . . . . 12 $/\$
596	582, 595	readdcld 10069	. . . . . . . . . . 11 $/\$
597	562, 564, 596	syl2anc 693	. . . . . . . . . 10 $/\$ $/\$
598	561, 597	fsumrecl 14465	. . . . . . . . 9 $/\$
599	560, 598	readdcld 10069	. . . . . . . 8 $/\$
600	28	fvmpt2 6291	. . . . . . . 8 $/\$
601	559, 599, 600	syl2anc 693	. . . . . . 7 $/\$
602	601, 599	eqeltrd 2701	. . . . . 6 $/\$
603	602	recnd 10068	. . . . 5 $/\$
604		eqidd 2623	. . . . . . 7 $/\$
605		oveq2 6658	. . . . . . . . 9
606	605	sumeq1d 14431	. . . . . . . 8
607	606	adantl 482	. . . . . . 7 $/\$ $/\$
608		sumex 14418	. . . . . . . 8
609	608	a1i 11	. . . . . . 7 $/\$
610	604, 607, 559, 609	fvmptd 6288	. . . . . 6 $/\$
611	560	recnd 10068	. . . . . . . 8 $/\$
612	598	recnd 10068	. . . . . . . 8 $/\$
613	611, 612	pncan2d 10394	. . . . . . 7 $/\$
614	613, 468	syl6req 2673	. . . . . 6 $/\$
615		ovex 6678	. . . . . . . . 9
616	28	fvmpt2 6291	. . . . . . . . 9 $/\$
617	559, 615, 616	sylancl 694	. . . . . . . 8 $/\$
618	617	eqcomd 2628	. . . . . . 7 $/\$
619	618	oveq1d 6665	. . . . . 6 $/\$
620	610, 614, 619	3eqtrd 2660	. . . . 5 $/\$
621	14, 15, 511, 556, 558, 603, 620	climsubc1 14368	. . . 4
622		seqex 12803	. . . . . 6
623	622	a1i 11	. . . . 5
624		eqidd 2623	. . . . . . 7 $/\$
625		oveq2 6658	. . . . . . . . 9
626	625	sumeq1d 14431	. . . . . . . 8
627	626	adantl 482	. . . . . . 7 $/\$ $/\$
628		simpr 477	. . . . . . 7 $/\$
629		fzfid 12772	. . . . . . . 8 $/\$
630		elfznn 12370	. . . . . . . . . . . . 13
631	630	nnnn0d 11351	. . . . . . . . . . . 12
632	631, 576	sylan2 491	. . . . . . . . . . 11 $/\$
633	630	nnred 11035	. . . . . . . . . . . . . 14
634	633	adantl 482	. . . . . . . . . . . . 13 $/\$
635	146	adantr 481	. . . . . . . . . . . . 13 $/\$
636	634, 635	remulcld 10070	. . . . . . . . . . . 12 $/\$
637	636	recoscld 14874	. . . . . . . . . . 11 $/\$
638	632, 637	remulcld 10070	. . . . . . . . . 10 $/\$
639	630, 592	sylan2 491	. . . . . . . . . . 11 $/\$
640	636	resincld 14873	. . . . . . . . . . 11 $/\$
641	639, 640	remulcld 10070	. . . . . . . . . 10 $/\$
642	638, 641	readdcld 10069	. . . . . . . . 9 $/\$
643	642	adantlr 751	. . . . . . . 8 $/\$ $/\$
644	629, 643	fsumrecl 14465	. . . . . . 7 $/\$
645	624, 627, 628, 644	fvmptd 6288	. . . . . 6 $/\$
646		eleq1 2689	. . . . . . . . 9
647	646	anbi2d 740	. . . . . . . 8 $/\$ $/\$
648		fveq2 6191	. . . . . . . . 9
649	626, 648	eqeq12d 2637	. . . . . . . 8
650	647, 649	imbi12d 334	. . . . . . 7 $/\$ $/\$
651		eqidd 2623	. . . . . . . . 9 $/\$ $/\$
652		fveq2 6191	. . . . . . . . . . . 12
653		oveq1 6657	. . . . . . . . . . . . 13
654	653	fveq2d 6195	. . . . . . . . . . . 12
655	652, 654	oveq12d 6668	. . . . . . . . . . 11
656		fveq2 6191	. . . . . . . . . . . 12
657	653	fveq2d 6195	. . . . . . . . . . . 12
658	656, 657	oveq12d 6668	. . . . . . . . . . 11
659	655, 658	oveq12d 6668	. . . . . . . . . 10
660	659	adantl 482	. . . . . . . . 9 $/\$ $/\$ $/\$
661		elfznn 12370	. . . . . . . . . 10
662	661	adantl 482	. . . . . . . . 9 $/\$ $/\$
663		simpll 790	. . . . . . . . . 10 $/\$ $/\$
664		nnnn0 11299	. . . . . . . . . . . 12
665		nn0re 11301	. . . . . . . . . . . . . . . 16
666	665	adantl 482	. . . . . . . . . . . . . . 15 $/\$
667	146	adantr 481	. . . . . . . . . . . . . . 15 $/\$
668	666, 667	remulcld 10070	. . . . . . . . . . . . . 14 $/\$
669	668	recoscld 14874	. . . . . . . . . . . . 13 $/\$
670	576, 669	remulcld 10070	. . . . . . . . . . . 12 $/\$
671	664, 670	sylan2 491	. . . . . . . . . . 11 $/\$
672	664, 668	sylan2 491	. . . . . . . . . . . . 13 $/\$
673	672	resincld 14873	. . . . . . . . . . . 12 $/\$
674	592, 673	remulcld 10070	. . . . . . . . . . 11 $/\$
675	671, 674	readdcld 10069	. . . . . . . . . 10 $/\$
676	663, 662, 675	syl2anc 693	. . . . . . . . 9 $/\$ $/\$
677	651, 660, 662, 676	fvmptd 6288	. . . . . . . 8 $/\$ $/\$
678	362, 14	syl6eleq 2711	. . . . . . . 8 $/\$
679	676	recnd 10068	. . . . . . . 8 $/\$ $/\$
680	677, 678, 679	fsumser 14461	. . . . . . 7 $/\$
681	650, 680	chvarv 2263	. . . . . 6 $/\$
682	645, 681	eqtrd 2656	. . . . 5 $/\$
683	14, 558, 623, 15, 682	climeq 14298	. . . 4
684	621, 683	mpbid 222	. . 3
685	13, 684	eqbrtrd 4675	. 2
686		eqidd 2623	. . . . . 6 $/\$
687		fveq2 6191	. . . . . . . . 9
688		oveq1 6657	. . . . . . . . . 10
689	688	fveq2d 6195	. . . . . . . . 9
690	687, 689	oveq12d 6668	. . . . . . . 8
691		fveq2 6191	. . . . . . . . 9
692	688	fveq2d 6195	. . . . . . . . 9
693	691, 692	oveq12d 6668	. . . . . . . 8
694	690, 693	oveq12d 6668	. . . . . . 7
695	694	adantl 482	. . . . . 6 $/\$ $/\$
696	686, 695, 362, 596	fvmptd 6288	. . . . 5 $/\$
697	596	recnd 10068	. . . . 5 $/\$
698	14, 15, 696, 697, 684	isumclim 14488	. . . 4
699	698	oveq2d 6666	. . 3
700	503, 505	addcld 10059	. . . . 5
701	700	halfcld 11277	. . . 4
702	556, 701	pncan3d 10395	. . 3
703	699, 702	eqtrd 2656	. 2
704	685, 703	jca 554	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $/\$ wa 384

wceq 1483

wcel 1990

wral 2912

wrex 2913

crab 2916

cvv 3200

csb 3533

cun 3572

cin 3573

wss 3574

cif 4086

cpr 4179 class class class wbr 4653

cmpt 4729

cdm 5114

crn 5115

cres 5116

cio 5849

wf 5884

cfv 5888

wiso 5889

crio 6610 (class class class)co 6650

cmap 7857

csup 8346

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cpnf 10071

cmnf 10072

cxr 10073

clt 10074

cle 10075

cmin 10266

cneg 10267

cdiv 10684

cn 11020

c2 11070

cn0 11292

cz 11377

cuz 11687

crp 11832

cioo 12175

cioc 12176

cicc 12178

cfz 12326 ..^cfzo 12465

cfl 12591

cmo 12668

cseq 12801

chash 13117

cabs 13974

cli 14215

csu 14416

csin 14794

ccos 14795

cpi 14797

ccncf 22679

cvol 23232

cibl 23386

citg 23387 lim

climc 23626

cdv 23627

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-cc 9257 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 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 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-disj 4621 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-of 6897 df-ofr 6898 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-omul 7565 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-acn 8768 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-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-xnn0 11364 df-z 11378 df-dec 11494 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-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-ef 14798 df-sin 14800 df-cos 14801 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-t1 21118 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389 df-itg2 23390 df-ibl 23391 df-itg 23392 df-0p 23437 df-ditg 23611 df-limc 23630 df-dv 23631

This theorem is referenced by: fourierdlem113 40436

W3C validator