fourierdlem73 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem73 40396

Description: A version of the Riemann Lebesgue lemma: as

increases, the integral in

goes to zero. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem73.a
fourierdlem73.b
fourierdlem73.f
fourierdlem73.m
fourierdlem73.qf
fourierdlem73.q0
fourierdlem73.qm
fourierdlem73.qilt	$/\$ ..^
fourierdlem73.fcn	$/\$ ..^
fourierdlem73.l	$/\$ ..^ lim
fourierdlem73.r	$/\$ ..^ lim
fourierdlem73.g
fourierdlem73.gcn	$/\$ ..^
fourierdlem73.gbd
fourierdlem73.s
fourierdlem73.d

**Assertion**
Ref	Expression
fourierdlem73

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem fourierdlem73 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem73.gcn	. . . . . . . . . . . . . 14 $/\$ ..^
2		cncff 22696	. . . . . . . . . . . . . 14
3	1, 2	syl 17	. . . . . . . . . . . . 13 $/\$ ..^
4		ax-resscn 9993	. . . . . . . . . . . . . . . . 17
5	4	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ ..^
6		fourierdlem73.qf	. . . . . . . . . . . . . . . . . . . 20
7		fourierdlem73.a	. . . . . . . . . . . . . . . . . . . . 21
8		fourierdlem73.b	. . . . . . . . . . . . . . . . . . . . 21
9	7, 8	iccssred 39727	. . . . . . . . . . . . . . . . . . . 20
10	6, 9	fssd 6057	. . . . . . . . . . . . . . . . . . 19
11	10	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
12		elfzofz 12485	. . . . . . . . . . . . . . . . . . 19 ..^
13	12	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
14	11, 13	ffvelrnd 6360	. . . . . . . . . . . . . . . . 17 $/\$ ..^
15		fzofzp1 12565	. . . . . . . . . . . . . . . . . . 19 ..^
16	15	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
17	11, 16	ffvelrnd 6360	. . . . . . . . . . . . . . . . 17 $/\$ ..^
18	14, 17	iccssred 39727	. . . . . . . . . . . . . . . 16 $/\$ ..^
19		limccl 23639	. . . . . . . . . . . . . . . . . . . 20 lim
20		fourierdlem73.r	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ lim
21	19, 20	sseldi 3601	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
22	21	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
23		limccl 23639	. . . . . . . . . . . . . . . . . . . . 21 lim
24		fourierdlem73.l	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ lim
25	23, 24	sseldi 3601	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
26	25	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
27		fourierdlem73.f	. . . . . . . . . . . . . . . . . . . . 21
28	27	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
29	7	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
30	8	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
31	14	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
32	17	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
33		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
34		eliccre 39728	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
35	31, 32, 33, 34	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
36	7	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	36	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^
38	8	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . 25
39	38	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^
40	6	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^
41	40, 13	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^
42		iccgelb 12230	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43	37, 39, 41, 42	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^
44	43	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
45	31	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
46	32	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
47		iccgelb 12230	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
48	45, 46, 33, 47	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
49	29, 31, 35, 44, 48	letrd 10194	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
50		iccleub 12229	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
51	45, 46, 33, 50	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
52	36	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
53	38	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
54	40, 16	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^
55	54	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
56		iccleub 12229	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
57	52, 53, 55, 56	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
58	35, 32, 30, 51, 57	letrd 10194	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
59	29, 30, 35, 49, 58	eliccd 39726	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
60	28, 59	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
61	26, 60	ifcld 4131	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
62	22, 61	ifcld 4131	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
63		fourierdlem73.d	. . . . . . . . . . . . . . . . 17
64	62, 63	fmptd 6385	. . . . . . . . . . . . . . . 16 $/\$ ..^
65		eqid 2622	. . . . . . . . . . . . . . . . 17 ℂ_fld ℂ_fld
66	65	tgioo2 22606	. . . . . . . . . . . . . . . 16 ℂ_fld ↾_t
67		iccntr 22624	. . . . . . . . . . . . . . . . 17 $/\$
68	14, 17, 67	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ ..^
69	5, 18, 64, 66, 65, 68	dvresntr 40132	. . . . . . . . . . . . . . 15 $/\$ ..^
70		ioossicc 12259	. . . . . . . . . . . . . . . . . . . . . . 23
71	70	sseli 3599	. . . . . . . . . . . . . . . . . . . . . 22
72	71	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
73		fvres 6207	. . . . . . . . . . . . . . . . . . . . 21
74	72, 73	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
75	72, 62	syldan 487	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
76	63	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
77	72, 75, 76	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
78	14	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
79	72, 45	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
80	72, 46	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
81		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
82		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
83	79, 80, 81, 82	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
84	78, 83	gtned 10172	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
85	84	neneqd 2799	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
86	85	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
87		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . 25
88	87	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
89		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
90	79, 80, 81, 89	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
91	88, 90	ltned 10173	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
92	91	neneqd 2799	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
93	92	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
94	77, 86, 93	3eqtrrd 2661	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
95	74, 94	eqtr2d 2657	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
96	95	ralrimiva 2966	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
97		ffn 6045	. . . . . . . . . . . . . . . . . . . 20
98	64, 97	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
99		ffn 6045	. . . . . . . . . . . . . . . . . . . . . 22
100	27, 99	syl 17	. . . . . . . . . . . . . . . . . . . . 21
101	100	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
102		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ ..^
103	37, 39, 40, 102	fourierdlem8 40332	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
104		fnssres 6004	. . . . . . . . . . . . . . . . . . . 20 $/\$
105	101, 103, 104	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
106	70	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
107		fvreseq 6319	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
108	98, 105, 106, 107	syl21anc 1325	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
109	96, 108	mpbird 247	. . . . . . . . . . . . . . . . 17 $/\$ ..^
110	106	resabs1d 5428	. . . . . . . . . . . . . . . . 17 $/\$ ..^
111	109, 110	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$ ..^
112	111	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$ ..^
113	27	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^
114	9	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^
115	106, 18	sstrd 3613	. . . . . . . . . . . . . . . . 17 $/\$ ..^
116	65, 66	dvres 23675	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
117	5, 113, 114, 115, 116	syl22anc 1327	. . . . . . . . . . . . . . . 16 $/\$ ..^
118		fourierdlem73.g	. . . . . . . . . . . . . . . . . . 19
119	118	eqcomi 2631	. . . . . . . . . . . . . . . . . 18
120	119	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ ..^
121		iooretop 22569	. . . . . . . . . . . . . . . . . 18
122		retop 22565	. . . . . . . . . . . . . . . . . . 19
123		uniretop 22566	. . . . . . . . . . . . . . . . . . . 20
124	123	isopn3 20870	. . . . . . . . . . . . . . . . . . 19 $/\$
125	122, 115, 124	sylancr 695	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
126	121, 125	mpbii 223	. . . . . . . . . . . . . . . . 17 $/\$ ..^
127	120, 126	reseq12d 5397	. . . . . . . . . . . . . . . 16 $/\$ ..^
128	117, 127	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ ..^
129	69, 112, 128	3eqtrd 2660	. . . . . . . . . . . . . 14 $/\$ ..^
130	129	feq1d 6030	. . . . . . . . . . . . 13 $/\$ ..^
131	3, 130	mpbird 247	. . . . . . . . . . . 12 $/\$ ..^
132	131	feqmptd 6249	. . . . . . . . . . 11 $/\$ ..^
133	132, 129	eqtr3d 2658	. . . . . . . . . 10 $/\$ ..^
134		ioombl 23333	. . . . . . . . . . . 12
135	134	a1i 11	. . . . . . . . . . 11 $/\$ ..^
136		fourierdlem73.qilt	. . . . . . . . . . . . . 14 $/\$ ..^
137	14, 17, 136	ltled 10185	. . . . . . . . . . . . 13 $/\$ ..^
138		volioo 23337	. . . . . . . . . . . . 13 $/\$ $/\$
139	14, 17, 137, 138	syl3anc 1326	. . . . . . . . . . . 12 $/\$ ..^
140	17, 14	resubcld 10458	. . . . . . . . . . . 12 $/\$ ..^
141	139, 140	eqeltrd 2701	. . . . . . . . . . 11 $/\$ ..^
142		fourierdlem73.gbd	. . . . . . . . . . . . 13
143	142	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
144		nfv 1843	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
145		nfra1 2941	. . . . . . . . . . . . . . . 16
146	144, 145	nfan 1828	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
147		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
148		fdm 6051	. . . . . . . . . . . . . . . . . . . . . . 23
149	3, 148	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
150	149	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
151	147, 150	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
152		fvres 6207	. . . . . . . . . . . . . . . . . . . 20
153	151, 152	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
154	153	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
155	154	ad4ant14 1293	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
156		simplr 792	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
157		ssdmres 5420	. . . . . . . . . . . . . . . . . . . . . . 23
158	149, 157	sylibr 224	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
159	158	sselda 3603	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
160	151, 159	syldan 487	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
161	160	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
162		rsp 2929	. . . . . . . . . . . . . . . . . . 19
163	156, 161, 162	sylc 65	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
164	163	adantllr 755	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
165	155, 164	eqbrtrd 4675	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
166	165	ex 450	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
167	146, 166	ralrimi 2957	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
168	167	ex 450	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
169	168	reximdva 3017	. . . . . . . . . . . 12 $/\$ ..^
170	143, 169	mpd 15	. . . . . . . . . . 11 $/\$ ..^
171	135, 141, 1, 170	cnbdibl 40178	. . . . . . . . . 10 $/\$ ..^
172	133, 171	eqeltrd 2701	. . . . . . . . 9 $/\$ ..^
173	172	adantr 481	. . . . . . . 8 $/\$ ..^ $/\$
174	134	a1i 11	. . . . . . . . . 10 $/\$ ..^ $/\$
175	141	adantr 481	. . . . . . . . . 10 $/\$ ..^ $/\$
176	133, 1	eqeltrd 2701	. . . . . . . . . . . 12 $/\$ ..^
177	176	adantr 481	. . . . . . . . . . 11 $/\$ ..^ $/\$
178		coscn 24199	. . . . . . . . . . . . . 14
179	178	a1i 11	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
180		ioosscn 39716	. . . . . . . . . . . . . . . 16
181	180	a1i 11	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
182		simpr 477	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
183	182	recnd 10068	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
184		ssid 3624	. . . . . . . . . . . . . . . 16
185	184	a1i 11	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
186	181, 183, 185	constcncfg 40084	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
187	180	a1i 11	. . . . . . . . . . . . . . . 16
188	184	a1i 11	. . . . . . . . . . . . . . . 16
189	187, 188	idcncfg 40085	. . . . . . . . . . . . . . 15
190	189	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
191	186, 190	mulcncf 23215	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
192	179, 191	cncfmpt1f 22716	. . . . . . . . . . . 12 $/\$ ..^ $/\$
193	192	negcncfg 40094	. . . . . . . . . . 11 $/\$ ..^ $/\$
194	177, 193	mulcncf 23215	. . . . . . . . . 10 $/\$ ..^ $/\$
195		nfv 1843	. . . . . . . . . . . . . . . . 17 $/\$ ..^
196	195, 145	nfan 1828	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
197	129	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^
198	197, 152	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
199	198	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
200	199	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
201		simplr 792	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
202	159	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
203	201, 202, 162	sylc 65	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
204	200, 203	eqbrtrd 4675	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
205	204	ex 450	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
206	196, 205	ralrimi 2957	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
207	206	ex 450	. . . . . . . . . . . . . 14 $/\$ ..^
208	207	reximdv 3016	. . . . . . . . . . . . 13 $/\$ ..^
209	143, 208	mpd 15	. . . . . . . . . . . 12 $/\$ ..^
210	209	adantr 481	. . . . . . . . . . 11 $/\$ ..^ $/\$
211		eqidd 2623	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
212		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
213		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25
214	213	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$ ..^ $/\$
215		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25
216	212, 215	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . 24
217	214, 216	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$ ..^ $/\$
218	217, 198	chvarv 2263	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
219	212, 218	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
220		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . 24
221	220	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . 23
222	221	negeqd 10275	. . . . . . . . . . . . . . . . . . . . . 22
223	222	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
224	219, 223	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
225	224	adantllr 755	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
226		simpr 477	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
227		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . 23
228	227	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
229	3	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
230	228, 229	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
231	230	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
232		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
233		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . 26
234	233	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
235	232, 234	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
236	235	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
237	236	coscld 14861	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
238	237	negcld 10379	. . . . . . . . . . . . . . . . . . . . 21 $/\$
239	238	adantll 750	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
240	231, 239	mulcld 10060	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
241	211, 225, 226, 240	fvmptd 6288	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
242	241	fveq2d 6195	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
243	242	ad4ant14 1293	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
244	240	abscld 14175	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
245	244	ad4ant14 1293	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
246	231	abscld 14175	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
247	246	ad4ant14 1293	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
248		simpllr 799	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
249	239	abscld 14175	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
250		1red 10055	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
251	231	absge0d 14183	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
252	237	absnegd 14188	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
253		abscosbd 39490	. . . . . . . . . . . . . . . . . . . . . . 23
254	235, 253	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
255	252, 254	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . 21 $/\$
256	255	adantll 750	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
257	249, 250, 246, 251, 256	lemul2ad 10964	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
258	231, 239	absmuld 14193	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
259	246	recnd 10068	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
260	259	mulid1d 10057	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
261	260	eqcomd 2628	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
262	257, 258, 261	3brtr4d 4685	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
263	262	ad4ant14 1293	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
264		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
265		nfra1 2941	. . . . . . . . . . . . . . . . . . . . . . 23
266	195, 265	nfan 1828	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
267	199	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
268	267	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
269		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
270	268, 269	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
271	270	ex 450	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
272	271	adantlr 751	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
273	266, 272	ralimdaa 2958	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
274	264, 273	mpd 15	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
275	215	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22
276	275	breq1d 4663	. . . . . . . . . . . . . . . . . . . . 21
277	276	cbvralv 3171	. . . . . . . . . . . . . . . . . . . 20
278	274, 277	sylib 208	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
279	278	ad4ant14 1293	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
280	279	r19.21bi 2932	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
281	245, 247, 248, 263, 280	letrd 10194	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
282	243, 281	eqbrtrd 4675	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
283	282	ralrimiva 2966	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
284	131	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
285	284	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
286		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
287	87	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
288	286, 287	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
289	288	recnd 10068	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
290	289	coscld 14861	. . . . . . . . . . . . . . . . . . . . 21 $/\$
291	290	negcld 10379	. . . . . . . . . . . . . . . . . . . 20 $/\$
292	291	adantll 750	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
293	285, 292	mulcld 10060	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
294	293	ralrimiva 2966	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
295		dmmptg 5632	. . . . . . . . . . . . . . . . 17
296	294, 295	syl 17	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
297	296	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$
298	297	raleqdv 3144	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
299	283, 298	mpbird 247	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
300	299	ex 450	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
301	300	reximdva 3017	. . . . . . . . . . 11 $/\$ ..^ $/\$
302	210, 301	mpd 15	. . . . . . . . . 10 $/\$ ..^ $/\$
303	174, 175, 194, 302	cnbdibl 40178	. . . . . . . . 9 $/\$ ..^ $/\$
304	303	adantlr 751	. . . . . . . 8 $/\$ ..^ $/\$ $/\$
305	284	adantlr 751	. . . . . . . 8 $/\$ ..^ $/\$ $/\$
306		simpr 477	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$ $/\$
307	180	sseli 3599	. . . . . . . . . . 11
308	307	ad2antlr 763	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$ $/\$
309	306, 308	mulcld 10060	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$ $/\$
310	309	coscld 14861	. . . . . . . 8 $/\$ ..^ $/\$ $/\$ $/\$
311	288	ancoms 469	. . . . . . . . . 10 $/\$
312		abscosbd 39490	. . . . . . . . . 10
313	311, 312	syl 17	. . . . . . . . 9 $/\$
314	313	adantll 750	. . . . . . . 8 $/\$ ..^ $/\$ $/\$ $/\$
315	63	a1i 11	. . . . . . . . . . 11 $/\$ ..^
316	14	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
317	136	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
318		eqcom 2629	. . . . . . . . . . . . . . . . . 18
319	318	biimpri 218	. . . . . . . . . . . . . . . . 17
320	319	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
321	317, 320	breqtrd 4679	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
322	316, 321	gtned 10172	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
323	322	neneqd 2799	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
324	323	iffalsed 4097	. . . . . . . . . . . 12 $/\$ ..^ $/\$
325		iftrue 4092	. . . . . . . . . . . . 13
326	325	adantl 482	. . . . . . . . . . . 12 $/\$ ..^ $/\$
327	324, 326	eqtrd 2656	. . . . . . . . . . 11 $/\$ ..^ $/\$
328	17	leidd 10594	. . . . . . . . . . . 12 $/\$ ..^
329	14, 17, 17, 137, 328	eliccd 39726	. . . . . . . . . . 11 $/\$ ..^
330	315, 327, 329, 24	fvmptd 6288	. . . . . . . . . 10 $/\$ ..^
331	330, 25	eqeltrd 2701	. . . . . . . . 9 $/\$ ..^
332	331	adantr 481	. . . . . . . 8 $/\$ ..^ $/\$
333		eqid 2622	. . . . . . . 8
334		iftrue 4092	. . . . . . . . . . . 12
335	334	adantl 482	. . . . . . . . . . 11 $/\$ ..^ $/\$
336	14	rexrd 10089	. . . . . . . . . . . 12 $/\$ ..^
337	17	rexrd 10089	. . . . . . . . . . . 12 $/\$ ..^
338		lbicc2 12288	. . . . . . . . . . . 12 $/\$ $/\$
339	336, 337, 137, 338	syl3anc 1326	. . . . . . . . . . 11 $/\$ ..^
340	315, 335, 339, 20	fvmptd 6288	. . . . . . . . . 10 $/\$ ..^
341	340, 21	eqeltrd 2701	. . . . . . . . 9 $/\$ ..^
342	341	adantr 481	. . . . . . . 8 $/\$ ..^ $/\$
343		eqid 2622	. . . . . . . 8
344		eqid 2622	. . . . . . . 8
345		simpr 477	. . . . . . . . . 10 $/\$
346		fourierdlem73.m	. . . . . . . . . . . 12
347	346	nnrpd 11870	. . . . . . . . . . 11
348	347	adantr 481	. . . . . . . . . 10 $/\$
349	345, 348	rpdivcld 11889	. . . . . . . . 9 $/\$
350	349	adantlr 751	. . . . . . . 8 $/\$ ..^ $/\$
351		simpr 477	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
352	17	recnd 10068	. . . . . . . . . . 11 $/\$ ..^
353	352	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
354	351, 353	mulcld 10060	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$
355	354	coscld 14861	. . . . . . . 8 $/\$ ..^ $/\$ $/\$
356	17	adantr 481	. . . . . . . . . . 11 $/\$ ..^ $/\$
357	182, 356	remulcld 10070	. . . . . . . . . 10 $/\$ ..^ $/\$
358		abscosbd 39490	. . . . . . . . . 10
359	357, 358	syl 17	. . . . . . . . 9 $/\$ ..^ $/\$
360	359	adantlr 751	. . . . . . . 8 $/\$ ..^ $/\$ $/\$
361	14	recnd 10068	. . . . . . . . . . 11 $/\$ ..^
362	361	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
363	351, 362	mulcld 10060	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$
364	363	coscld 14861	. . . . . . . 8 $/\$ ..^ $/\$ $/\$
365	14	adantr 481	. . . . . . . . . . 11 $/\$ ..^ $/\$
366	182, 365	remulcld 10070	. . . . . . . . . 10 $/\$ ..^ $/\$
367		abscosbd 39490	. . . . . . . . . 10
368	366, 367	syl 17	. . . . . . . . 9 $/\$ ..^ $/\$
369	368	adantlr 751	. . . . . . . 8 $/\$ ..^ $/\$ $/\$
370		fveq2 6191	. . . . . . . . . . . . . . 15
371	370	fveq2d 6195	. . . . . . . . . . . . . 14
372	371	cbvitgv 23543	. . . . . . . . . . . . 13
373	372	oveq2i 6661	. . . . . . . . . . . 12
374	373	oveq1i 6660	. . . . . . . . . . 11
375	374	oveq1i 6660	. . . . . . . . . 10
376	375	fveq2i 6194	. . . . . . . . 9
377	376	oveq1i 6660	. . . . . . . 8
378	173, 304, 305, 310, 314, 332, 333, 342, 343, 344, 350, 355, 360, 364, 369, 377	fourierdlem47 40370	. . . . . . 7 $/\$ ..^ $/\$
379		simplll 798	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
380		simpllr 799	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ ..^
381		elioore 12205	. . . . . . . . . . . . . . . 16
382	381	adantl 482	. . . . . . . . . . . . . . 15 $/\$
383		0red 10041	. . . . . . . . . . . . . . . 16 $/\$
384		nnre 11027	. . . . . . . . . . . . . . . . 17
385	384	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
386		nngt0 11049	. . . . . . . . . . . . . . . . 17
387	386	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
388	385	rexrd 10089	. . . . . . . . . . . . . . . . 17 $/\$
389		pnfxr 10092	. . . . . . . . . . . . . . . . . 18
390	389	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
391		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$
392		ioogtlb 39717	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
393	388, 390, 391, 392	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$
394	383, 385, 382, 387, 393	lttrd 10198	. . . . . . . . . . . . . . 15 $/\$
395	382, 394	elrpd 11869	. . . . . . . . . . . . . 14 $/\$
396	395	adantll 750	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
397	14	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
398	17	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
399	64	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
400	399	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
401		rpcn 11841	. . . . . . . . . . . . . . . . . . 19
402	401	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
403	35	recnd 10068	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
404	403	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
405	402, 404	mulcld 10060	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
406	405	sincld 14860	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
407	400, 406	mulcld 10060	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
408	397, 398, 407	itgioo 23582	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
409	137	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
410	64	feqmptd 6249	. . . . . . . . . . . . . . . . 17 $/\$ ..^
411		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . 24
412	325, 411	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . 23
413	412	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
414		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . 24
415	414	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$ $/\$
416	45	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$ $/\$
417	46	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$ $/\$
418	35	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$ $/\$
419	14	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$
420	35	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$
421	48	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$
422		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
423	422	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$
424	419, 420, 421, 423	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$ $/\$
425	424	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$ $/\$
426	35	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$
427	17	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$
428	51	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$
429	318	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
430	429	necon3bi 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
431	430	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$
432	426, 427, 428, 431	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$ $/\$
433	432	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$ $/\$
434	416, 417, 418, 425, 433	eliood 39720	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$ $/\$
435		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . . 24
436	434, 435	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$ $/\$
437		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . 25
438	437	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24
439	438	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$ $/\$
440	415, 436, 439	3eqtrrd 2661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
441	413, 440	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
442	441	ifeq2da 4117	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
443	442	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
444	315, 410, 443	3eqtr3d 2664	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
445		eqid 2622	. . . . . . . . . . . . . . . . . . 19
446		fourierdlem73.fcn	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
447	195, 445, 14, 17, 446, 24, 20	cncfiooicc 40107	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
448	444, 447	eqeltrd 2701	. . . . . . . . . . . . . . . . 17 $/\$ ..^
449	410, 448	eqeltrd 2701	. . . . . . . . . . . . . . . 16 $/\$ ..^
450	449	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
451		eqid 2622	. . . . . . . . . . . . . . 15
452	129, 1	eqeltrd 2701	. . . . . . . . . . . . . . . 16 $/\$ ..^
453	452	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
454	209	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
455		simpr 477	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
456	397, 398, 409, 450, 451, 453, 454, 455	fourierdlem39 40363	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
457	408, 456	eqtr3d 2658	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
458	379, 380, 396, 457	syl21anc 1325	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
459	458	fveq2d 6195	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
460	459	breq1d 4663	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
461	460	ralbidva 2985	. . . . . . . . 9 $/\$ ..^ $/\$
462	461	rexbidva 3049	. . . . . . . 8 $/\$ ..^
463	462	adantr 481	. . . . . . 7 $/\$ ..^ $/\$
464	378, 463	mpbird 247	. . . . . 6 $/\$ ..^ $/\$
465	464	an32s 846	. . . . 5 $/\$ $/\$ ..^
466	94	oveq1d 6665	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
467	466	itgeq2dv 23548	. . . . . . . . . . . . 13 $/\$ ..^
468	467	eqcomd 2628	. . . . . . . . . . . 12 $/\$ ..^
469	468	adantr 481	. . . . . . . . . . 11 $/\$ ..^ $/\$
470	14	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$
471	17	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$
472	399	adantlr 751	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
473	381	recnd 10068	. . . . . . . . . . . . . . . 16
474	473	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
475	403	adantlr 751	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$
476	474, 475	mulcld 10060	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
477	476	sincld 14860	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
478	472, 477	mulcld 10060	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
479	470, 471, 478	itgioo 23582	. . . . . . . . . . 11 $/\$ ..^ $/\$
480	60	adantlr 751	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
481	480, 477	mulcld 10060	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
482	470, 471, 481	itgioo 23582	. . . . . . . . . . 11 $/\$ ..^ $/\$
483	469, 479, 482	3eqtr3d 2664	. . . . . . . . . 10 $/\$ ..^ $/\$
484	483	fveq2d 6195	. . . . . . . . 9 $/\$ ..^ $/\$
485	484	breq1d 4663	. . . . . . . 8 $/\$ ..^ $/\$
486	485	ralbidva 2985	. . . . . . 7 $/\$ ..^
487	486	adantlr 751	. . . . . 6 $/\$ $/\$ ..^
488	487	rexbidv 3052	. . . . 5 $/\$ $/\$ ..^
489	465, 488	mpbid 222	. . . 4 $/\$ $/\$ ..^
490	489	ralrimiva 2966	. . 3 $/\$ ..^
491	490	ralrimiva 2966	. 2 ..^
492		nfv 1843	. . . . . . 7 $/\$
493		nfra1 2941	. . . . . . 7 ..^
494	492, 493	nfan 1828	. . . . . 6 $/\$ $/\$ ..^
495		nfv 1843	. . . . . . 7 $/\$
496		nfcv 2764	. . . . . . . 8 ..^
497		nfcv 2764	. . . . . . . . 9
498		nfra1 2941	. . . . . . . . 9
499	497, 498	nfrex 3007	. . . . . . . 8
500	496, 499	nfral 2945	. . . . . . 7 ..^
501	495, 500	nfan 1828	. . . . . 6 $/\$ $/\$ ..^
502		nfmpt1 4747	. . . . . 6 ..^ inf
503		fzofi 12773	. . . . . . 7 ..^
504	503	a1i 11	. . . . . 6 $/\$ $/\$ ..^ ..^
505		simpr 477	. . . . . 6 $/\$ $/\$ ..^ ..^
506		eqid 2622	. . . . . 6
507		eqid 2622	. . . . . 6 ..^ inf ..^ inf
508		eqid 2622	. . . . . 6 ..^ inf ..^ inf
509	494, 501, 502, 504, 505, 506, 507, 508	fourierdlem31 40355	. . . . 5 $/\$ $/\$ ..^ ..^
510		simpr 477	. . . . . 6 $/\$ $/\$ ..^ ..^
511		nfv 1843	. . . . . . . 8 $/\$
512		nfre1 3005	. . . . . . . 8 ..^
513	511, 512	nfan 1828	. . . . . . 7 $/\$ $/\$ ..^
514		nfv 1843	. . . . . . . . . . 11
515		nfra1 2941	. . . . . . . . . . 11 ..^
516	495, 514, 515	nf3an 1831	. . . . . . . . . 10 $/\$ $/\$ $/\$ ..^
517		simpll 790	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
518		elioore 12205	. . . . . . . . . . . . . . . . . . . 20
519	518	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
520		0red 10041	. . . . . . . . . . . . . . . . . . . 20 $/\$
521		nnre 11027	. . . . . . . . . . . . . . . . . . . . 21
522	521	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
523		nngt0 11049	. . . . . . . . . . . . . . . . . . . . 21
524	523	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
525	522	rexrd 10089	. . . . . . . . . . . . . . . . . . . . 21 $/\$
526	389	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
527		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
528		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
529	525, 526, 527, 528	syl3anc 1326	. . . . . . . . . . . . . . . . . . . 20 $/\$
530	520, 522, 519, 524, 529	lttrd 10198	. . . . . . . . . . . . . . . . . . 19 $/\$
531	519, 530	elrpd 11869	. . . . . . . . . . . . . . . . . 18 $/\$
532	531	adantll 750	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
533	7	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
534	8	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
535	27	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . 21 $/\$
536	535	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
537	401	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
538	9	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
539	538	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
540	539	adantlr 751	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
541	537, 540	mulcld 10060	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
542	541	sincld 14860	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
543	536, 542	mulcld 10060	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
544	533, 534, 543	itgioo 23582	. . . . . . . . . . . . . . . . . 18 $/\$
545		fourierdlem73.q0	. . . . . . . . . . . . . . . . . . . . . 22
546	545	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . 21
547		fourierdlem73.qm	. . . . . . . . . . . . . . . . . . . . . 22
548	547	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . 21
549	546, 548	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20
550	549	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
551	550	itgeq1d 40172	. . . . . . . . . . . . . . . . . 18 $/\$
552		0zd 11389	. . . . . . . . . . . . . . . . . . 19 $/\$
553		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . 22
554		0p1e1 11132	. . . . . . . . . . . . . . . . . . . . . . 23
555	554	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . 22
556	553, 555	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . 21
557	346, 556	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . 20
558	557	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
559	10	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
560	136	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
561		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
562	549	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . 23
563	562	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
564	561, 563	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . 21 $/\$
565	564	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
566	565, 543	syldan 487	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
567	14	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
568	17	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
569	106, 103	sstrd 3613	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^
570	113, 569	feqresmpt 6250	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^
571	570, 446	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^
572	571	adantlr 751	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^
573		sincn 24198	. . . . . . . . . . . . . . . . . . . . . . . 24
574	573	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^
575	180	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
576	401	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
577	184	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
578	575, 576, 577	constcncfg 40084	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
579	189	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
580	578, 579	mulcncf 23215	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
581	580	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^
582	574, 581	cncfmpt1f 22716	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^
583	572, 582	mulcncf 23215	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^
584		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22
585		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22
586		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22
587	27	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
588	36	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
589	38	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
590	6	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
591		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ ..^
592	588, 589, 590, 591, 72	fourierdlem1 40325	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
593	587, 592	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
594	593	adantllr 755	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
595	576	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$
596	307	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$
597	595, 596	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
598	597	sincld 14860	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
599	570	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ lim lim
600	24, 599	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ lim
601	600	adantlr 751	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ lim
602		rpre 11839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
603	602	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
604	87	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
605	603, 604	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
606	605	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
607	606	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$ $/\$
608		recn 10026	. . . . . . . . . . . . . . . . . . . . . . . . 25
609	608	sincld 14860	. . . . . . . . . . . . . . . . . . . . . . . 24
610	609	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
611		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
612		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
613		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
614	180	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^
615	576	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^
616	568	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^
617	611, 614, 615, 616	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ lim
618	614, 612, 616	idlimc 39858	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ lim
619	611, 612, 613, 595, 596, 617, 618	mullimc 39848	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ lim
620		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
621		sinf 14854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
622	621	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
623	622	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
624	623, 573	syl6eqelr 2710	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
625	4	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
626		resincl 14870	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
627	626	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
628	620, 624, 625, 625, 627	cncfmptssg 40083	. . . . . . . . . . . . . . . . . . . . . . . . . 26
629	628	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . 25
630	629	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^
631	602	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^
632	631, 568	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^
633		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
634	630, 632, 633	cnmptlimc 23654	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ lim
635		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23
636		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
637	636	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$ $/\$
638	607, 610, 619, 634, 635, 637	limcco 23657	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ lim
639	584, 585, 586, 594, 598, 601, 638	mullimc 39848	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ lim
640	570	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ lim lim
641	20, 640	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ lim
642	641	adantlr 751	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ lim
643	606	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$ $/\$
644	567	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^
645	611, 614, 615, 644	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ lim
646	614, 612, 644	idlimc 39858	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ lim
647	611, 612, 613, 595, 596, 645, 646	mullimc 39848	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ lim
648	631, 567	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^
649		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
650	630, 648, 649	cnmptlimc 23654	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ lim
651		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
652	651	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$ $/\$
653	643, 610, 647, 650, 635, 652	limcco 23657	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ lim
654	584, 585, 586, 594, 598, 642, 653	mullimc 39848	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ lim
655	567, 568, 583, 639, 654	iblcncfioo 40194	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
656		simpll 790	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$ $/\$
657	59	adantllr 755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
658	656, 657, 543	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^ $/\$
659	567, 568, 655, 658	ibliooicc 40187	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
660	552, 558, 559, 560, 566, 659	itgspltprt 40195	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
661	544, 551, 660	3eqtrd 2660	. . . . . . . . . . . . . . . . 17 $/\$ ..^
662	517, 532, 661	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
663	503	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
664	60	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^ $/\$
665	518	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . 24
666	665	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
667	666	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
668	403	adantllr 755	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
669	667, 668	mulcld 10060	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
670	669	sincld 14860	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^ $/\$
671	664, 670	mulcld 10060	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^ $/\$
672	671	adantlllr 39199	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ ..^ $/\$
673		simplll 798	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ ..^
674	532	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ ..^
675		simpr 477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ ..^ ..^
676	673, 674, 675, 659	syl21anc 1325	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ ..^
677	672, 676	itgcl 23550	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ ..^
678	663, 677	fsumcl 14464	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
679	662, 678	eqeltrd 2701	. . . . . . . . . . . . . . 15 $/\$ $/\$
680	679	adantllr 755	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
681	680	3adantl3 1219	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ ..^ $/\$
682	681	abscld 14175	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ ..^ $/\$
683	677	abscld 14175	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ ..^
684	663, 683	fsumrecl 14465	. . . . . . . . . . . . . 14 $/\$ $/\$ ..^
685	684	adantllr 755	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ ..^
686	685	3adantl3 1219	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ ..^ $/\$ ..^
687		rpre 11839	. . . . . . . . . . . . . 14
688	687	ad2antlr 763	. . . . . . . . . . . . 13 $/\$ $/\$
689	688	3ad2antl1 1223	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ ..^ $/\$
690	662	fveq2d 6195	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^
691	663, 677	fsumabs 14533	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^ ..^
692	690, 691	eqbrtrd 4675	. . . . . . . . . . . . . 14 $/\$ $/\$ ..^
693	692	adantllr 755	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ ..^
694	693	3adantl3 1219	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ ..^ $/\$ ..^
695	503	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ ..^ $/\$ ..^
696		0zd 11389	. . . . . . . . . . . . . . . . . 18
697	346	nnzd 11481	. . . . . . . . . . . . . . . . . 18
698	346	nngt0d 11064	. . . . . . . . . . . . . . . . . 18
699		fzolb 12476	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$
700	696, 697, 698, 699	syl3anbrc 1246	. . . . . . . . . . . . . . . . 17 ..^
701		ne0i 3921	. . . . . . . . . . . . . . . . 17 ..^ ..^
702	700, 701	syl 17	. . . . . . . . . . . . . . . 16 ..^
703	702	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^
704	703	3ad2antl1 1223	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ ..^ $/\$ ..^
705		simp1l 1085	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ ..^
706	705	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^
707		simpll2 1101	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^
708	706, 707	jca 554	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ $/\$
709		simplr 792	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^
710		simpr 477	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ ..^
711		eleq1 2689	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
712	711	anbi2d 740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^
713		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
714		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
715	714	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21
716	713, 715	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20
717	716	itgeq1d 40172	. . . . . . . . . . . . . . . . . . 19
718	717	eleq1d 2686	. . . . . . . . . . . . . . . . . 18
719	712, 718	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^
720	719, 677	chvarv 2263	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ ..^
721	708, 709, 710, 720	syl21anc 1325	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^
722	721	abscld 14175	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^
723	349	rpred 11872	. . . . . . . . . . . . . . . 16 $/\$
724	723	3ad2ant1 1082	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ ..^
725	724	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^
726		simpll3 1102	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^ ..^
727		rspa 2930	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ ..^
728	727	adantr 481	. . . . . . . . . . . . . . . . 17 ..^ $/\$ $/\$ ..^ ..^
729	717	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
730	729	breq1d 4663	. . . . . . . . . . . . . . . . . 18
731	730	cbvralv 3171	. . . . . . . . . . . . . . . . 17 ..^ ..^
732	728, 731	sylib 208	. . . . . . . . . . . . . . . 16 ..^ $/\$ $/\$ ..^ ..^
733		rspa 2930	. . . . . . . . . . . . . . . 16 ..^ $/\$ ..^
734	732, 733	sylancom 701	. . . . . . . . . . . . . . 15 ..^ $/\$ $/\$ ..^
735	726, 709, 710, 734	syl21anc 1325	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^
736	695, 704, 722, 725, 735	fsumlt 14532	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ ..^ $/\$ ..^ ..^
737		fveq2 6191	. . . . . . . . . . . . . . . . . 18
738		oveq1 6657	. . . . . . . . . . . . . . . . . . 19
739	738	fveq2d 6195	. . . . . . . . . . . . . . . . . 18
740	737, 739	oveq12d 6668	. . . . . . . . . . . . . . . . 17
741	740	itgeq1d 40172	. . . . . . . . . . . . . . . 16
742	741	fveq2d 6195	. . . . . . . . . . . . . . 15
743	742	cbvsumv 14426	. . . . . . . . . . . . . 14 ..^ ..^
744	743	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ ..^ $/\$ ..^ ..^
745	349	rpcnd 11874	. . . . . . . . . . . . . . . . 17 $/\$
746		fsumconst 14522	. . . . . . . . . . . . . . . . 17 ..^ $/\$ ..^ ..^
747	503, 745, 746	sylancr 695	. . . . . . . . . . . . . . . 16 $/\$ ..^ ..^
748	346	nnnn0d 11351	. . . . . . . . . . . . . . . . . . 19
749		hashfzo0 13217	. . . . . . . . . . . . . . . . . . 19 ..^
750	748, 749	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
751	750	oveq1d 6665	. . . . . . . . . . . . . . . . 17 ..^
752	751	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^
753	345	rpcnd 11874	. . . . . . . . . . . . . . . . 17 $/\$
754	348	rpcnd 11874	. . . . . . . . . . . . . . . . 17 $/\$
755	348	rpne0d 11877	. . . . . . . . . . . . . . . . 17 $/\$
756	753, 754, 755	divcan2d 10803	. . . . . . . . . . . . . . . 16 $/\$
757	747, 752, 756	3eqtrd 2660	. . . . . . . . . . . . . . 15 $/\$ ..^
758	757	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ ..^
759	758	3ad2antl1 1223	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ ..^ $/\$ ..^
760	736, 744, 759	3brtr3d 4684	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ ..^ $/\$ ..^
761	682, 686, 689, 694, 760	lelttrd 10195	. . . . . . . . . . 11 $/\$ $/\$ $/\$ ..^ $/\$
762	761	ex 450	. . . . . . . . . 10 $/\$ $/\$ $/\$ ..^
763	516, 762	ralrimi 2957	. . . . . . . . 9 $/\$ $/\$ $/\$ ..^
764	763	3exp 1264	. . . . . . . 8 $/\$ ..^
765	764	adantr 481	. . . . . . 7 $/\$ $/\$ ..^ ..^
766	513, 765	reximdai 3012	. . . . . 6 $/\$ $/\$ ..^ ..^
767	510, 766	mpd 15	. . . . 5 $/\$ $/\$ ..^
768	509, 767	syldan 487	. . . 4 $/\$ $/\$ ..^
769	768	ex 450	. . 3 $/\$ ..^
770	769	ralimdva 2962	. 2 ..^
771	491, 770	mpd 15	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wtru 1484

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

wss 3574

c0 3915

cif 4086 class class class wbr 4653

cmpt 4729

cdm 5114

crn 5115

cres 5116

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cfn 7955

csup 8346 infcinf 8347

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cpnf 10071

cxr 10073

clt 10074

cle 10075

cmin 10266

cneg 10267

cdiv 10684

cn 11020

cn0 11292

cz 11377

cuz 11687

crp 11832

cioo 12175

cicc 12178

cfz 12326 ..^cfzo 12465

cfl 12591

chash 13117

cabs 13974

csu 14416

csin 14794

ccos 14795

ctopn 16082

ctg 16098 ℂ_fldccnfld 19746

ctop 20698

cnt 20821

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-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-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-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: fourierdlem103 40426 fourierdlem104 40427

W3C validator