fourierdlem83 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem83 40406

Description: The fourier partial sum for

rewritten as an integral. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem83.f
fourierdlem83.c
fourierdlem83.fl1
fourierdlem83.a
fourierdlem83.b
fourierdlem83.x
fourierdlem83.s
fourierdlem83.d
fourierdlem83.n

**Assertion**
Ref	Expression
fourierdlem83

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem fourierdlem83 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem83.s	. . . 4
2	1	a1i 11	. . 3
3		oveq2 6658	. . . . . 6
4	3	sumeq1d 14431	. . . . 5
5	4	oveq2d 6666	. . . 4
6	5	adantl 482	. . 3 $/\$
7		fourierdlem83.n	. . 3
8		id 22	. . . . . 6
9		0nn0 11307	. . . . . . 7
10	9	a1i 11	. . . . . 6
11	9	elexi 3213	. . . . . . 7
12		eleq1 2689	. . . . . . . . 9
13	12	anbi2d 740	. . . . . . . 8 $/\$ $/\$
14		fveq2 6191	. . . . . . . . 9
15	14	eleq1d 2686	. . . . . . . 8
16	13, 15	imbi12d 334	. . . . . . 7 $/\$ $/\$
17		fourierdlem83.f	. . . . . . . . . 10
18		fourierdlem83.c	. . . . . . . . . 10
19		fourierdlem83.fl1	. . . . . . . . . 10
20		fourierdlem83.a	. . . . . . . . . 10
21		fourierdlem83.b	. . . . . . . . . 10
22	17, 18, 19, 20, 21	fourierdlem22 40346	. . . . . . . . 9 $/\$
23	22	simpld 475	. . . . . . . 8
24	23	imp 445	. . . . . . 7 $/\$
25	11, 16, 24	vtocl 3259	. . . . . 6 $/\$
26	8, 10, 25	syl2anc 693	. . . . 5
27	26	rehalfcld 11279	. . . 4
28		fzfid 12772	. . . . 5
29		eleq1 2689	. . . . . . . . . . . . . 14
30	29	anbi2d 740	. . . . . . . . . . . . 13 $/\$ $/\$
31		simpl 473	. . . . . . . . . . . . . . . . . 18 $/\$
32	31	oveq1d 6665	. . . . . . . . . . . . . . . . 17 $/\$
33	32	fveq2d 6195	. . . . . . . . . . . . . . . 16 $/\$
34	33	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$
35	34	itgeq2dv 23548	. . . . . . . . . . . . . 14
36	35	eleq1d 2686	. . . . . . . . . . . . 13
37	30, 36	imbi12d 334	. . . . . . . . . . . 12 $/\$ $/\$
38	17	adantr 481	. . . . . . . . . . . . . 14 $/\$
39	19	adantr 481	. . . . . . . . . . . . . 14 $/\$
40		simpr 477	. . . . . . . . . . . . . 14 $/\$
41	38, 18, 39, 20, 40	fourierdlem16 40340	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
42	41	simprd 479	. . . . . . . . . . . 12 $/\$
43	37, 42	chvarv 2263	. . . . . . . . . . 11 $/\$
44		pire 24210	. . . . . . . . . . . 12
45	44	a1i 11	. . . . . . . . . . 11 $/\$
46		0re 10040	. . . . . . . . . . . . 13
47		pipos 24212	. . . . . . . . . . . . 13
48	46, 47	gtneii 10149	. . . . . . . . . . . 12
49	48	a1i 11	. . . . . . . . . . 11 $/\$
50	43, 45, 49	redivcld 10853	. . . . . . . . . 10 $/\$
51	50, 20	fmptd 6385	. . . . . . . . 9
52	51	adantr 481	. . . . . . . 8 $/\$
53		elfznn 12370	. . . . . . . . . 10
54	53	nnnn0d 11351	. . . . . . . . 9
55	54	adantl 482	. . . . . . . 8 $/\$
56	52, 55	ffvelrnd 6360	. . . . . . 7 $/\$
57	55	nn0red 11352	. . . . . . . . 9 $/\$
58		fourierdlem83.x	. . . . . . . . . 10
59	58	adantr 481	. . . . . . . . 9 $/\$
60	57, 59	remulcld 10070	. . . . . . . 8 $/\$
61	60	recoscld 14874	. . . . . . 7 $/\$
62	56, 61	remulcld 10070	. . . . . 6 $/\$
63		eleq1 2689	. . . . . . . . . . . . . 14
64	63	anbi2d 740	. . . . . . . . . . . . 13 $/\$ $/\$
65		oveq1 6657	. . . . . . . . . . . . . . . . . 18
66	65	fveq2d 6195	. . . . . . . . . . . . . . . . 17
67	66	oveq2d 6666	. . . . . . . . . . . . . . . 16
68	67	adantr 481	. . . . . . . . . . . . . . 15 $/\$
69	68	itgeq2dv 23548	. . . . . . . . . . . . . 14
70	69	eleq1d 2686	. . . . . . . . . . . . 13
71	64, 70	imbi12d 334	. . . . . . . . . . . 12 $/\$ $/\$
72	17	adantr 481	. . . . . . . . . . . . . 14 $/\$
73	19	adantr 481	. . . . . . . . . . . . . 14 $/\$
74		simpr 477	. . . . . . . . . . . . . 14 $/\$
75	72, 18, 73, 21, 74	fourierdlem21 40345	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
76	75	simprd 479	. . . . . . . . . . . 12 $/\$
77	71, 76	chvarv 2263	. . . . . . . . . . 11 $/\$
78	44	a1i 11	. . . . . . . . . . 11 $/\$
79	48	a1i 11	. . . . . . . . . . 11 $/\$
80	77, 78, 79	redivcld 10853	. . . . . . . . . 10 $/\$
81	80, 21	fmptd 6385	. . . . . . . . 9
82	81	adantr 481	. . . . . . . 8 $/\$
83	53	adantl 482	. . . . . . . 8 $/\$
84	82, 83	ffvelrnd 6360	. . . . . . 7 $/\$
85	60	resincld 14873	. . . . . . 7 $/\$
86	84, 85	remulcld 10070	. . . . . 6 $/\$
87	62, 86	readdcld 10069	. . . . 5 $/\$
88	28, 87	fsumrecl 14465	. . . 4
89	27, 88	readdcld 10069	. . 3
90	2, 6, 7, 89	fvmptd 6288	. 2
91	20	a1i 11	. . . . . . 7
92		oveq1 6657	. . . . . . . . . . . . 13
93	92	fveq2d 6195	. . . . . . . . . . . 12
94	93	oveq2d 6666	. . . . . . . . . . 11
95	94	adantr 481	. . . . . . . . . 10 $/\$
96	95	itgeq2dv 23548	. . . . . . . . 9
97	96	adantl 482	. . . . . . . 8 $/\$
98	97	oveq1d 6665	. . . . . . 7 $/\$
99	17, 18, 19, 20, 10	fourierdlem16 40340	. . . . . . . . 9 $/\$ $/\$
100	99	simprd 479	. . . . . . . 8
101	44	a1i 11	. . . . . . . 8
102	48	a1i 11	. . . . . . . 8
103	100, 101, 102	redivcld 10853	. . . . . . 7
104	91, 98, 10, 103	fvmptd 6288	. . . . . 6
105		ioosscn 39716	. . . . . . . . . . . . . . 15
106		id 22	. . . . . . . . . . . . . . . 16
107	106, 18	syl6eleq 2711	. . . . . . . . . . . . . . 15
108	105, 107	sseldi 3601	. . . . . . . . . . . . . 14
109	108	mul02d 10234	. . . . . . . . . . . . 13
110	109	fveq2d 6195	. . . . . . . . . . . 12
111		cos0 14880	. . . . . . . . . . . 12
112	110, 111	syl6eq 2672	. . . . . . . . . . 11
113	112	oveq2d 6666	. . . . . . . . . 10
114	113	adantl 482	. . . . . . . . 9 $/\$
115	17	adantr 481	. . . . . . . . . . . 12 $/\$
116		ioossre 12235	. . . . . . . . . . . . . 14
117	116, 107	sseldi 3601	. . . . . . . . . . . . 13
118	117	adantl 482	. . . . . . . . . . . 12 $/\$
119	115, 118	ffvelrnd 6360	. . . . . . . . . . 11 $/\$
120	119	recnd 10068	. . . . . . . . . 10 $/\$
121	120	mulid1d 10057	. . . . . . . . 9 $/\$
122	114, 121	eqtrd 2656	. . . . . . . 8 $/\$
123	122	itgeq2dv 23548	. . . . . . 7
124	123	oveq1d 6665	. . . . . 6
125	104, 124	eqtrd 2656	. . . . 5
126	125	oveq1d 6665	. . . 4
127	17	feqmptd 6249	. . . . . . . . 9
128	127	reseq1d 5395	. . . . . . . 8
129	44	a1i 11	. . . . . . . . . . . 12
130	129	renegcld 10457	. . . . . . . . . . 11
131		ioossicc 12259	. . . . . . . . . . . . 13
132	18, 131	eqsstri 3635	. . . . . . . . . . . 12
133	132	sseli 3599	. . . . . . . . . . 11
134		eliccre 39728	. . . . . . . . . . 11 $/\$ $/\$
135	130, 129, 133, 134	syl3anc 1326	. . . . . . . . . 10
136	135	ssriv 3607	. . . . . . . . 9
137		resmpt 5449	. . . . . . . . 9
138	136, 137	mp1i 13	. . . . . . . 8
139	128, 138	eqtr2d 2657	. . . . . . 7
140	139, 19	eqeltrd 2701	. . . . . 6
141	119, 140	itgcl 23550	. . . . 5
142	101	recnd 10068	. . . . 5
143		2cnd 11093	. . . . 5
144		2ne0 11113	. . . . . 6
145	144	a1i 11	. . . . 5
146	141, 142, 143, 102, 145	divdiv32d 10826	. . . 4
147	141, 143, 145	divrecd 10804	. . . . . 6
148	143, 145	reccld 10794	. . . . . . 7
149	141, 148	mulcomd 10061	. . . . . 6
150	148, 119, 140	itgmulc2 23600	. . . . . 6
151	147, 149, 150	3eqtrd 2660	. . . . 5
152	151	oveq1d 6665	. . . 4
153	126, 146, 152	3eqtrd 2660	. . 3
154	55, 50	syldan 487	. . . . . . . . . 10 $/\$
155	20	fvmpt2 6291	. . . . . . . . . 10 $/\$
156	55, 154, 155	syl2anc 693	. . . . . . . . 9 $/\$
157	156	oveq1d 6665	. . . . . . . 8 $/\$
158	154	recnd 10068	. . . . . . . . 9 $/\$
159	61	recnd 10068	. . . . . . . . 9 $/\$
160	158, 159	mulcomd 10061	. . . . . . . 8 $/\$
161	55, 43	syldan 487	. . . . . . . . . . 11 $/\$
162	161	recnd 10068	. . . . . . . . . 10 $/\$
163	142	adantr 481	. . . . . . . . . 10 $/\$
164	48	a1i 11	. . . . . . . . . 10 $/\$
165	159, 162, 163, 164	divassd 10836	. . . . . . . . 9 $/\$
166	17	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$
167	117	adantl 482	. . . . . . . . . . . . . . 15 $/\$ $/\$
168	166, 167	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$ $/\$
169		nn0re 11301	. . . . . . . . . . . . . . . . 17
170	169	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$
171	170, 167	remulcld 10070	. . . . . . . . . . . . . . 15 $/\$ $/\$
172	171	recoscld 14874	. . . . . . . . . . . . . 14 $/\$ $/\$
173	168, 172	remulcld 10070	. . . . . . . . . . . . 13 $/\$ $/\$
174	54, 173	sylanl2 683	. . . . . . . . . . . 12 $/\$ $/\$
175		ioombl 23333	. . . . . . . . . . . . . . . . . . 19
176	18, 175	eqeltri 2697	. . . . . . . . . . . . . . . . . 18
177	176	elexi 3213	. . . . . . . . . . . . . . . . 17
178	177	a1i 11	. . . . . . . . . . . . . . . 16 $/\$
179		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$
180		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$
181	178, 172, 168, 179, 180	offval2 6914	. . . . . . . . . . . . . . 15 $/\$
182	172	recnd 10068	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
183	120	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
184	182, 183	mulcomd 10061	. . . . . . . . . . . . . . . 16 $/\$ $/\$
185	184	mpteq2dva 4744	. . . . . . . . . . . . . . 15 $/\$
186	181, 185	eqtr2d 2657	. . . . . . . . . . . . . 14 $/\$
187		coscn 24199	. . . . . . . . . . . . . . . . . 18
188	187	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
189		ax-resscn 9993	. . . . . . . . . . . . . . . . . . . . 21
190	136, 189	sstri 3612	. . . . . . . . . . . . . . . . . . . 20
191	190	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
192	169	recnd 10068	. . . . . . . . . . . . . . . . . . . 20
193	192	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
194		ssid 3624	. . . . . . . . . . . . . . . . . . . 20
195	194	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
196	191, 193, 195	constcncfg 40084	. . . . . . . . . . . . . . . . . 18 $/\$
197	191, 195	idcncfg 40085	. . . . . . . . . . . . . . . . . 18 $/\$
198	196, 197	mulcncf 23215	. . . . . . . . . . . . . . . . 17 $/\$
199	188, 198	cncfmpt1f 22716	. . . . . . . . . . . . . . . 16 $/\$
200		cnmbf 23426	. . . . . . . . . . . . . . . 16 $/\$ MblFn
201	176, 199, 200	sylancr 695	. . . . . . . . . . . . . . 15 $/\$ MblFn
202	140	adantr 481	. . . . . . . . . . . . . . 15 $/\$
203		1re 10039	. . . . . . . . . . . . . . . . 17
204		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$
205	169	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
206	117	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
207	205, 206	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
208	207	recoscld 14874	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
209	208	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . 22
210	209	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
211		dmmptg 5632	. . . . . . . . . . . . . . . . . . . . 21
212	210, 211	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
213	204, 212	eleqtrd 2703	. . . . . . . . . . . . . . . . . . 19 $/\$
214		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
215		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . 24
216	215	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23
217	216	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
218		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
219	169	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
220	136, 218	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
221	219, 220	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
222	221	recoscld 14874	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
223	214, 217, 218, 222	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . 21 $/\$
224	223	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 $/\$
225		abscosbd 39490	. . . . . . . . . . . . . . . . . . . . 21
226	221, 225	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
227	224, 226	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . 19 $/\$
228	213, 227	syldan 487	. . . . . . . . . . . . . . . . . 18 $/\$
229	228	ralrimiva 2966	. . . . . . . . . . . . . . . . 17
230		breq2 4657	. . . . . . . . . . . . . . . . . . 19
231	230	ralbidv 2986	. . . . . . . . . . . . . . . . . 18
232	231	rspcev 3309	. . . . . . . . . . . . . . . . 17 $/\$
233	203, 229, 232	sylancr 695	. . . . . . . . . . . . . . . 16
234	233	adantl 482	. . . . . . . . . . . . . . 15 $/\$
235		bddmulibl 23605	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$
236	201, 202, 234, 235	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$
237	186, 236	eqeltrd 2701	. . . . . . . . . . . . 13 $/\$
238	55, 237	syldan 487	. . . . . . . . . . . 12 $/\$
239	159, 174, 238	itgmulc2 23600	. . . . . . . . . . 11 $/\$
240	159	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$
241	120	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$
242	54, 182	sylanl2 683	. . . . . . . . . . . . . 14 $/\$ $/\$
243	240, 241, 242	mul12d 10245	. . . . . . . . . . . . 13 $/\$ $/\$
244	240, 242	mulcomd 10061	. . . . . . . . . . . . . 14 $/\$ $/\$
245	244	oveq2d 6666	. . . . . . . . . . . . 13 $/\$ $/\$
246	243, 245	eqtrd 2656	. . . . . . . . . . . 12 $/\$ $/\$
247	246	itgeq2dv 23548	. . . . . . . . . . 11 $/\$
248	239, 247	eqtrd 2656	. . . . . . . . . 10 $/\$
249	248	oveq1d 6665	. . . . . . . . 9 $/\$
250	165, 249	eqtr3d 2658	. . . . . . . 8 $/\$
251	157, 160, 250	3eqtrd 2660	. . . . . . 7 $/\$
252	83, 80	syldan 487	. . . . . . . . . 10 $/\$
253	21	fvmpt2 6291	. . . . . . . . . 10 $/\$
254	83, 252, 253	syl2anc 693	. . . . . . . . 9 $/\$
255	254	oveq1d 6665	. . . . . . . 8 $/\$
256	252	recnd 10068	. . . . . . . . 9 $/\$
257	85	recnd 10068	. . . . . . . . 9 $/\$
258	256, 257	mulcomd 10061	. . . . . . . 8 $/\$
259	83, 77	syldan 487	. . . . . . . . . . 11 $/\$
260	259	recnd 10068	. . . . . . . . . 10 $/\$
261	257, 260, 163, 164	divassd 10836	. . . . . . . . 9 $/\$
262	119	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$
263		nnre 11027	. . . . . . . . . . . . . . . . . 18
264	263	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
265	117	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
266	264, 265	remulcld 10070	. . . . . . . . . . . . . . . 16 $/\$
267	266	resincld 14873	. . . . . . . . . . . . . . 15 $/\$
268	267	adantll 750	. . . . . . . . . . . . . 14 $/\$ $/\$
269	262, 268	remulcld 10070	. . . . . . . . . . . . 13 $/\$ $/\$
270	53, 269	sylanl2 683	. . . . . . . . . . . 12 $/\$ $/\$
271	177	a1i 11	. . . . . . . . . . . . . . . 16 $/\$
272		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$
273		eqidd 2623	. . . . . . . . . . . . . . . 16 $/\$
274	271, 268, 262, 272, 273	offval2 6914	. . . . . . . . . . . . . . 15 $/\$
275	268	recnd 10068	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
276	120	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
277	275, 276	mulcomd 10061	. . . . . . . . . . . . . . . 16 $/\$ $/\$
278	277	mpteq2dva 4744	. . . . . . . . . . . . . . 15 $/\$
279	274, 278	eqtr2d 2657	. . . . . . . . . . . . . 14 $/\$
280		sincn 24198	. . . . . . . . . . . . . . . . . 18
281	280	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
282	190	a1i 11	. . . . . . . . . . . . . . . . . . . 20
283	263	recnd 10068	. . . . . . . . . . . . . . . . . . . 20
284	194	a1i 11	. . . . . . . . . . . . . . . . . . . 20
285	282, 283, 284	constcncfg 40084	. . . . . . . . . . . . . . . . . . 19
286	282, 284	idcncfg 40085	. . . . . . . . . . . . . . . . . . 19
287	285, 286	mulcncf 23215	. . . . . . . . . . . . . . . . . 18
288	287	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
289	281, 288	cncfmpt1f 22716	. . . . . . . . . . . . . . . 16 $/\$
290		cnmbf 23426	. . . . . . . . . . . . . . . 16 $/\$ MblFn
291	176, 289, 290	sylancr 695	. . . . . . . . . . . . . . 15 $/\$ MblFn
292	140	adantr 481	. . . . . . . . . . . . . . 15 $/\$
293		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$
294	267	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . . 22
295		dmmptg 5632	. . . . . . . . . . . . . . . . . . . . . 22
296	294, 295	syl 17	. . . . . . . . . . . . . . . . . . . . 21
297	296	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
298	293, 297	eleqtrd 2703	. . . . . . . . . . . . . . . . . . 19 $/\$
299		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
300	215	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23
301	300	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
302		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
303	263	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
304	136, 302	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
305	303, 304	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
306	305	resincld 14873	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
307	299, 301, 302, 306	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . 21 $/\$
308	307	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 $/\$
309		abssinbd 39509	. . . . . . . . . . . . . . . . . . . . 21
310	305, 309	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$
311	308, 310	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . 19 $/\$
312	298, 311	syldan 487	. . . . . . . . . . . . . . . . . 18 $/\$
313	312	ralrimiva 2966	. . . . . . . . . . . . . . . . 17
314		breq2 4657	. . . . . . . . . . . . . . . . . . 19
315	314	ralbidv 2986	. . . . . . . . . . . . . . . . . 18
316	315	rspcev 3309	. . . . . . . . . . . . . . . . 17 $/\$
317	203, 313, 316	sylancr 695	. . . . . . . . . . . . . . . 16
318	317	adantl 482	. . . . . . . . . . . . . . 15 $/\$
319		bddmulibl 23605	. . . . . . . . . . . . . . 15 MblFn $/\$ $/\$
320	291, 292, 318, 319	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$
321	279, 320	eqeltrd 2701	. . . . . . . . . . . . 13 $/\$
322	83, 321	syldan 487	. . . . . . . . . . . 12 $/\$
323	257, 270, 322	itgmulc2 23600	. . . . . . . . . . 11 $/\$
324	257	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$
325	53, 275	sylanl2 683	. . . . . . . . . . . . . 14 $/\$ $/\$
326	324, 241, 325	mul12d 10245	. . . . . . . . . . . . 13 $/\$ $/\$
327	324, 325	mulcomd 10061	. . . . . . . . . . . . . 14 $/\$ $/\$
328	327	oveq2d 6666	. . . . . . . . . . . . 13 $/\$ $/\$
329	326, 328	eqtrd 2656	. . . . . . . . . . . 12 $/\$ $/\$
330	329	itgeq2dv 23548	. . . . . . . . . . 11 $/\$
331	323, 330	eqtrd 2656	. . . . . . . . . 10 $/\$
332	331	oveq1d 6665	. . . . . . . . 9 $/\$
333	261, 332	eqtr3d 2658	. . . . . . . 8 $/\$
334	255, 258, 333	3eqtrd 2660	. . . . . . 7 $/\$
335	251, 334	oveq12d 6668	. . . . . 6 $/\$
336	54, 168	sylanl2 683	. . . . . . . . 9 $/\$ $/\$
337	55, 208	sylan 488	. . . . . . . . . 10 $/\$ $/\$
338	61	adantr 481	. . . . . . . . . 10 $/\$ $/\$
339	337, 338	remulcld 10070	. . . . . . . . 9 $/\$ $/\$
340	336, 339	remulcld 10070	. . . . . . . 8 $/\$ $/\$
341	241, 242, 240	mul13d 39491	. . . . . . . . . . 11 $/\$ $/\$
342	242, 241	mulcomd 10061	. . . . . . . . . . . 12 $/\$ $/\$
343	342	oveq2d 6666	. . . . . . . . . . 11 $/\$ $/\$
344	341, 343	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$
345	344	mpteq2dva 4744	. . . . . . . . 9 $/\$
346	159, 174, 238	iblmulc2 23597	. . . . . . . . 9 $/\$
347	345, 346	eqeltrd 2701	. . . . . . . 8 $/\$
348	340, 347	itgcl 23550	. . . . . . 7 $/\$
349	83, 267	sylan 488	. . . . . . . . . 10 $/\$ $/\$
350	85	adantr 481	. . . . . . . . . 10 $/\$ $/\$
351	349, 350	remulcld 10070	. . . . . . . . 9 $/\$ $/\$
352	336, 351	remulcld 10070	. . . . . . . 8 $/\$ $/\$
353	241, 325, 324	mul13d 39491	. . . . . . . . . . 11 $/\$ $/\$
354	325, 241	mulcomd 10061	. . . . . . . . . . . 12 $/\$ $/\$
355	354	oveq2d 6666	. . . . . . . . . . 11 $/\$ $/\$
356	353, 355	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$
357	356	mpteq2dva 4744	. . . . . . . . 9 $/\$
358	257, 270, 322	iblmulc2 23597	. . . . . . . . 9 $/\$
359	357, 358	eqeltrd 2701	. . . . . . . 8 $/\$
360	352, 359	itgcl 23550	. . . . . . 7 $/\$
361	348, 360, 163, 164	divdird 10839	. . . . . 6 $/\$
362	53	nncnd 11036	. . . . . . . . . . . . . . 15
363	362	ad2antlr 763	. . . . . . . . . . . . . 14 $/\$ $/\$
364	108	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
365	58	recnd 10068	. . . . . . . . . . . . . . 15
366	365	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$
367	363, 364, 366	subdid 10486	. . . . . . . . . . . . 13 $/\$ $/\$
368	367	fveq2d 6195	. . . . . . . . . . . 12 $/\$ $/\$
369	363, 364	mulcld 10060	. . . . . . . . . . . . 13 $/\$ $/\$
370	363, 366	mulcld 10060	. . . . . . . . . . . . 13 $/\$ $/\$
371		cossub 14899	. . . . . . . . . . . . 13 $/\$
372	369, 370, 371	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$
373	368, 372	eqtrd 2656	. . . . . . . . . . 11 $/\$ $/\$
374	373	oveq2d 6666	. . . . . . . . . 10 $/\$ $/\$
375	339	recnd 10068	. . . . . . . . . . 11 $/\$ $/\$
376	351	recnd 10068	. . . . . . . . . . 11 $/\$ $/\$
377	241, 375, 376	adddid 10064	. . . . . . . . . 10 $/\$ $/\$
378	374, 377	eqtrd 2656	. . . . . . . . 9 $/\$ $/\$
379	378	itgeq2dv 23548	. . . . . . . 8 $/\$
380	340, 347, 352, 359	itgadd 23591	. . . . . . . 8 $/\$
381	379, 380	eqtr2d 2657	. . . . . . 7 $/\$
382	381	oveq1d 6665	. . . . . 6 $/\$
383	335, 361, 382	3eqtr2d 2662	. . . . 5 $/\$
384	383	sumeq2dv 14433	. . . 4
385	57	adantr 481	. . . . . . . . 9 $/\$ $/\$
386	117	adantl 482	. . . . . . . . . 10 $/\$ $/\$
387	58	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$
388	386, 387	resubcld 10458	. . . . . . . . 9 $/\$ $/\$
389	385, 388	remulcld 10070	. . . . . . . 8 $/\$ $/\$
390	389	recoscld 14874	. . . . . . 7 $/\$ $/\$
391	336, 390	remulcld 10070	. . . . . 6 $/\$ $/\$
392	177	a1i 11	. . . . . . . . 9 $/\$
393		eqidd 2623	. . . . . . . . 9 $/\$
394		eqidd 2623	. . . . . . . . 9 $/\$
395	392, 390, 336, 393, 394	offval2 6914	. . . . . . . 8 $/\$
396	390	recnd 10068	. . . . . . . . . 10 $/\$ $/\$
397	396, 241	mulcomd 10061	. . . . . . . . 9 $/\$ $/\$
398	397	mpteq2dva 4744	. . . . . . . 8 $/\$
399	395, 398	eqtr2d 2657	. . . . . . 7 $/\$
400	187	a1i 11	. . . . . . . . . 10 $/\$
401	83, 285	syl 17	. . . . . . . . . . 11 $/\$
402	83, 286	syl 17	. . . . . . . . . . . 12 $/\$
403	190	a1i 11	. . . . . . . . . . . . 13 $/\$
404	365	adantr 481	. . . . . . . . . . . . 13 $/\$
405	194	a1i 11	. . . . . . . . . . . . 13 $/\$
406	403, 404, 405	constcncfg 40084	. . . . . . . . . . . 12 $/\$
407	402, 406	subcncf 40082	. . . . . . . . . . 11 $/\$
408	401, 407	mulcncf 23215	. . . . . . . . . 10 $/\$
409	400, 408	cncfmpt1f 22716	. . . . . . . . 9 $/\$
410		cnmbf 23426	. . . . . . . . 9 $/\$ MblFn
411	176, 409, 410	sylancr 695	. . . . . . . 8 $/\$ MblFn
412	140	adantr 481	. . . . . . . 8 $/\$
413		simpr 477	. . . . . . . . . . . 12 $/\$ $/\$
414	390	ralrimiva 2966	. . . . . . . . . . . . . 14 $/\$
415		dmmptg 5632	. . . . . . . . . . . . . 14
416	414, 415	syl 17	. . . . . . . . . . . . 13 $/\$
417	416	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$
418	413, 417	eleqtrd 2703	. . . . . . . . . . 11 $/\$ $/\$
419		eqidd 2623	. . . . . . . . . . . . . 14 $/\$ $/\$
420		oveq1 6657	. . . . . . . . . . . . . . . . 17
421	420	oveq2d 6666	. . . . . . . . . . . . . . . 16
422	421	fveq2d 6195	. . . . . . . . . . . . . . 15
423	422	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
424		simpr 477	. . . . . . . . . . . . . 14 $/\$ $/\$
425	57	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
426	55, 220	sylan 488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
427	58	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
428	426, 427	resubcld 10458	. . . . . . . . . . . . . . . 16 $/\$ $/\$
429	425, 428	remulcld 10070	. . . . . . . . . . . . . . 15 $/\$ $/\$
430	429	recoscld 14874	. . . . . . . . . . . . . 14 $/\$ $/\$
431	419, 423, 424, 430	fvmptd 6288	. . . . . . . . . . . . 13 $/\$ $/\$
432	431	fveq2d 6195	. . . . . . . . . . . 12 $/\$ $/\$
433		abscosbd 39490	. . . . . . . . . . . . 13
434	429, 433	syl 17	. . . . . . . . . . . 12 $/\$ $/\$
435	432, 434	eqbrtrd 4675	. . . . . . . . . . 11 $/\$ $/\$
436	418, 435	syldan 487	. . . . . . . . . 10 $/\$ $/\$
437	436	ralrimiva 2966	. . . . . . . . 9 $/\$
438		breq2 4657	. . . . . . . . . . 11
439	438	ralbidv 2986	. . . . . . . . . 10
440	439	rspcev 3309	. . . . . . . . 9 $/\$
441	203, 437, 440	sylancr 695	. . . . . . . 8 $/\$
442		bddmulibl 23605	. . . . . . . 8 MblFn $/\$ $/\$
443	411, 412, 441, 442	syl3anc 1326	. . . . . . 7 $/\$
444	399, 443	eqeltrd 2701	. . . . . 6 $/\$
445	391, 444	itgcl 23550	. . . . 5 $/\$
446	28, 142, 445, 102	fsumdivc 14518	. . . 4
447	176	a1i 11	. . . . . . . 8
448		anass 681	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
449		ancom 466	. . . . . . . . . . 11 $/\$ $/\$
450	449	anbi2i 730	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
451	448, 450	bitri 264	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
452	451, 391	sylbir 225	. . . . . . . 8 $/\$ $/\$
453	447, 28, 452, 444	itgfsum 23593	. . . . . . 7 $/\$
454	453	simprd 479	. . . . . 6
455	454	eqcomd 2628	. . . . 5
456	455	oveq1d 6665	. . . 4
457	384, 446, 456	3eqtr2d 2662	. . 3
458	153, 457	oveq12d 6668	. 2
459		fourierdlem83.d	. . . . . . . . . . 11
460	7	adantr 481	. . . . . . . . . . 11 $/\$
461		eqid 2622	. . . . . . . . . . 11
462		eqid 2622	. . . . . . . . . . 11
463	459, 460, 461, 462	dirkertrigeq 40318	. . . . . . . . . 10 $/\$
464		oveq2 6658	. . . . . . . . . . . . . . 15
465	464	fveq2d 6195	. . . . . . . . . . . . . 14
466	465	sumeq2sdv 14435	. . . . . . . . . . . . 13
467	466	oveq2d 6666	. . . . . . . . . . . 12
468	467	oveq1d 6665	. . . . . . . . . . 11
469	468	adantl 482	. . . . . . . . . 10 $/\$ $/\$
470	58	adantr 481	. . . . . . . . . . 11 $/\$
471	118, 470	resubcld 10458	. . . . . . . . . 10 $/\$
472		halfre 11246	. . . . . . . . . . . . 13
473	472	a1i 11	. . . . . . . . . . . 12 $/\$
474		fzfid 12772	. . . . . . . . . . . . 13 $/\$
475	390	an32s 846	. . . . . . . . . . . . 13 $/\$ $/\$
476	474, 475	fsumrecl 14465	. . . . . . . . . . . 12 $/\$
477	473, 476	readdcld 10069	. . . . . . . . . . 11 $/\$
478	44	a1i 11	. . . . . . . . . . 11 $/\$
479	48	a1i 11	. . . . . . . . . . 11 $/\$
480	477, 478, 479	redivcld 10853	. . . . . . . . . 10 $/\$
481	463, 469, 471, 480	fvmptd 6288	. . . . . . . . 9 $/\$
482	481, 480	eqeltrd 2701	. . . . . . . 8 $/\$
483	119, 482	remulcld 10070	. . . . . . 7 $/\$
484	177	a1i 11	. . . . . . . . . 10
485		eqidd 2623	. . . . . . . . . 10
486		eqidd 2623	. . . . . . . . . 10
487	484, 482, 119, 485, 486	offval2 6914	. . . . . . . . 9
488	482	recnd 10068	. . . . . . . . . . 11 $/\$
489	488, 120	mulcomd 10061	. . . . . . . . . 10 $/\$
490	489	mpteq2dva 4744	. . . . . . . . 9
491	487, 490	eqtr2d 2657	. . . . . . . 8
492		eqid 2622	. . . . . . . . . . 11
493		eqid 2622	. . . . . . . . . . . 12
494	194	a1i 11	. . . . . . . . . . . . . 14
495		cncfss 22702	. . . . . . . . . . . . . 14 $/\$
496	189, 494, 495	sylancr 695	. . . . . . . . . . . . 13
497		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$
498	58	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
499	497, 498	resubcld 10458	. . . . . . . . . . . . . . . 16 $/\$
500		eqid 2622	. . . . . . . . . . . . . . . 16
501	499, 500	fmptd 6385	. . . . . . . . . . . . . . 15
502	189	a1i 11	. . . . . . . . . . . . . . . . . 18
503	502, 494	idcncfg 40085	. . . . . . . . . . . . . . . . 17
504	502, 365, 494	constcncfg 40084	. . . . . . . . . . . . . . . . 17
505	503, 504	subcncf 40082	. . . . . . . . . . . . . . . 16
506		cncffvrn 22701	. . . . . . . . . . . . . . . 16 $/\$
507	189, 505, 506	sylancr 695	. . . . . . . . . . . . . . 15
508	501, 507	mpbird 247	. . . . . . . . . . . . . 14
509	459	dirkercncf 40324	. . . . . . . . . . . . . . 15
510	7, 509	syl 17	. . . . . . . . . . . . . 14
511	508, 510	cncfcompt 40096	. . . . . . . . . . . . 13
512	496, 511	sseldd 3604	. . . . . . . . . . . 12
513	44	renegcli 10342	. . . . . . . . . . . . . 14
514		iccssre 12255	. . . . . . . . . . . . . 14 $/\$
515	513, 44, 514	mp2an 708	. . . . . . . . . . . . 13
516	515	a1i 11	. . . . . . . . . . . 12
517	459	dirkerf 40314	. . . . . . . . . . . . . . . 16
518	7, 517	syl 17	. . . . . . . . . . . . . . 15
519	518	adantr 481	. . . . . . . . . . . . . 14 $/\$
520	516	sselda 3603	. . . . . . . . . . . . . . 15 $/\$
521	58	adantr 481	. . . . . . . . . . . . . . 15 $/\$
522	520, 521	resubcld 10458	. . . . . . . . . . . . . 14 $/\$
523	519, 522	ffvelrnd 6360	. . . . . . . . . . . . 13 $/\$
524	523	recnd 10068	. . . . . . . . . . . 12 $/\$
525	493, 512, 516, 494, 524	cncfmptssg 40083	. . . . . . . . . . 11
526	132	a1i 11	. . . . . . . . . . 11
527	492, 525, 526, 494, 488	cncfmptssg 40083	. . . . . . . . . 10
528		cnmbf 23426	. . . . . . . . . 10 $/\$ MblFn
529	176, 527, 528	sylancr 695	. . . . . . . . 9 MblFn
530	513	a1i 11	. . . . . . . . . . . . 13
531		0red 10041	. . . . . . . . . . . . . . 15
532		negpilt0 39492	. . . . . . . . . . . . . . . 16
533	532	a1i 11	. . . . . . . . . . . . . . 15
534	47	a1i 11	. . . . . . . . . . . . . . 15
535	530, 531, 101, 533, 534	lttrd 10198	. . . . . . . . . . . . . 14
536	530, 101, 535	ltled 10185	. . . . . . . . . . . . 13
537	493, 512, 516, 502, 523	cncfmptssg 40083	. . . . . . . . . . . . 13
538	530, 101, 536, 537	evthiccabs 39718	. . . . . . . . . . . 12 $/\$
539	538	simpld 475	. . . . . . . . . . 11
540		eqidd 2623	. . . . . . . . . . . . . . . . 17 $/\$
541	420	fveq2d 6195	. . . . . . . . . . . . . . . . . 18
542	541	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
543		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$
544	518	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
545	515, 543	sseldi 3601	. . . . . . . . . . . . . . . . . . 19 $/\$
546	58	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
547	545, 546	resubcld 10458	. . . . . . . . . . . . . . . . . 18 $/\$
548	544, 547	ffvelrnd 6360	. . . . . . . . . . . . . . . . 17 $/\$
549	540, 542, 543, 548	fvmptd 6288	. . . . . . . . . . . . . . . 16 $/\$
550	549	fveq2d 6195	. . . . . . . . . . . . . . 15 $/\$
551	550	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$
552		eqidd 2623	. . . . . . . . . . . . . . . . 17 $/\$
553		oveq1 6657	. . . . . . . . . . . . . . . . . . 19
554	553	fveq2d 6195	. . . . . . . . . . . . . . . . . 18
555	554	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
556		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$
557	518	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
558	515, 556	sseldi 3601	. . . . . . . . . . . . . . . . . . 19 $/\$
559	58	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
560	558, 559	resubcld 10458	. . . . . . . . . . . . . . . . . 18 $/\$
561	557, 560	ffvelrnd 6360	. . . . . . . . . . . . . . . . 17 $/\$
562	552, 555, 556, 561	fvmptd 6288	. . . . . . . . . . . . . . . 16 $/\$
563	562	fveq2d 6195	. . . . . . . . . . . . . . 15 $/\$
564	563	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$
565	551, 564	breq12d 4666	. . . . . . . . . . . . 13 $/\$ $/\$
566	565	ralbidva 2985	. . . . . . . . . . . 12 $/\$
567	566	rexbidva 3049	. . . . . . . . . . 11
568	539, 567	mpbid 222	. . . . . . . . . 10
569	561	recnd 10068	. . . . . . . . . . . . . 14 $/\$
570	569	abscld 14175	. . . . . . . . . . . . 13 $/\$
571	570	3adant3 1081	. . . . . . . . . . . 12 $/\$ $/\$
572		nfv 1843	. . . . . . . . . . . . . 14
573		nfv 1843	. . . . . . . . . . . . . 14
574		nfra1 2941	. . . . . . . . . . . . . 14
575	572, 573, 574	nf3an 1831	. . . . . . . . . . . . 13 $/\$ $/\$
576		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$
577	482	ralrimiva 2966	. . . . . . . . . . . . . . . . . . 19
578		dmmptg 5632	. . . . . . . . . . . . . . . . . . 19
579	577, 578	syl 17	. . . . . . . . . . . . . . . . . 18
580	579	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
581	576, 580	eleqtrd 2703	. . . . . . . . . . . . . . . 16 $/\$
582	581	3ad2antl1 1223	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
583		eqidd 2623	. . . . . . . . . . . . . . . . . . . 20 $/\$
584	541	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
585		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$
586	518	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
587	136, 585	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
588	58	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
589	587, 588	resubcld 10458	. . . . . . . . . . . . . . . . . . . . 21 $/\$
590	586, 589	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . 20 $/\$
591	583, 584, 585, 590	fvmptd 6288	. . . . . . . . . . . . . . . . . . 19 $/\$
592	591	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 $/\$
593	592	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
594		simplr 792	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
595	132	sseli 3599	. . . . . . . . . . . . . . . . . . 19
596	595	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
597		rspa 2930	. . . . . . . . . . . . . . . . . 18 $/\$
598	594, 596, 597	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
599	593, 598	eqbrtrd 4675	. . . . . . . . . . . . . . . 16 $/\$ $/\$
600	599	3adantl2 1218	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
601	582, 600	syldan 487	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
602	601	ex 450	. . . . . . . . . . . . 13 $/\$ $/\$
603	575, 602	ralrimi 2957	. . . . . . . . . . . 12 $/\$ $/\$
604		breq2 4657	. . . . . . . . . . . . . 14
605	604	ralbidv 2986	. . . . . . . . . . . . 13
606	605	rspcev 3309	. . . . . . . . . . . 12 $/\$
607	571, 603, 606	syl2anc 693	. . . . . . . . . . 11 $/\$ $/\$
608	607	rexlimdv3a 3033	. . . . . . . . . 10
609	568, 608	mpd 15	. . . . . . . . 9
610		bddmulibl 23605	. . . . . . . . 9 MblFn $/\$ $/\$
611	529, 140, 609, 610	syl3anc 1326	. . . . . . . 8
612	491, 611	eqeltrd 2701	. . . . . . 7
613	142, 483, 612	itgmulc2 23600	. . . . . 6
614	142	adantr 481	. . . . . . . . 9 $/\$
615	120, 488, 614	mul13d 39491	. . . . . . . 8 $/\$
616	489	oveq2d 6666	. . . . . . . 8 $/\$
617	615, 616	eqtrd 2656	. . . . . . 7 $/\$
618	617	itgeq2dv 23548	. . . . . 6
619	613, 618	eqtr4d 2659	. . . . 5
620	148	adantr 481	. . . . . . . . 9 $/\$
621	620, 120	mulcomd 10061	. . . . . . . 8 $/\$
622	396	an32s 846	. . . . . . . . . 10 $/\$ $/\$
623	474, 120, 622	fsummulc2 14516	. . . . . . . . 9 $/\$
624	623	eqcomd 2628	. . . . . . . 8 $/\$
625	621, 624	oveq12d 6668	. . . . . . 7 $/\$
626	474, 622	fsumcl 14464	. . . . . . . 8 $/\$
627	120, 620, 626	adddid 10064	. . . . . . 7 $/\$
628	481	oveq1d 6665	. . . . . . . . 9 $/\$
629	620, 626	addcld 10059	. . . . . . . . . 10 $/\$
630	629, 614, 479	divcan1d 10802	. . . . . . . . 9 $/\$
631	628, 630	eqtr2d 2657	. . . . . . . 8 $/\$
632	631	oveq2d 6666	. . . . . . 7 $/\$
633	625, 627, 632	3eqtr2rd 2663	. . . . . 6 $/\$
634	633	itgeq2dv 23548	. . . . 5
635		remulcl 10021	. . . . . . 7 $/\$
636	472, 119, 635	sylancr 695	. . . . . 6 $/\$
637	148, 119, 140	iblmulc2 23597	. . . . . 6
638	391	an32s 846	. . . . . . 7 $/\$ $/\$
639	474, 638	fsumrecl 14465	. . . . . 6 $/\$
640	453	simpld 475	. . . . . 6
641	636, 637, 639, 640	itgadd 23591	. . . . 5
642	619, 634, 641	3eqtrrd 2661	. . . 4
643	642	oveq1d 6665	. . 3
644	636, 637	itgcl 23550	. . . 4
645	639, 640	itgcl 23550	. . . 4
646	644, 645, 142, 102	divdird 10839	. . 3
647	483, 612	itgcl 23550	. . . 4
648	647, 142, 102	divcan3d 10806	. . 3
649	643, 646, 648	3eqtr3d 2664	. 2
650	90, 458, 649	3eqtrd 2660	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

cvv 3200

wss 3574

cif 4086 class class class wbr 4653

cmpt 4729

cdm 5114

cres 5116

wf 5884

cfv 5888 (class class class)co 6650

cof 6895

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

clt 10074

cle 10075

cmin 10266

cneg 10267

cdiv 10684

cn 11020

c2 11070

cn0 11292

cioo 12175

cicc 12178

cfz 12326

cmo 12668

cabs 13974

csu 14416

csin 14794

ccos 14795

cpi 14797

ccncf 22679

cvol 23232 MblFncmbf 23383

cibl 23386

citg 23387

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-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-limc 23630 df-dv 23631

This theorem is referenced by: fourierdlem111 40434

W3C validator