fourierdlem103 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem103 40426

Description: The half lower part of the integral equal to the fourier partial sum, converges to half the left limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem103.f
fourierdlem103.xre
fourierdlem103.p	$/\$ $/\$ ..^
fourierdlem103.m
fourierdlem103.v
fourierdlem103.x
fourierdlem103.fcn	$/\$ ..^
fourierdlem103.fbdioo	$/\$ ..^
fourierdlem103.fdvcn	$/\$ ..^
fourierdlem103.fdvbd	$/\$ ..^
fourierdlem103.r	$/\$ ..^ lim
fourierdlem103.l	$/\$ ..^ lim
fourierdlem103.h
fourierdlem103.k
fourierdlem103.u
fourierdlem103.s
fourierdlem103.g
fourierdlem103.z
fourierdlem103.e
fourierdlem103.y	lim
fourierdlem103.w	lim
fourierdlem103.a	lim
fourierdlem103.b	lim
fourierdlem103.d
fourierdlem103.o
fourierdlem103.t
fourierdlem103.n
fourierdlem103.j
fourierdlem103.q
fourierdlem103.1	..^
fourierdlem103.ch	$/\$ $/\$ $/\$ $/\$ $/\$

**Assertion**
Ref	Expression
fourierdlem103

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem fourierdlem103 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3
2		1zzd 11408	. . 3
3		nfv 1843	. . . . 5
4		nfmpt1 4747	. . . . 5
5		nfmpt1 4747	. . . . 5
6		fourierdlem103.e	. . . . . 6
7		nfmpt1 4747	. . . . . 6
8	6, 7	nfcxfr 2762	. . . . 5
9		nnuz 11723	. . . . 5
10		pire 24210	. . . . . . . . . . . . . . . . 17
11	10	renegcli 10342	. . . . . . . . . . . . . . . 16
12	11	a1i 11	. . . . . . . . . . . . . . 15 $/\$
13		elioore 12205	. . . . . . . . . . . . . . . 16
14	13	adantl 482	. . . . . . . . . . . . . . 15 $/\$
15		fourierdlem103.f	. . . . . . . . . . . . . . . . . . . 20
16		fourierdlem103.xre	. . . . . . . . . . . . . . . . . . . 20
17		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . 23
18	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
19	15, 18	fssresd 6071	. . . . . . . . . . . . . . . . . . . . 21
20		ioosscn 39716	. . . . . . . . . . . . . . . . . . . . . 22
21	20	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
22		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ℂ_fld
23		pnfxr 10092	. . . . . . . . . . . . . . . . . . . . . . 23
24	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
25	16	ltpnfd 11955	. . . . . . . . . . . . . . . . . . . . . 22
26	22, 24, 16, 25	lptioo1cn 39878	. . . . . . . . . . . . . . . . . . . . 21 ℂ_fld
27		fourierdlem103.y	. . . . . . . . . . . . . . . . . . . . 21 lim
28	19, 21, 26, 27	limcrecl 39861	. . . . . . . . . . . . . . . . . . . 20
29		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . 23
30	29	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
31	15, 30	fssresd 6071	. . . . . . . . . . . . . . . . . . . . 21
32		ioosscn 39716	. . . . . . . . . . . . . . . . . . . . . 22
33	32	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
34		mnfxr 10096	. . . . . . . . . . . . . . . . . . . . . . 23
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
36	16	mnfltd 11958	. . . . . . . . . . . . . . . . . . . . . 22
37	22, 35, 16, 36	lptioo2cn 39877	. . . . . . . . . . . . . . . . . . . . 21 ℂ_fld
38		fourierdlem103.w	. . . . . . . . . . . . . . . . . . . . 21 lim
39	31, 33, 37, 38	limcrecl 39861	. . . . . . . . . . . . . . . . . . . 20
40		fourierdlem103.h	. . . . . . . . . . . . . . . . . . . 20
41		fourierdlem103.k	. . . . . . . . . . . . . . . . . . . 20
42		fourierdlem103.u	. . . . . . . . . . . . . . . . . . . 20
43	15, 16, 28, 39, 40, 41, 42	fourierdlem55 40378	. . . . . . . . . . . . . . . . . . 19
44		ax-resscn 9993	. . . . . . . . . . . . . . . . . . . 20
45	44	a1i 11	. . . . . . . . . . . . . . . . . . 19
46	43, 45	fssd 6057	. . . . . . . . . . . . . . . . . 18
47	46	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
48	11	a1i 11	. . . . . . . . . . . . . . . . . . 19
49	10	a1i 11	. . . . . . . . . . . . . . . . . . 19
50	48	leidd 10594	. . . . . . . . . . . . . . . . . . 19
51		0red 10041	. . . . . . . . . . . . . . . . . . . . 21
52	11	rexri 10097	. . . . . . . . . . . . . . . . . . . . . 22
53		0xr 10086	. . . . . . . . . . . . . . . . . . . . . 22
54		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
55	52, 53, 54	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . 21
56		pipos 24212	. . . . . . . . . . . . . . . . . . . . . 22
57	56	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
58	13, 51, 49, 55, 57	lttrd 10198	. . . . . . . . . . . . . . . . . . . 20
59	13, 49, 58	ltled 10185	. . . . . . . . . . . . . . . . . . 19
60		iccss 12241	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
61	48, 49, 50, 59, 60	syl22anc 1327	. . . . . . . . . . . . . . . . . 18
62	61	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
63	47, 62	fssresd 6071	. . . . . . . . . . . . . . . 16 $/\$
64		fourierdlem103.o	. . . . . . . . . . . . . . . . . 18
65	64	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
66	65	feq1d 6030	. . . . . . . . . . . . . . . 16 $/\$
67	63, 66	mpbird 247	. . . . . . . . . . . . . . 15 $/\$
68		fourierdlem103.n	. . . . . . . . . . . . . . . . . . 19
69	11	elexi 3213	. . . . . . . . . . . . . . . . . . . . . . . . . 26
70	69	prid1 4297	. . . . . . . . . . . . . . . . . . . . . . . . 25
71		elun1 3780	. . . . . . . . . . . . . . . . . . . . . . . . 25
72	70, 71	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24
73		fourierdlem103.t	. . . . . . . . . . . . . . . . . . . . . . . 24
74	72, 73	eleqtrri 2700	. . . . . . . . . . . . . . . . . . . . . . 23
75	74	ne0ii 3923	. . . . . . . . . . . . . . . . . . . . . 22
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
77		prfi 8235	. . . . . . . . . . . . . . . . . . . . . . . . 25
78	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
79		fzfi 12771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
80		fourierdlem103.q	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
81	80	rnmptfi 39351	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
82	79, 81	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26
83	82	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
84		infi 8184	. . . . . . . . . . . . . . . . . . . . . . . . 25
85	83, 84	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
86		unfi 8227	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
87	78, 85, 86	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23
88	73, 87	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . . . 22
89		hashnncl 13157	. . . . . . . . . . . . . . . . . . . . . 22
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . . . . 21
91	76, 90	mpbird 247	. . . . . . . . . . . . . . . . . . . 20
92		nnm1nn0 11334	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	syl 17	. . . . . . . . . . . . . . . . . . 19
94	68, 93	syl5eqel 2705	. . . . . . . . . . . . . . . . . 18
95	94	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
96		0red 10041	. . . . . . . . . . . . . . . . . . 19 $/\$
97		1red 10055	. . . . . . . . . . . . . . . . . . 19 $/\$
98	95	nn0red 11352	. . . . . . . . . . . . . . . . . . 19 $/\$
99		0lt1 10550	. . . . . . . . . . . . . . . . . . . 20
100	99	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
101		2re 11090	. . . . . . . . . . . . . . . . . . . . . 22
102	101	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
103	91	nnred 11035	. . . . . . . . . . . . . . . . . . . . . 22
104	103	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
105		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
106	52, 53, 105	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . . 26
107	48, 106	ltned 10173	. . . . . . . . . . . . . . . . . . . . . . . . 25
108	107	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
109		hashprg 13182	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
110	12, 14, 109	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
111	108, 110	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
112	111	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113	88	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
114		ssun1 3776	. . . . . . . . . . . . . . . . . . . . . . . 24
115	114, 73	sseqtr4i 3638	. . . . . . . . . . . . . . . . . . . . . . 23
116		hashssle 39512	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
117	113, 115, 116	sylancl 694	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
118	112, 117	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . 21 $/\$
119	102, 104, 97, 118	lesub1dd 10643	. . . . . . . . . . . . . . . . . . . 20 $/\$
120		1e2m1 11136	. . . . . . . . . . . . . . . . . . . 20
121	119, 120, 68	3brtr4g 4687	. . . . . . . . . . . . . . . . . . 19 $/\$
122	96, 97, 98, 100, 121	ltletrd 10197	. . . . . . . . . . . . . . . . . 18 $/\$
123	122	gt0ne0d 10592	. . . . . . . . . . . . . . . . 17 $/\$
124	95, 123	jca 554	. . . . . . . . . . . . . . . 16 $/\$ $/\$
125		elnnne0 11306	. . . . . . . . . . . . . . . 16 $/\$
126	124, 125	sylibr 224	. . . . . . . . . . . . . . 15 $/\$
127		fourierdlem103.j	. . . . . . . . . . . . . . . . . 18
128	50	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
129	48, 13, 106	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . 24
130	129	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
131	12, 14, 12, 128, 130	eliccd 39726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
132	14	leidd 10594	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
133	12, 14, 14, 130, 132	eliccd 39726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	131, 133	jca 554	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
135		vex 3203	. . . . . . . . . . . . . . . . . . . . . 22
136	69, 135	prss 4351	. . . . . . . . . . . . . . . . . . . . 21 $/\$
137	134, 136	sylib 208	. . . . . . . . . . . . . . . . . . . 20 $/\$
138		inss2 3834	. . . . . . . . . . . . . . . . . . . . . 22
139	138	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
140		ioossicc 12259	. . . . . . . . . . . . . . . . . . . . 21
141	139, 140	syl6ss 3615	. . . . . . . . . . . . . . . . . . . 20 $/\$
142	137, 141	unssd 3789	. . . . . . . . . . . . . . . . . . 19 $/\$
143	73, 142	syl5eqss 3649	. . . . . . . . . . . . . . . . . 18 $/\$
144	74	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$
145	135	prid2 4298	. . . . . . . . . . . . . . . . . . . . 21
146		elun1 3780	. . . . . . . . . . . . . . . . . . . . 21
147	145, 146	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
148	147, 73	eleqtrri 2700	. . . . . . . . . . . . . . . . . . 19
149	148	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$
150	113, 68, 127, 12, 14, 143, 144, 149	fourierdlem52 40375	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
151	150	simpld 475	. . . . . . . . . . . . . . . 16 $/\$ $/\$
152	151	simpld 475	. . . . . . . . . . . . . . 15 $/\$
153	151	simprd 479	. . . . . . . . . . . . . . 15 $/\$
154	150	simprd 479	. . . . . . . . . . . . . . 15 $/\$
155		elfzoelz 12470	. . . . . . . . . . . . . . . . . . 19 ..^
156	155	zred 11482	. . . . . . . . . . . . . . . . . 18 ..^
157	156	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
158	157	ltp1d 10954	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
159	48, 13	jca 554	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
160	69, 135	prss 4351	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
161	159, 160	sylib 208	. . . . . . . . . . . . . . . . . . . . . 22
162	161	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
163		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . 23
164	138, 163	sstri 3612	. . . . . . . . . . . . . . . . . . . . . 22
165	164	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	162, 165	unssd 3789	. . . . . . . . . . . . . . . . . . . 20 $/\$
167	73, 166	syl5eqss 3649	. . . . . . . . . . . . . . . . . . 19 $/\$
168	113, 167, 127, 68	fourierdlem36 40360	. . . . . . . . . . . . . . . . . 18 $/\$
169	168	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
170		elfzofz 12485	. . . . . . . . . . . . . . . . . 18 ..^
171	170	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
172		fzofzp1 12565	. . . . . . . . . . . . . . . . . 18 ..^
173	172	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
174		isorel 6576	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
175	169, 171, 173, 174	syl12anc 1324	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
176	158, 175	mpbid 222	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^
177	43	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
178	177, 62	feqresmpt 6250	. . . . . . . . . . . . . . . . . . 19 $/\$
179	62	sselda 3603	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
180	15, 16, 28, 39, 40	fourierdlem9 40333	. . . . . . . . . . . . . . . . . . . . . . . . 25
181	180	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
182	181, 179	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
183	41	fourierdlem43 40367	. . . . . . . . . . . . . . . . . . . . . . . . 25
184	183	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
185	184, 179	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
186	182, 185	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
187	42	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
188	179, 186, 187	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
189	11	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
190	13	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
191		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
192		eliccre 39728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
193	189, 190, 191, 192	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
194		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
195	52	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
196	190	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
197		iccleub 12229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
198	195, 196, 191, 197	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
199	55	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
200	193, 190, 194, 198, 199	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
201	193, 200	ltned 10173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
202	201	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
203	202	neneqd 2799	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
204	203	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
205	193, 194, 200	ltnsymd 10186	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
206	205	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
207	206	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
208	207	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
209	208	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
210	204, 209	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
211	15	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
212	16	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
213		iccssre 12255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
214	11, 10, 213	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
215	214, 179	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
216	212, 215	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
217	211, 216	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
218	39	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
219	217, 218	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
220	219, 215, 202	redivcld 10853	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
221	210, 220	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
222	40	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
223	179, 221, 222	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
224	223, 204, 209	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
225	10	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
226	225	renegcld 10457	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
227		iccgelb 12230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
228	195, 196, 191, 227	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
229	58	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
230	193, 190, 225, 198, 229	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
231	193, 225, 230	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
232	226, 225, 193, 228, 231	eliccd 39726	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
233	201	neneqd 2799	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
234	233	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
235	101	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
236	193	rehalfcld 11279	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
237	236	resincld 14873	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
238	235, 237	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
239		2cn 11091	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
240	239	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
241	193	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
242	241	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
243	242	sincld 14860	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
244		2ne0 11113	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
245	244	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
246		fourierdlem44 40368	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
247	232, 201, 246	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
248	240, 243, 245, 247	mulne0d 10679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
249	193, 238, 248	redivcld 10853	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
250	234, 249	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
251	41	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
252	232, 250, 251	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
253	252	adantll 750	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
254	224, 253	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
255	203	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
256	255	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
257	188, 254, 256	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
258	257	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19 $/\$
259	65, 178, 258	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18 $/\$
260	259	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
261	260	reseq1d 5395	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
262	15	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
263	16	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
264		fourierdlem103.p	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
265		fourierdlem103.m	. . . . . . . . . . . . . . . . . . 19
266	265	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
267		fourierdlem103.v	. . . . . . . . . . . . . . . . . . 19
268	267	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
269		fourierdlem103.fcn	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
270	269	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
271		fourierdlem103.r	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ lim
272	271	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^ lim
273		fourierdlem103.l	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ lim
274	273	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^ lim
275	106	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
276	52	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
277	53	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
278	55	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
279	276, 14, 277, 278	gtnelicc 39722	. . . . . . . . . . . . . . . . . 18 $/\$
280	39	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
281		eqid 2622	. . . . . . . . . . . . . . . . . 18
282		eqid 2622	. . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
283		eqid 2622	. . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
284		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
285		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
286	285	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21
287	284, 286	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20
288	287	sseq2d 3633	. . . . . . . . . . . . . . . . . . 19
289	288	cbvriotav 6622	. . . . . . . . . . . . . . . . . 18 ..^ ..^
290	262, 263, 264, 266, 268, 270, 272, 274, 12, 14, 275, 62, 279, 280, 281, 80, 73, 68, 127, 282, 283, 289	fourierdlem86 40409	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^ ..^ ..^ lim $/\$ ..^ ..^ lim $/\$
291	290	simprd 479	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
292	261, 291	eqeltrd 2701	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^
293	290	simpld 475	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^ ..^ ..^ lim $/\$ ..^ ..^ lim
294	293	simpld 475	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^ ..^ ..^ lim
295	260	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
296	295	reseq1d 5395	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
297	296	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^ lim lim
298	294, 297	eleqtrd 2703	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^ ..^ ..^ lim
299	293	simprd 479	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^ ..^ ..^ lim
300	296	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^ lim lim
301	299, 300	eleqtrd 2703	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^ ..^ ..^ lim
302		eqid 2622	. . . . . . . . . . . . . . 15
303	67	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
304	11	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
305	14	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
306		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . 24
307	306	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
308	62, 214	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
309	308	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
310	152	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
311	310, 171	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
312	309, 311	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^
313	312	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
314	52	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
315	14	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
316	315	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
317		iccgelb 12230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
318	314, 316, 311, 317	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^
319	318	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
320	313	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^ $/\$
321	310, 173	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ ..^
322	309, 321	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
323	322	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
324	323	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^ $/\$
325		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^ $/\$
326		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
327	320, 324, 325, 326	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
328	304, 313, 307, 319, 327	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$
329	304, 307, 328	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
330	322	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
331		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
332	320, 324, 325, 331	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
333		iccleub 12229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
334	314, 316, 321, 333	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^
335	334	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
336	307, 330, 305, 332, 335	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$
337	307, 305, 336	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
338	304, 305, 307, 329, 337	eliccd 39726	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
339	338	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^
340		dfss3 3592	. . . . . . . . . . . . . . . . . . . . 21
341	339, 340	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
342	303, 341	feqresmpt 6250	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
343		simplll 798	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
344		simpllr 799	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
345	64	fveq1i 6192	. . . . . . . . . . . . . . . . . . . . . . . 24
346	345	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
347		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . . 24
348	347	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
349	253, 255	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
350	224, 349	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
351	219	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
352	241	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
353	239	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
354	352	halfcld 11277	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
355	354	sincld 14860	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
356	353, 355	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
357	248	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
358	351, 352, 356, 202, 357	dmdcan2d 10831	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
359	188, 350, 358	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
360	346, 348, 359	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
361	343, 344, 338, 360	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
362	343, 344, 338, 358	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
363	362	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
364		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
365		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
366	365	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
367	366	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
368		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
369	367, 368	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . 26
370	369	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
371		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
372		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . 26
373	372	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
374	364, 370, 371, 373	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
375		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
376		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
377	376	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
378	377	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
379	368, 378	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . 26
380	379	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
381		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . 26
382	381	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
383	375, 380, 371, 382	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
384	374, 383	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
385	384	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
386	385	adantllr 755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
387	361, 363, 386	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^ $/\$
388	387	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
389	342, 388	eqtr2d 2657	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
390	389	oveq2d 6666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
391	44	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
392	341, 309	sstrd 3613	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
393	22	tgioo2 22606	. . . . . . . . . . . . . . . . . . 19 ℂ_fld ↾_t
394	22, 393	dvres 23675	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
395	391, 303, 309, 392, 394	syl22anc 1327	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
396		ioontr 39736	. . . . . . . . . . . . . . . . . . 19
397	396	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
398	397	reseq2d 5396	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
399	390, 395, 398	3eqtrrd 2661	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
400	15	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
401	16	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
402	265	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
403	267	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
404		fourierdlem103.fdvcn	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
405	404	ad4ant14 1293	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^ $/\$ ..^
406	62	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
407	341, 406	sstrd 3613	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
408	312	rexrd 10089	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
409	53	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
410		0red 10041	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
411	55	ad2antlr 763	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
412	322, 315, 410, 334, 411	lelttrd 10195	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
413	408, 322, 409, 412	gtnelicc 39722	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
414	39	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
415	11	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
416	106	ad2antlr 763	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
417		simpr 477	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^ ..^
418		biid 251	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^ $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$ ..^ $/\$ $/\$ ..^ $/\$
419	401, 264, 402, 403, 415, 315, 416, 406, 80, 73, 68, 127, 417, 289, 418	fourierdlem50 40373	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^ ..^ ..^ $/\$ ..^ ..^
420	419	simpld 475	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^ ..^ ..^
421	419	simprd 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^ ..^ ..^
422	369	cbvmptv 4750	. . . . . . . . . . . . . . . . 17
423	379	cbvmptv 4750	. . . . . . . . . . . . . . . . 17
424		eqid 2622	. . . . . . . . . . . . . . . . 17
425	400, 401, 264, 402, 403, 405, 312, 322, 176, 407, 413, 414, 80, 420, 421, 422, 423, 424	fourierdlem72 40395	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
426	399, 425	eqeltrd 2701	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^
427		eqid 2622	. . . . . . . . . . . . . . . . 17
428		eqid 2622	. . . . . . . . . . . . . . . . 17
429		fourierdlem103.1	. . . . . . . . . . . . . . . . . . . 20 ..^
430	429, 420	syl5eqel 2705	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^ ..^
431		simpll 790	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
432	431, 430	jca 554	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^ $/\$ ..^
433		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
434	433	anbi2d 740	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ ..^
435		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
436		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25
437	436	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . 24
438	435, 437	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . 23
439		raleq 3138	. . . . . . . . . . . . . . . . . . . . . . 23
440	438, 439	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
441	440	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . 21
442	434, 441	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ ..^
443		fourierdlem103.fbdioo	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
444	442, 443	vtoclg 3266	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ ..^
445	430, 432, 444	sylc 65	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
446		nfv 1843	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^
447		nfra1 2941	. . . . . . . . . . . . . . . . . . . . . 22
448	446, 447	nfan 1828	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
449		simplr 792	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$ $/\$
450	11	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
451	450, 16	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
452	10	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
453	452, 16	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
454	451, 453	iccssred 39727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
455		ressxr 10083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
456	454, 455	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
457	456	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
458	264, 402, 403	fourierdlem15 40339	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
459		elfzofz 12485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
460	430, 459	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
461	458, 460	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
462	457, 461	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^
463	462	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
464		fzofzp1 12565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^
465	430, 464	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
466	458, 465	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
467	457, 466	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^
468	467	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
469		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . 26
470	469	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
471	10	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ ..^
472	415, 471, 401, 264, 402, 403, 460, 80	fourierdlem13 40337	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^ $/\$
473	472	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
474	473	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^ $/\$
475	454	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ ..^
476	475, 461	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ ..^
477	476	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^ $/\$
478	474, 477	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^ $/\$
479	401, 312	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
480	479	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^ $/\$
481	472	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ ..^
482	476, 401	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ ..^
483	481, 482	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ ..^
484	415, 471, 401, 264, 402, 403, 465, 80	fourierdlem13 40337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ ..^ $/\$
485	484	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ ..^
486	475, 466	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ ..^
487	486, 401	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ ..^
488	485, 487	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ ..^
489	429	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
490	489	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
491	489	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^
492	491	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^
493	490, 492	oveq12i 6662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ ..^
494	421, 493	syl6sseq 3651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ ..^
495	483, 488, 312, 322, 176, 494	fourierdlem10 40334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ ..^ $/\$
496	495	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ ..^
497	483, 312, 401, 496	leadd2dd 10642	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
498	497	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^ $/\$
499	480	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^ $/\$
500	401, 322	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ ..^
501	500	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ ..^
502	501	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^ $/\$
503		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^ $/\$
504		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
505	499, 502, 503, 504	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^ $/\$
506	478, 480, 470, 498, 505	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^ $/\$
507	474, 506	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
508	500	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^ $/\$
509	484	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ ..^
510	509, 486	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
511	510	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^ $/\$
512		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
513	499, 502, 503, 512	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^ $/\$
514	495	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ ..^
515	322, 488, 401, 514	leadd2dd 10642	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
516	515	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^ $/\$
517	470, 508, 511, 513, 516	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^ $/\$
518	509	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
519	518	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^ $/\$
520	517, 519	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
521	463, 468, 470, 507, 520	eliood 39720	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$
522	521	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$ $/\$
523		rspa 2930	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
524	449, 522, 523	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$ $/\$
525	524	ex 450	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
526	448, 525	ralrimi 2957	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^ $/\$
527	526	ex 450	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
528	527	reximdv 3016	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
529	445, 528	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
530	438	raleqdv 3144	. . . . . . . . . . . . . . . . . . . . . 22
531	530	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . 21
532	434, 531	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ ..^
533		fourierdlem103.fdvbd	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
534	532, 533	vtoclg 3266	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ ..^
535	430, 432, 534	sylc 65	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
536		nfra1 2941	. . . . . . . . . . . . . . . . . . . . . 22
537	446, 536	nfan 1828	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
538	15, 45	fssd 6057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
539		ssid 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
540	539	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
541		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
542	541	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
543	22, 393	dvres 23675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
544	45, 538, 540, 542, 543	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
545		ioontr 39736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
546	545	reseq2i 5393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
547	546	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
548	544, 547	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
549	548	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
550		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
551	549, 550	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
552	551	ad4ant14 1293	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
553	552	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$
554	553	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$ $/\$
555		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$ $/\$
556	521	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$ $/\$
557		rspa 2930	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
558	555, 556, 557	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$ $/\$
559	554, 558	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$ $/\$
560	559	ex 450	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
561	537, 560	ralrimi 2957	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^ $/\$
562	561	ex 450	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
563	562	reximdv 3016	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
564	535, 563	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
565	415	rexrd 10089	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
566	565, 316, 310, 417	fourierdlem8 40332	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
567	126	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
568	152, 308	fssd 6057	. . . . . . . . . . . . . . . . . . 19 $/\$
569	568	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
570		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
571	153	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
572	154	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
573	571, 572	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . 21 $/\$
574	573	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
575	570, 574	eleqtrd 2703	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
576	575	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
577		simpr 477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
578		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
579	578	breq1d 4663	. . . . . . . . . . . . . . . . . . . 20
580	579	cbvrabv 3199	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
581	580	supeq1i 8353	. . . . . . . . . . . . . . . . . 18 ..^ ..^
582	567, 569, 576, 577, 581	fourierdlem25 40349	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ ..^
583	546	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
584	538	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
585	539	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
586	541	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
587	391, 584, 585, 586, 543	syl22anc 1327	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
588	521	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^
589		dfss3 3592	. . . . . . . . . . . . . . . . . . . . 21
590	588, 589	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
591	590	resabs1d 5428	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
592	583, 587, 591	3eqtr4rd 2667	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
593		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ ..^
594		id 22	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ ..^
595	438	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . . . 24
596	595, 438	feq12d 6033	. . . . . . . . . . . . . . . . . . . . . . 23
597	434, 596	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ ..^
598		cncff 22696	. . . . . . . . . . . . . . . . . . . . . . 23
599	404, 598	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^
600	597, 599	vtoclg 3266	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ ..^
601	593, 594, 600	sylc 65	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
602	432, 601	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
603	602, 590	fssresd 6071	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
604	592, 603	feq1dd 39347	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
605	367, 378	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
606	605	cbvmptv 4750	. . . . . . . . . . . . . . . . 17
607		biid 251	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$
608		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
609	608	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21
610	609	breq1d 4663	. . . . . . . . . . . . . . . . . . . 20
611	610	cbvralv 3171	. . . . . . . . . . . . . . . . . . 19
612	607, 611	anbi12i 733	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
613		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
614	613	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
615	614	breq1d 4663	. . . . . . . . . . . . . . . . . . 19
616	615	cbvralv 3171	. . . . . . . . . . . . . . . . . 18
617	612, 616	anbi12i 733	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ $/\$ $/\$
618	262, 263, 12, 14, 62, 279, 280, 427, 428, 529, 564, 152, 176, 566, 582, 604, 606, 617	fourierdlem80 40403	. . . . . . . . . . . . . . . 16 $/\$
619	358	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
620	259, 619	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$
621	620	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 $/\$
622	621	dmeqd 5326	. . . . . . . . . . . . . . . . . . 19 $/\$
623		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20
624		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . 22
625		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . 22
626		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . . 22
627	624, 625, 626	nfov 6676	. . . . . . . . . . . . . . . . . . . . 21
628	627	nfdm 5367	. . . . . . . . . . . . . . . . . . . 20
629	623, 628	raleqf 3134	. . . . . . . . . . . . . . . . . . 19
630	622, 629	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$
631	621	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21 $/\$
632	631	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 $/\$
633	632	breq1d 4663	. . . . . . . . . . . . . . . . . . 19 $/\$
634	633	ralbidv 2986	. . . . . . . . . . . . . . . . . 18 $/\$
635	630, 634	bitrd 268	. . . . . . . . . . . . . . . . 17 $/\$
636	635	rexbidv 3052	. . . . . . . . . . . . . . . 16 $/\$
637	618, 636	mpbird 247	. . . . . . . . . . . . . . 15 $/\$
638		eqid 2622	. . . . . . . . . . . . . . 15
639		eqeq1 2626	. . . . . . . . . . . . . . . . 17
640		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
641		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
642	641	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
643	640, 642	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
644	643	sseq2d 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
645	644	cbvriotav 6622	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
646	645	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
647	646	eqeq2i 2634	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
648	647	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
649		csbeq1 3536	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^ ..^ ..^
650	645, 649	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
651	650	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^
652	648, 651	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^ ..^ ..^
653	652	trud 1493	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^ ..^ ..^
654	653	oveq1i 6660	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^ ..^ ..^
655	654	oveq1i 6660	. . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^ ..^
656	655	oveq1i 6660	. . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
657	656	a1i 11	. . . . . . . . . . . . . . . . 17 ..^ ..^ ..^ ..^
658		eqeq1 2626	. . . . . . . . . . . . . . . . . 18
659	645	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^ ..^
660	659	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^
661	660	eqeq2i 2634	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
662	661	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
663		csbeq1 3536	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ..^ ..^ ..^ ..^
664	645, 663	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^ ..^
665	664	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
666	662, 665	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ ..^ ..^ ..^
667	666	trud 1493	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^ ..^ ..^
668	667	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . 21 ..^ ..^ ..^ ..^
669	668	oveq1i 6660	. . . . . . . . . . . . . . . . . . . 20 ..^ ..^ ..^ ..^
670	669	oveq1i 6660	. . . . . . . . . . . . . . . . . . 19 ..^ ..^ ..^ ..^
671	670	a1i 11	. . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
672		fveq2 6191	. . . . . . . . . . . . . . . . . 18
673	658, 671, 672	ifeq123d 39207	. . . . . . . . . . . . . . . . 17 ..^ ..^ ..^ ..^
674	639, 657, 673	ifeq123d 39207	. . . . . . . . . . . . . . . 16 ..^ ..^ ..^ ..^ ..^ ..^ ..^ ..^
675	674	cbvmptv 4750	. . . . . . . . . . . . . . 15 ..^ ..^ ..^ ..^ ..^ ..^ ..^ ..^
676	12, 14, 67, 126, 152, 153, 154, 176, 292, 298, 301, 302, 426, 637, 638, 675	fourierdlem73 40396	. . . . . . . . . . . . . 14 $/\$
677		breq2 4657	. . . . . . . . . . . . . . . 16
678	677	rexralbidv 3058	. . . . . . . . . . . . . . 15
679	678	cbvralv 3171	. . . . . . . . . . . . . 14
680	676, 679	sylib 208	. . . . . . . . . . . . 13 $/\$
681	680	adantlr 751	. . . . . . . . . . . 12 $/\$ $/\$
682		rphalfcl 11858	. . . . . . . . . . . . 13
683	682	ad2antlr 763	. . . . . . . . . . . 12 $/\$ $/\$
684		breq2 4657	. . . . . . . . . . . . . 14
685	684	rexralbidv 3058	. . . . . . . . . . . . 13
686	685	rspccva 3308	. . . . . . . . . . . 12 $/\$
687	681, 683, 686	syl2anc 693	. . . . . . . . . . 11 $/\$ $/\$
688	345	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
689	140	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
690	689	sselda 3603	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
691	690, 347	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
692	688, 691	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
693	692	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
694	693	itgeq2dv 23548	. . . . . . . . . . . . . . . . . 18 $/\$
695	694	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
696	695	fveq2d 6195	. . . . . . . . . . . . . . . 16 $/\$ $/\$
697		simpr 477	. . . . . . . . . . . . . . . 16 $/\$ $/\$
698	696, 697	eqbrtrd 4675	. . . . . . . . . . . . . . 15 $/\$ $/\$
699	698	ex 450	. . . . . . . . . . . . . 14 $/\$
700	699	adantlr 751	. . . . . . . . . . . . 13 $/\$ $/\$
701	700	ralimdv 2963	. . . . . . . . . . . 12 $/\$ $/\$
702	701	reximdv 3016	. . . . . . . . . . 11 $/\$ $/\$
703	687, 702	mpd 15	. . . . . . . . . 10 $/\$ $/\$
704	703	adantr 481	. . . . . . . . 9 $/\$ $/\$ $/\$
705		nfv 1843	. . . . . . . . . . . . . . 15 $/\$ $/\$
706		nfra1 2941	. . . . . . . . . . . . . . 15
707	705, 706	nfan 1828	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
708		nfv 1843	. . . . . . . . . . . . . 14
709	707, 708	nfan 1828	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
710		nfv 1843	. . . . . . . . . . . . 13
711	709, 710	nfan 1828	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
712		simpll 790	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
713		eluznn 11758	. . . . . . . . . . . . . . . . . . . . 21 $/\$
714	713	adantll 750	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
715	712, 714	jca 554	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
716	715	adantllr 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
717		simpllr 799	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
718	713	adantll 750	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
719		rspa 2930	. . . . . . . . . . . . . . . . . . 19 $/\$
720	717, 718, 719	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
721	716, 720	jca 554	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
722	721	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
723		nnre 11027	. . . . . . . . . . . . . . . . . . . . . 22
724	723	rexrd 10089	. . . . . . . . . . . . . . . . . . . . 21
725	724	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
726	23	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
727		eluzelre 11698	. . . . . . . . . . . . . . . . . . . . . 22
728		1re 10039	. . . . . . . . . . . . . . . . . . . . . . . 24
729	728	rehalfcli 11281	. . . . . . . . . . . . . . . . . . . . . . 23
730	729	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
731	727, 730	readdcld 10069	. . . . . . . . . . . . . . . . . . . . 21
732	731	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
733	723	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
734	727	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
735		eluzle 11700	. . . . . . . . . . . . . . . . . . . . . 22
736	735	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
737		halfgt0 11248	. . . . . . . . . . . . . . . . . . . . . . 23
738	737	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
739	729	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
740	739, 734	ltaddposd 10611	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
741	738, 740	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 $/\$
742	733, 734, 732, 736, 741	lelttrd 10195	. . . . . . . . . . . . . . . . . . . 20 $/\$
743	732	ltpnfd 11955	. . . . . . . . . . . . . . . . . . . 20 $/\$
744	725, 726, 732, 742, 743	eliood 39720	. . . . . . . . . . . . . . . . . . 19 $/\$
745	744	adantlr 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
746		simplr 792	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
747		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25
748	747	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . 24
749	748	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23
750	749	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
751	750	itgeq2dv 23548	. . . . . . . . . . . . . . . . . . . . 21
752	751	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
753	752	breq1d 4663	. . . . . . . . . . . . . . . . . . 19
754	753	rspcv 3305	. . . . . . . . . . . . . . . . . 18
755	745, 746, 754	sylc 65	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
756	755	adantlll 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
757	722, 756	jca 554	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
758		fourierdlem103.ch	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
759	757, 758	sylibr 224	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
760	11	a1i 11	. . . . . . . . . . . . . . . . . 18
761		0red 10041	. . . . . . . . . . . . . . . . . 18
762		ioossicc 12259	. . . . . . . . . . . . . . . . . . 19
763	758	biimpi 206	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
764		simp-4r 807	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
765	763, 764	syl 17	. . . . . . . . . . . . . . . . . . 19
766	762, 765	sseldi 3601	. . . . . . . . . . . . . . . . . 18
767		simp-5l 808	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
768	763, 767	syl 17	. . . . . . . . . . . . . . . . . . . . 21
769	43	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
770	10	rexri 10097	. . . . . . . . . . . . . . . . . . . . . . . . . 26
771		0re 10040	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
772	771, 10, 56	ltleii 10160	. . . . . . . . . . . . . . . . . . . . . . . . . 26
773		iooss2 12211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
774	770, 772, 773	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . 25
775		ioossicc 12259	. . . . . . . . . . . . . . . . . . . . . . . . 25
776	774, 775	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . . 24
777	776	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . 23
778	777	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
779	769, 778	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . 21 $/\$
780	768, 779	sylan 488	. . . . . . . . . . . . . . . . . . . 20 $/\$
781		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
782	763, 781	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
783	782	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . . 24
784	729	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
785	783, 784	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . 23
786	785	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
787		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . 23
788	787	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
789	786, 788	remulcld 10070	. . . . . . . . . . . . . . . . . . . . 21 $/\$
790	789	resincld 14873	. . . . . . . . . . . . . . . . . . . 20 $/\$
791	780, 790	remulcld 10070	. . . . . . . . . . . . . . . . . . 19 $/\$
792	791	recnd 10068	. . . . . . . . . . . . . . . . . 18 $/\$
793	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20
794	53	a1i 11	. . . . . . . . . . . . . . . . . . . 20
795	760	leidd 10594	. . . . . . . . . . . . . . . . . . . 20
796		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . 22
797	796, 765	sseldi 3601	. . . . . . . . . . . . . . . . . . . . 21
798	793, 794, 765, 54	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21
799	797, 761, 798	ltled 10185	. . . . . . . . . . . . . . . . . . . 20
800		ioossioo 12265	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
801	793, 794, 795, 799, 800	syl22anc 1327	. . . . . . . . . . . . . . . . . . 19
802		ioombl 23333	. . . . . . . . . . . . . . . . . . . 20
803	802	a1i 11	. . . . . . . . . . . . . . . . . . 19
804		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . 23
805	804	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
806		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
807	806	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
808	807	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
809	808	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
810	809	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
811	810	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . 23
812	811	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . 22
813	805, 812	imbi12d 334	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
814	776	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
815		ioombl 23333	. . . . . . . . . . . . . . . . . . . . . . 23
816	815	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
817	43	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
818	817	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
819		nnre 11027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
820		readdcl 10019	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
821	819, 729, 820	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
822	821	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
823		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
824	214, 823	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
825	822, 824	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
826	825	resincld 14873	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
827	826	adantll 750	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
828	818, 827	remulcld 10070	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
829		fourierdlem103.g	. . . . . . . . . . . . . . . . . . . . . . . . 25
830	829	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
831		fourierdlem103.s	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
832	831	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
833	823, 826, 832	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
834	833	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
835	834	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
836	835	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
837	830, 836	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
838	15	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
839		fourierdlem103.x	. . . . . . . . . . . . . . . . . . . . . . . . 25
840	839	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
841	27	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ lim
842	38	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ lim
843	819	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
844	265	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
845	267	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
846	269	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^
847	271	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ lim
848	273	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ lim
849		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$ $/\$ ..^
850		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
851	599	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^
852		fourierdlem103.a	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim
853	852	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ lim
854		fourierdlem103.b	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim
855	854	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ lim
856	264, 838, 840, 841, 842, 40, 41, 42, 843, 831, 829, 844, 845, 846, 847, 848, 80, 849, 850, 851, 853, 855	fourierdlem88 40411	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
857	837, 856	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
858	814, 816, 828, 857	iblss 23571	. . . . . . . . . . . . . . . . . . . . 21 $/\$
859	813, 858	chvarv 2263	. . . . . . . . . . . . . . . . . . . 20 $/\$
860	768, 782, 859	syl2anc 693	. . . . . . . . . . . . . . . . . . 19
861	801, 803, 791, 860	iblss 23571	. . . . . . . . . . . . . . . . . 18
862	765, 106	syl 17	. . . . . . . . . . . . . . . . . . . . 21
863	760, 797, 862	ltled 10185	. . . . . . . . . . . . . . . . . . . 20
864	761	leidd 10594	. . . . . . . . . . . . . . . . . . . 20
865		ioossioo 12265	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
866	793, 794, 863, 864, 865	syl22anc 1327	. . . . . . . . . . . . . . . . . . 19
867		ioombl 23333	. . . . . . . . . . . . . . . . . . . 20
868	867	a1i 11	. . . . . . . . . . . . . . . . . . 19
869	866, 868, 791, 860	iblss 23571	. . . . . . . . . . . . . . . . . 18
870	760, 761, 766, 792, 861, 869	itgsplitioo 23604	. . . . . . . . . . . . . . . . 17
871	801	sselda 3603	. . . . . . . . . . . . . . . . . . . 20 $/\$
872	871, 791	syldan 487	. . . . . . . . . . . . . . . . . . 19 $/\$
873	872, 861	itgcl 23550	. . . . . . . . . . . . . . . . . 18
874	866	sselda 3603	. . . . . . . . . . . . . . . . . . . 20 $/\$
875	874, 791	syldan 487	. . . . . . . . . . . . . . . . . . 19 $/\$
876	875, 869	itgcl 23550	. . . . . . . . . . . . . . . . . 18
877	873, 876	addcomd 10238	. . . . . . . . . . . . . . . . 17
878	870, 877	eqtrd 2656	. . . . . . . . . . . . . . . 16
879	878	fveq2d 6195	. . . . . . . . . . . . . . 15
880	876, 873	addcld 10059	. . . . . . . . . . . . . . . . 17
881	880	abscld 14175	. . . . . . . . . . . . . . . 16
882	876	abscld 14175	. . . . . . . . . . . . . . . . 17
883	873	abscld 14175	. . . . . . . . . . . . . . . . 17
884	882, 883	readdcld 10069	. . . . . . . . . . . . . . . 16
885		simp-5r 809	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
886	763, 885	syl 17	. . . . . . . . . . . . . . . . 17
887	886	rpred 11872	. . . . . . . . . . . . . . . 16
888	876, 873	abstrid 14195	. . . . . . . . . . . . . . . 16
889		simplr 792	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
890	763, 889	syl 17	. . . . . . . . . . . . . . . . 17
891	763	simprd 479	. . . . . . . . . . . . . . . . 17
892	882, 883, 887, 890, 891	lt2halvesd 11280	. . . . . . . . . . . . . . . 16
893	881, 884, 887, 888, 892	lelttrd 10195	. . . . . . . . . . . . . . 15
894	879, 893	eqbrtrd 4675	. . . . . . . . . . . . . 14
895	759, 894	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
896	895	ex 450	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
897	711, 896	ralrimi 2957	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
898	897	ex 450	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
899	898	reximdva 3017	. . . . . . . . 9 $/\$ $/\$ $/\$
900	704, 899	mpd 15	. . . . . . . 8 $/\$ $/\$ $/\$
901		negpilt0 39492	. . . . . . . . . . . . . 14
902	11, 771, 10	lttri 10163	. . . . . . . . . . . . . 14 $/\$
903	901, 56, 902	mp2an 708	. . . . . . . . . . . . 13
904	11, 10, 903	ltleii 10160	. . . . . . . . . . . 12
905	904	a1i 11	. . . . . . . . . . 11
906	264	fourierdlem2 40326	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ ..^
907	265, 906	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ ..^
908	267, 907	mpbid 222	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ ..^
909	908	simpld 475	. . . . . . . . . . . . . . 15
910		elmapi 7879	. . . . . . . . . . . . . . 15
911	909, 910	syl 17	. . . . . . . . . . . . . 14
912	911	ffvelrnda 6359	. . . . . . . . . . . . 13 $/\$
913	16	adantr 481	. . . . . . . . . . . . 13 $/\$
914	912, 913	resubcld 10458	. . . . . . . . . . . 12 $/\$
915	914, 80	fmptd 6385	. . . . . . . . . . 11
916	80	a1i 11	. . . . . . . . . . . . 13
917		fveq2 6191	. . . . . . . . . . . . . . 15
918	917	oveq1d 6665	. . . . . . . . . . . . . 14
919	918	adantl 482	. . . . . . . . . . . . 13 $/\$
920	265	nnnn0d 11351	. . . . . . . . . . . . . . 15
921		nn0uz 11722	. . . . . . . . . . . . . . 15
922	920, 921	syl6eleq 2711	. . . . . . . . . . . . . 14
923		eluzfz1 12348	. . . . . . . . . . . . . 14
924	922, 923	syl 17	. . . . . . . . . . . . 13
925	911, 924	ffvelrnd 6360	. . . . . . . . . . . . . 14
926	925, 16	resubcld 10458	. . . . . . . . . . . . 13
927	916, 919, 924, 926	fvmptd 6288	. . . . . . . . . . . 12
928	908	simprd 479	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^
929	928	simpld 475	. . . . . . . . . . . . . 14 $/\$
930	929	simpld 475	. . . . . . . . . . . . 13
931	930	oveq1d 6665	. . . . . . . . . . . 12
932	450	recnd 10068	. . . . . . . . . . . . 13
933	16	recnd 10068	. . . . . . . . . . . . 13
934	932, 933	pncand 10393	. . . . . . . . . . . 12
935	927, 931, 934	3eqtrd 2660	. . . . . . . . . . 11
936	450, 452, 16, 264, 849, 265, 267, 80	fourierdlem14 40338	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^
937	849	fourierdlem2 40326	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^
938	265, 937	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^ $/\$ $/\$ $/\$ ..^
939	936, 938	mpbid 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ ..^
940	939	simprd 479	. . . . . . . . . . . . 13 $/\$ $/\$ ..^
941	940	simpld 475	. . . . . . . . . . . 12 $/\$
942	941	simprd 479	. . . . . . . . . . 11
943	940	simprd 479	. . . . . . . . . . . 12 ..^
944	943	r19.21bi 2932	. . . . . . . . . . 11 $/\$ ..^
945	15	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
946	849, 265, 936	fourierdlem15 40339	. . . . . . . . . . . . . 14
947	946	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^
948		elfzofz 12485	. . . . . . . . . . . . . 14 ..^
949	948	adantl 482	. . . . . . . . . . . . 13 $/\$ ..^
950	947, 949	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$ ..^
951		fzofzp1 12565	. . . . . . . . . . . . . 14 ..^
952	951	adantl 482	. . . . . . . . . . . . 13 $/\$ ..^
953	947, 952	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$ ..^
954	16	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
955		ffn 6045	. . . . . . . . . . . . . . . . . 18
956	909, 910, 955	3syl 18	. . . . . . . . . . . . . . . . 17
957		fvelrnb 6243	. . . . . . . . . . . . . . . . 17
958	956, 957	syl 17	. . . . . . . . . . . . . . . 16
959	839, 958	mpbid 222	. . . . . . . . . . . . . . 15
960		oveq1 6657	. . . . . . . . . . . . . . . . . . 19
961	960	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
962	933	subidd 10380	. . . . . . . . . . . . . . . . . . 19
963	962	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
964	961, 963	eqtr2d 2657	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
965	964	ex 450	. . . . . . . . . . . . . . . 16 $/\$
966	965	reximdva 3017	. . . . . . . . . . . . . . 15
967	959, 966	mpd 15	. . . . . . . . . . . . . 14
968	80	elrnmpt 5372	. . . . . . . . . . . . . . 15
969	771, 968	ax-mp 5	. . . . . . . . . . . . . 14
970	967, 969	sylibr 224	. . . . . . . . . . . . 13
971	849, 265, 936, 970	fourierdlem12 40336	. . . . . . . . . . . 12 $/\$ ..^
972	911	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
973	972, 949	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
974	973, 954	resubcld 10458	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
975	80	fvmpt2 6291	. . . . . . . . . . . . . . . . . 18 $/\$
976	949, 974, 975	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ ..^
977	976	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ ..^
978	973	recnd 10068	. . . . . . . . . . . . . . . . 17 $/\$ ..^
979	933	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^
980	978, 979	npcand 10396	. . . . . . . . . . . . . . . 16 $/\$ ..^
981	977, 980	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ ..^
982		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
983	982	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21
984	983	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . 20
985	80, 984	eqtr4i 2647	. . . . . . . . . . . . . . . . . . 19
986	985	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
987		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
988	987	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19
989	988	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
990	972, 952	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
991	990, 954	resubcld 10458	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
992	986, 989, 952, 991	fvmptd 6288	. . . . . . . . . . . . . . . . 17 $/\$ ..^
993	992	oveq1d 6665	. . . . . . . . . . . . . . . 16 $/\$ ..^
994	990	recnd 10068	. . . . . . . . . . . . . . . . 17 $/\$ ..^
995	994, 979	npcand 10396	. . . . . . . . . . . . . . . 16 $/\$ ..^
996	993, 995	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ ..^
997	981, 996	oveq12d 6668	. . . . . . . . . . . . . 14 $/\$ ..^
998	997	reseq2d 5396	. . . . . . . . . . . . 13 $/\$ ..^
999	997	oveq1d 6665	. . . . . . . . . . . . 13 $/\$ ..^
1000	269, 998, 999	3eltr4d 2716	. . . . . . . . . . . 12 $/\$ ..^
1001	28	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
1002	39	adantr 481	. . . . . . . . . . . 12 $/\$ ..^
1003	945, 950, 953, 954, 971, 1000, 1001, 1002, 40	fourierdlem40 40364	. . . . . . . . . . 11 $/\$ ..^
1004		id 22	. . . . . . . . . . . . . 14
1005	44	a1i 11	. . . . . . . . . . . . . 14
1006	1004, 1005	fssd 6057	. . . . . . . . . . . . 13
1007	404, 598, 1006	3syl 18	. . . . . . . . . . . 12 $/\$ ..^
1008		eqid 2622	. . . . . . . . . . . 12
1009	16, 264, 15, 839, 27, 39, 40, 265, 267, 271, 80, 849, 850, 1007, 854, 1008	fourierdlem75 40398	. . . . . . . . . . 11 $/\$ ..^ lim
1010		eqid 2622	. . . . . . . . . . . 12
1011	16, 264, 15, 839, 28, 38, 40, 265, 267, 273, 80, 849, 850, 599, 852, 1010	fourierdlem74 40397	. . . . . . . . . . 11 $/\$ ..^ lim
1012		fveq2 6191	. . . . . . . . . . . . 13
1013		oveq1 6657	. . . . . . . . . . . . . 14
1014	1013	fveq2d 6195	. . . . . . . . . . . . 13
1015	1012, 1014	oveq12d 6668	. . . . . . . . . . . 12
1016	1015	cbvmptv 4750	. . . . . . . . . . 11 ..^ ..^
1017	450, 452, 905, 180, 265, 915, 935, 942, 944, 1003, 1009, 1011, 1016	fourierdlem70 40393	. . . . . . . . . 10
1018		eqid 2622	. . . . . . . . . 10
1019		fveq2 6191	. . . . . . . . . . . . . . . . . 18
1020	1019	fveq2d 6195	. . . . . . . . . . . . . . . . 17
1021	1020	breq1d 4663	. . . . . . . . . . . . . . . 16
1022	1021	cbvralv 3171	. . . . . . . . . . . . . . 15
1023	1022	ralbii 2980	. . . . . . . . . . . . . 14
1024	1023	3anbi3i 1255	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
1025	1024	anbi1i 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
1026	1025	anbi1i 731	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
1027	1026	anbi1i 731	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
1028	15, 16, 28, 39, 40, 41, 42, 831, 829, 1017, 856, 1018, 1027	fourierdlem87 40410	. . . . . . . . 9 $/\$ $/\$
1029		iftrue 4092	. . . . . . . . . . . . . . . 16
1030	1029	negeqd 10275	. . . . . . . . . . . . . . 15
1031	1030	adantl 482	. . . . . . . . . . . . . 14 $/\$
1032	52	a1i 11	. . . . . . . . . . . . . . 15 $/\$
1033	53	a1i 11	. . . . . . . . . . . . . . 15 $/\$
1034		rpre 11839	. . . . . . . . . . . . . . . . 17
1035	1034	renegcld 10457	. . . . . . . . . . . . . . . 16
1036	1035	adantr 481	. . . . . . . . . . . . . . 15 $/\$
1037	1034	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
1038	10	rehalfcli 11281	. . . . . . . . . . . . . . . . . 18
1039	1038	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
1040	10	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
1041		simpr 477	. . . . . . . . . . . . . . . . 17 $/\$
1042		halfpos 11262	. . . . . . . . . . . . . . . . . . . 20
1043	10, 1042	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
1044	56, 1043	mpbi 220	. . . . . . . . . . . . . . . . . 18
1045	1044	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
1046	1037, 1039, 1040, 1041, 1045	lelttrd 10195	. . . . . . . . . . . . . . . 16 $/\$
1047	1037, 1040	ltnegd 10605	. . . . . . . . . . . . . . . 16 $/\$
1048	1046, 1047	mpbid 222	. . . . . . . . . . . . . . 15 $/\$
1049		rpgt0 11844	. . . . . . . . . . . . . . . . 17
1050	1034	lt0neg2d 10598	. . . . . . . . . . . . . . . . 17
1051	1049, 1050	mpbid 222	. . . . . . . . . . . . . . . 16
1052	1051	adantr 481	. . . . . . . . . . . . . . 15 $/\$
1053	1032, 1033, 1036, 1048, 1052	eliood 39720	. . . . . . . . . . . . . 14 $/\$
1054	1031, 1053	eqeltrd 2701	. . . . . . . . . . . . 13 $/\$
1055		iffalse 4095	. . . . . . . . . . . . . . . 16
1056	1055	negeqd 10275	. . . . . . . . . . . . . . 15
1057	1038	renegcli 10342	. . . . . . . . . . . . . . . . . . 19
1058	1057	rexri 10097	. . . . . . . . . . . . . . . . . 18
1059	52, 53, 1058	3pm3.2i 1239	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
1060	1038, 10	ltnegi 10572	. . . . . . . . . . . . . . . . . . 19
1061	1044, 1060	mpbi 220	. . . . . . . . . . . . . . . . . 18
1062		2pos 11112	. . . . . . . . . . . . . . . . . . . 20
1063	10, 101, 56, 1062	divgt0ii 10941	. . . . . . . . . . . . . . . . . . 19
1064		lt0neg2 10535	. . . . . . . . . . . . . . . . . . . 20
1065	1038, 1064	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
1066	1063, 1065	mpbi 220	. . . . . . . . . . . . . . . . . 18
1067	1061, 1066	pm3.2i 471	. . . . . . . . . . . . . . . . 17 $/\$
1068		elioo3g 12204	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
1069	1059, 1067, 1068	mpbir2an 955	. . . . . . . . . . . . . . . 16
1070	1069	a1i 11	. . . . . . . . . . . . . . 15
1071	1056, 1070	eqeltrd 2701	. . . . . . . . . . . . . 14
1072	1071	adantl 482	. . . . . . . . . . . . 13 $/\$
1073	1054, 1072	pm2.61dan 832	. . . . . . . . . . . 12
1074	1073	3ad2ant2 1083	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
1075		ioombl 23333	. . . . . . . . . . . . . . 15
1076	1075	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
1077		simpr 477	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
1078	1076, 1077	jca 554	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
1079		ioossicc 12259	. . . . . . . . . . . . . . . . 17
1080	1079	a1i 11	. . . . . . . . . . . . . . . 16
1081	11	a1i 11	. . . . . . . . . . . . . . . . 17
1082	10	a1i 11	. . . . . . . . . . . . . . . . 17
1083	1037, 1040, 1046	ltled 10185	. . . . . . . . . . . . . . . . . . . 20 $/\$
1084	1037, 1040	lenegd 10606	. . . . . . . . . . . . . . . . . . . 20 $/\$
1085	1083, 1084	mpbid 222	. . . . . . . . . . . . . . . . . . 19 $/\$
1086	1030	eqcomd 2628	. . . . . . . . . . . . . . . . . . . 20
1087	1086	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
1088	1085, 1087	breqtrd 4679	. . . . . . . . . . . . . . . . . 18 $/\$
1089	11, 1057, 1061	ltleii 10160	. . . . . . . . . . . . . . . . . . . 20
1090	1089	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
1091	1056	eqcomd 2628	. . . . . . . . . . . . . . . . . . . 20
1092	1091	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
1093	1090, 1092	breqtrd 4679	. . . . . . . . . . . . . . . . . 18 $/\$
1094	1088, 1093	pm2.61dan 832	. . . . . . . . . . . . . . . . 17
1095	772	a1i 11	. . . . . . . . . . . . . . . . 17
1096		iccss 12241	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
1097	1081, 1082, 1094, 1095, 1096	syl22anc 1327	. . . . . . . . . . . . . . . 16
1098	1080, 1097	sstrd 3613	. . . . . . . . . . . . . . 15
1099	796, 1073	sseldi 3601	. . . . . . . . . . . . . . . . . 18
1100		0red 10041	. . . . . . . . . . . . . . . . . 18
1101		rpge0 11845	. . . . . . . . . . . . . . . . . . . . . 22
1102	1101	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1103	1041	iftrued 4094	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1104	1102, 1103	breqtrrd 4681	. . . . . . . . . . . . . . . . . . . 20 $/\$
1105	771, 1038, 1063	ltleii 10160	. . . . . . . . . . . . . . . . . . . . 21
1106		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
1107	1106	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1108	1105, 1107	syl5breqr 4691	. . . . . . . . . . . . . . . . . . . 20 $/\$
1109	1104, 1108	pm2.61dan 832	. . . . . . . . . . . . . . . . . . 19
1110	1038	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
1111	1034, 1110	ifcld 4131	. . . . . . . . . . . . . . . . . . . 20
1112	1111	le0neg2d 10600	. . . . . . . . . . . . . . . . . . 19
1113	1109, 1112	mpbid 222	. . . . . . . . . . . . . . . . . 18
1114		volioo 23337	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
1115	1099, 1100, 1113, 1114	syl3anc 1326	. . . . . . . . . . . . . . . . 17
1116		0cn 10032	. . . . . . . . . . . . . . . . . . 19
1117	1116	a1i 11	. . . . . . . . . . . . . . . . . 18
1118	1111	recnd 10068	. . . . . . . . . . . . . . . . . 18
1119	1117, 1118	subnegd 10399	. . . . . . . . . . . . . . . . 17
1120	1118	addid2d 10237	. . . . . . . . . . . . . . . . 17
1121	1115, 1119, 1120	3eqtrd 2660	. . . . . . . . . . . . . . . 16
1122		min1 12020	. . . . . . . . . . . . . . . . 17 $/\$
1123	1034, 1038, 1122	sylancl 694	. . . . . . . . . . . . . . . 16
1124	1121, 1123	eqbrtrd 4675	. . . . . . . . . . . . . . 15
1125	1098, 1124	jca 554	. . . . . . . . . . . . . 14 $/\$
1126	1125	adantr 481	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
1127		sseq1 3626	. . . . . . . . . . . . . . . 16
1128		fveq2 6191	. . . . . . . . . . . . . . . . 17
1129	1128	breq1d 4663	. . . . . . . . . . . . . . . 16
1130	1127, 1129	anbi12d 747	. . . . . . . . . . . . . . 15 $/\$ $/\$
1131		itgeq1 23539	. . . . . . . . . . . . . . . . . 18
1132	1131	fveq2d 6195	. . . . . . . . . . . . . . . . 17
1133	1132	breq1d 4663	. . . . . . . . . . . . . . . 16
1134	1133	ralbidv 2986	. . . . . . . . . . . . . . 15
1135	1130, 1134	imbi12d 334	. . . . . . . . . . . . . 14 $/\$ $/\$
1136	1135	rspcva 3307	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
1137	1078, 1126, 1136	sylc 65	. . . . . . . . . . . 12 $/\$ $/\$
1138	1137	3adant1 1079	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
1139		oveq1 6657	. . . . . . . . . . . . . . . 16
1140	1139	itgeq1d 40172	. . . . . . . . . . . . . . 15
1141	1140	fveq2d 6195	. . . . . . . . . . . . . 14
1142	1141	breq1d 4663	. . . . . . . . . . . . 13
1143	1142	ralbidv 2986	. . . . . . . . . . . 12
1144	1143	rspcev 3309	. . . . . . . . . . 11 $/\$
1145	1074, 1138, 1144	syl2anc 693	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
1146	1145	rexlimdv3a 3033	. . . . . . . . 9 $/\$ $/\$
1147	1028, 1146	mpd 15	. . . . . . . 8 $/\$
1148	900, 1147	r19.29a 3078	. . . . . . 7 $/\$
1149	1148	ralrimiva 2966	. . . . . 6
1150		nnex 11026	. . . . . . . . 9
1151	1150	mptex 6486	. . . . . . . 8
1152	1151	a1i 11	. . . . . . 7
1153		eqidd 2623	. . . . . . . 8 $/\$
1154	777	adantl 482	. . . . . . . . . . 11 $/\$ $/\$ $/\$
1155	779	ad4ant14 1293	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
1156	777	adantl 482	. . . . . . . . . . . . . . 15 $/\$ $/\$
1157		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1158		simpl 473	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1159	1157, 1158	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . 20 $/\$
1160	1159	nnred 11035	. . . . . . . . . . . . . . . . . . 19 $/\$
1161	729	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
1162	1160, 1161	readdcld 10069	. . . . . . . . . . . . . . . . . 18 $/\$
1163	1162	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
1164	214, 1156	sseldi 3601	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
1165	1163, 1164	remulcld 10070	. . . . . . . . . . . . . . . 16 $/\$ $/\$
1166	1165	resincld 14873	. . . . . . . . . . . . . . 15 $/\$ $/\$
1167	1156, 1166, 832	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$
1168	1167	adantlll 754	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
1169	1160	adantll 750	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
1170	1169	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
1171		1red 10055	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
1172	1171	rehalfcld 11279	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
1173	1170, 1172	readdcld 10069	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
1174	214, 1154	sseldi 3601	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
1175	1173, 1174	remulcld 10070	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
1176	1175	resincld 14873	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
1177	1168, 1176	eqeltrd 2701	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
1178	1155, 1177	remulcld 10070	. . . . . . . . . . 11 $/\$ $/\$ $/\$
1179	829	fvmpt2 6291	. . . . . . . . . . 11 $/\$
1180	1154, 1178, 1179	syl2anc 693	. . . . . . . . . 10 $/\$ $/\$ $/\$
1181		oveq1 6657	. . . . . . . . . . . . . . 15
1182	1181	oveq1d 6665	. . . . . . . . . . . . . 14
1183	1182	fveq2d 6195	. . . . . . . . . . . . 13
1184	1183	ad2antlr 763	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
1185	1168, 1184	eqtrd 2656	. . . . . . . . . . 11 $/\$ $/\$ $/\$
1186	1185	oveq2d 6666	. . . . . . . . . 10 $/\$ $/\$ $/\$
1187	1180, 1186	eqtrd 2656	. . . . . . . . 9 $/\$ $/\$ $/\$
1188	1187	itgeq2dv 23548	. . . . . . . 8 $/\$ $/\$
1189		simpr 477	. . . . . . . 8 $/\$
1190	810	itgeq2dv 23548	. . . . . . . . . . 11
1191	1190	eleq1d 2686	. . . . . . . . . 10
1192	805, 1191	imbi12d 334	. . . . . . . . 9 $/\$ $/\$
1193	779	adantlr 751	. . . . . . . . . . 11 $/\$ $/\$
1194		simpr 477	. . . . . . . . . . . 12 $/\$
1195	1194, 777, 826	syl2an 494	. . . . . . . . . . 11 $/\$ $/\$
1196	1193, 1195	remulcld 10070	. . . . . . . . . 10 $/\$ $/\$
1197	1196, 858	itgcl 23550	. . . . . . . . 9 $/\$
1198	1192, 1197	chvarv 2263	. . . . . . . 8 $/\$
1199	1153, 1188, 1189, 1198	fvmptd 6288	. . . . . . 7 $/\$
1200	9, 2, 1152, 1199, 1198	clim0c 14238	. . . . . 6
1201	1149, 1200	mpbird 247	. . . . 5
1202	1150	mptex 6486	. . . . . . 7
1203	6, 1202	eqeltri 2697	. . . . . 6
1204	1203	a1i 11	. . . . 5
1205	1150	mptex 6486	. . . . . . 7
1206	1205	a1i 11	. . . . . 6
1207		picn 24211	. . . . . . 7
1208	1207	a1i 11	. . . . . 6
1209		eqidd 2623	. . . . . . . 8
1210		eqidd 2623	. . . . . . . 8 $/\$
1211		id 22	. . . . . . . 8
1212	10	a1i 11	. . . . . . . 8
1213	1209, 1210, 1211, 1212	fvmptd 6288	. . . . . . 7
1214	1213	adantl 482	. . . . . 6 $/\$
1215	9, 2, 1206, 1208, 1214	climconst 14274	. . . . 5
1216	771, 56	gtneii 10149	. . . . . 6
1217	1216	a1i 11	. . . . 5
1218	16	adantr 481	. . . . . . . . . . 11 $/\$
1219	28	adantr 481	. . . . . . . . . . 11 $/\$
1220	39	adantr 481	. . . . . . . . . . 11 $/\$
1221	838, 1218, 1219, 1220, 40, 41, 42, 843, 831, 829	fourierdlem67 40390	. . . . . . . . . 10 $/\$
1222	1221	adantr 481	. . . . . . . . 9 $/\$ $/\$
1223	814	sselda 3603	. . . . . . . . 9 $/\$ $/\$
1224	1222, 1223	ffvelrnd 6360	. . . . . . . 8 $/\$ $/\$
1225	1221	ffvelrnda 6359	. . . . . . . . 9 $/\$ $/\$
1226	1221	feqmptd 6249	. . . . . . . . . 10 $/\$
1227	1226, 856	eqeltrrd 2702	. . . . . . . . 9 $/\$
1228	814, 816, 1225, 1227	iblss 23571	. . . . . . . 8 $/\$
1229	1224, 1228	itgcl 23550	. . . . . . 7 $/\$
1230		eqid 2622	. . . . . . . 8
1231	1230	fvmpt2 6291	. . . . . . 7 $/\$
1232	1194, 1229, 1231	syl2anc 693	. . . . . 6 $/\$
1233	1232, 1229	eqeltrd 2701	. . . . 5 $/\$
1234		id 22	. . . . . . . 8
1235		eqid 2622	. . . . . . . . 9
1236	1235	fvmpt2 6291	. . . . . . . 8 $/\$
1237	1234, 10, 1236	sylancl 694	. . . . . . 7
1238	1207	a1i 11	. . . . . . . . 9
1239	1216	a1i 11	. . . . . . . . 9
1240	1238, 1239	jca 554	. . . . . . . 8 $/\$
1241		eldifsn 4317	. . . . . . . 8 $\$ $/\$
1242	1240, 1241	sylibr 224	. . . . . . 7 $\$
1243	1237, 1242	eqeltrd 2701	. . . . . 6 $\$
1244	1243	adantl 482	. . . . 5 $/\$ $\$
1245	1207	a1i 11	. . . . . . . 8 $/\$
1246	1216	a1i 11	. . . . . . . 8 $/\$
1247	1229, 1245, 1246	divcld 10801	. . . . . . 7 $/\$
1248	6	fvmpt2 6291	. . . . . . 7 $/\$
1249	1194, 1247, 1248	syl2anc 693	. . . . . 6 $/\$
1250	1232	eqcomd 2628	. . . . . . 7 $/\$
1251	1237	eqcomd 2628	. . . . . . . 8
1252	1251	adantl 482	. . . . . . 7 $/\$
1253	1250, 1252	oveq12d 6668	. . . . . 6 $/\$
1254	1249, 1253	eqtrd 2656	. . . . 5 $/\$
1255	3, 4, 5, 8, 9, 2, 1201, 1204, 1215, 1217, 1233, 1244, 1254	climdivf 39844	. . . 4
1256	1207, 1216	div0i 10759	. . . . 5
1257	1256	a1i 11	. . . 4
1258	1255, 1257	breqtrd 4679	. . 3
1259		fourierdlem103.z	. . . . 5
1260	1150	mptex 6486	. . . . 5
1261	1259, 1260	eqeltri 2697	. . . 4
1262	1261	a1i 11	. . 3
1263	1150	mptex 6486	. . . . 5
1264	1263	a1i 11	. . . 4
1265		limccl 23639	. . . . . 6 lim
1266	1265, 38	sseldi 3601	. . . . 5
1267	1266	halfcld 11277	. . . 4
1268		eqidd 2623	. . . . 5 $/\$
1269		eqidd 2623	. . . . 5 $/\$ $/\$
1270	9	eqcomi 2631	. . . . . . . 8
1271	1270	eleq2i 2693	. . . . . . 7
1272	1271	biimpi 206	. . . . . 6
1273	1272	adantl 482	. . . . 5 $/\$
1274	1267	adantr 481	. . . . 5 $/\$
1275	1268, 1269, 1273, 1274	fvmptd 6288	. . . 4 $/\$
1276	1, 2, 1264, 1267, 1275	climconst 14274	. . 3
1277	1247, 6	fmptd 6385	. . . . 5
1278	1277	adantr 481	. . . 4 $/\$
1279	1278, 1273	ffvelrnd 6360	. . 3 $/\$
1280	1275, 1274	eqeltrd 2701	. . 3 $/\$
1281	1275	oveq2d 6666	. . . 4 $/\$
1282	815	a1i 11	. . . . . 6
1283	52	a1i 11	. . . . . . . . . . . . 13
1284		0red 10041	. . . . . . . . . . . . . 14
1285	1284	rexrd 10089	. . . . . . . . . . . . 13
1286		id 22	. . . . . . . . . . . . 13
1287		iooltub 39735	. . . . . . . . . . . . 13 $/\$ $/\$
1288	1283, 1285, 1286, 1287	syl3anc 1326	. . . . . . . . . . . 12
1289	787, 1288	ltned 10173	. . . . . . . . . . 11
1290	1289	neneqd 2799	. . . . . . . . . 10
1291		velsn 4193	. . . . . . . . . 10
1292	1290, 1291	sylnibr 319	. . . . . . . . 9
1293	777, 1292	eldifd 3585	. . . . . . . 8 $\$
1294	1293	ssriv 3607	. . . . . . 7 $\$
1295	1294	a1i 11	. . . . . 6 $\$
1296		fourierdlem103.d	. . . . . 6
1297	787	adantl 482	. . . . . . . 8 $/\$
1298		0red 10041	. . . . . . . 8 $/\$
1299	787, 1284, 1288	ltled 10185	. . . . . . . . 9
1300	1299	adantl 482	. . . . . . . 8 $/\$
1301	1297, 1298, 1300	lensymd 10188	. . . . . . 7 $/\$
1302	1301	iffalsed 4097	. . . . . 6 $/\$
1303		eqid 2622	. . . . . . . 8
1304	11	a1i 11	. . . . . . . 8 $/\$
1305		0red 10041	. . . . . . . 8 $/\$
1306	11, 771, 901	ltleii 10160	. . . . . . . . 9
1307	1306	a1i 11	. . . . . . . 8 $/\$
1308		eqid 2622	. . . . . . . 8
1309	1296, 1194, 1303, 1304, 1305, 1307, 1308	dirkeritg 40319	. . . . . . 7 $/\$
1310		ubicc2 12289	. . . . . . . . . . 11 $/\$ $/\$
1311	52, 53, 1306, 1310	mp3an 1424	. . . . . . . . . 10
1312		oveq1 6657	. . . . . . . . . . . . . . . 16
1313	239, 244	div0i 10759	. . . . . . . . . . . . . . . . 17
1314	1313	a1i 11	. . . . . . . . . . . . . . . 16
1315	1312, 1314	eqtrd 2656	. . . . . . . . . . . . . . 15
1316		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . 22
1317		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . . . 24
1318	1317	zcnd 11483	. . . . . . . . . . . . . . . . . . . . . . 23
1319	1318	mul01d 10235	. . . . . . . . . . . . . . . . . . . . . 22
1320	1316, 1319	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1321	1320	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 $/\$
1322		sin0 14879	. . . . . . . . . . . . . . . . . . . . 21
1323	1322	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
1324	1321, 1323	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 $/\$
1325	1324	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 $/\$
1326		0red 10041	. . . . . . . . . . . . . . . . . . . . . 22
1327		1red 10055	. . . . . . . . . . . . . . . . . . . . . 22
1328	1317	zred 11482	. . . . . . . . . . . . . . . . . . . . . 22
1329	99	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
1330		elfzle1 12344	. . . . . . . . . . . . . . . . . . . . . 22
1331	1326, 1327, 1328, 1329, 1330	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . 21
1332	1331	gt0ne0d 10592	. . . . . . . . . . . . . . . . . . . 20
1333	1318, 1332	div0d 10800	. . . . . . . . . . . . . . . . . . 19
1334	1333	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
1335	1325, 1334	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$
1336	1335	sumeq2dv 14433	. . . . . . . . . . . . . . . 16
1337		fzfi 12771	. . . . . . . . . . . . . . . . . . 19
1338	1337	olci 406	. . . . . . . . . . . . . . . . . 18 $\/$
1339		sumz 14453	. . . . . . . . . . . . . . . . . 18 $\/$
1340	1338, 1339	ax-mp 5	. . . . . . . . . . . . . . . . 17
1341	1340	a1i 11	. . . . . . . . . . . . . . . 16
1342	1336, 1341	eqtrd 2656	. . . . . . . . . . . . . . 15
1343	1315, 1342	oveq12d 6668	. . . . . . . . . . . . . 14
1344		00id 10211	. . . . . . . . . . . . . . 15
1345	1344	a1i 11	. . . . . . . . . . . . . 14
1346	1343, 1345	eqtrd 2656	. . . . . . . . . . . . 13
1347	1346	oveq1d 6665	. . . . . . . . . . . 12
1348	1256	a1i 11	. . . . . . . . . . . 12
1349	1347, 1348	eqtrd 2656	. . . . . . . . . . 11
1350	771	elexi 3213	. . . . . . . . . . 11
1351	1349, 1308, 1350	fvmpt 6282	. . . . . . . . . 10
1352	1311, 1351	ax-mp 5	. . . . . . . . 9
1353		lbicc2 12288	. . . . . . . . . . . 12 $/\$ $/\$
1354	52, 53, 1306, 1353	mp3an 1424	. . . . . . . . . . 11
1355		oveq1 6657	. . . . . . . . . . . . . 14
1356		oveq2 6658	. . . . . . . . . . . . . . . . 17
1357	1356	fveq2d 6195	. . . . . . . . . . . . . . . 16
1358	1357	oveq1d 6665	. . . . . . . . . . . . . . 15
1359	1358	sumeq2sdv 14435	. . . . . . . . . . . . . 14
1360	1355, 1359	oveq12d 6668	. . . . . . . . . . . . 13
1361	1360	oveq1d 6665	. . . . . . . . . . . 12
1362		ovex 6678	. . . . . . . . . . . 12
1363	1361, 1308, 1362	fvmpt 6282	. . . . . . . . . . 11
1364	1354, 1363	ax-mp 5	. . . . . . . . . 10
1365		mulneg12 10468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
1366	1318, 1207, 1365	sylancl 694	. . . . . . . . . . . . . . . . . . . . 21
1367	1366	eqcomd 2628	. . . . . . . . . . . . . . . . . . . 20
1368	1367	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19
1369	1318	negcld 10379	. . . . . . . . . . . . . . . . . . . 20
1370	1207	a1i 11	. . . . . . . . . . . . . . . . . . . 20
1371	1216	a1i 11	. . . . . . . . . . . . . . . . . . . 20
1372	1369, 1370, 1371	divcan4d 10807	. . . . . . . . . . . . . . . . . . 19
1373	1368, 1372	eqtrd 2656	. . . . . . . . . . . . . . . . . 18
1374	1317	znegcld 11484	. . . . . . . . . . . . . . . . . 18
1375	1373, 1374	eqeltrd 2701	. . . . . . . . . . . . . . . . 17
1376		negpicn 24214	. . . . . . . . . . . . . . . . . . . 20
1377	1376	a1i 11	. . . . . . . . . . . . . . . . . . 19
1378	1318, 1377	mulcld 10060	. . . . . . . . . . . . . . . . . 18
1379		sineq0 24273	. . . . . . . . . . . . . . . . . 18
1380	1378, 1379	syl 17	. . . . . . . . . . . . . . . . 17
1381	1375, 1380	mpbird 247	. . . . . . . . . . . . . . . 16
1382	1381	oveq1d 6665	. . . . . . . . . . . . . . 15
1383	1382, 1333	eqtrd 2656	. . . . . . . . . . . . . 14
1384	1383	sumeq2i 14429	. . . . . . . . . . . . 13
1385	1384, 1340	eqtri 2644	. . . . . . . . . . . 12
1386	1385	oveq2i 6661	. . . . . . . . . . 11
1387	1386	oveq1i 6660	. . . . . . . . . 10
1388	1376, 239, 244	divcli 10767	. . . . . . . . . . . . . 14
1389	1388	addid1i 10223	. . . . . . . . . . . . 13
1390		divneg 10719	. . . . . . . . . . . . . 14 $/\$ $/\$
1391	1207, 239, 244, 1390	mp3an 1424	. . . . . . . . . . . . 13
1392	1389, 1391	eqtr4i 2647	. . . . . . . . . . . 12
1393	1392	oveq1i 6660	. . . . . . . . . . 11
1394	1038	recni 10052	. . . . . . . . . . . . 13
1395		divneg 10719	. . . . . . . . . . . . 13 $/\$ $/\$
1396	1394, 1207, 1216, 1395	mp3an 1424	. . . . . . . . . . . 12
1397	1396	eqcomi 2631	. . . . . . . . . . 11
1398	1207, 239, 1207, 244, 1216	divdiv32i 10780	. . . . . . . . . . . . 13
1399	1207, 1216	dividi 10758	. . . . . . . . . . . . . 14
1400	1399	oveq1i 6660	. . . . . . . . . . . . 13
1401	1398, 1400	eqtri 2644	. . . . . . . . . . . 12
1402	1401	negeqi 10274	. . . . . . . . . . 11
1403	1393, 1397, 1402	3eqtri 2648	. . . . . . . . . 10
1404	1364, 1387, 1403	3eqtri 2648	. . . . . . . . 9
1405	1352, 1404	oveq12i 6662	. . . . . . . 8
1406	1405	a1i 11	. . . . . . 7 $/\$
1407		halfcn 11247	. . . . . . . . . 10
1408	1116, 1407	subnegi 10360	. . . . . . . . 9
1409	1407	addid2i 10224	. . . . . . . . 9
1410	1408, 1409	eqtri 2644	. . . . . . . 8
1411	1410	a1i 11	. . . . . . 7 $/\$
1412	1309, 1406, 1411	3eqtrd 2660	. . . . . 6 $/\$
1413	15, 16, 264, 265, 267, 839, 269, 271, 273, 40, 41, 42, 831, 829, 850, 599, 852, 854, 27, 38, 1282, 1295, 6, 1296, 39, 1302, 1412	fourierdlem95 40418	. . . . 5 $/\$
1414	1273, 1413	syldan 487	. . . 4 $/\$
1415	1259	a1i 11	. . . . . . 7 $/\$
1416		fveq2 6191	. . . . . . . . . . . 12
1417	1416	fveq1d 6193	. . . . . . . . . . 11
1418	1417	oveq2d 6666	. . . . . . . . . 10
1419	1418	adantr 481	. . . . . . . . 9 $/\$
1420	1419	itgeq2dv 23548	. . . . . . . 8
1421	1420	adantl 482	. . . . . . 7 $/\$ $/\$
1422	15	adantr 481	. . . . . . . . . . 11 $/\$
1423	16	adantr 481	. . . . . . . . . . . 12 $/\$
1424	1423, 1297	readdcld 10069	. . . . . . . . . . 11 $/\$
1425	1422, 1424	ffvelrnd 6360	. . . . . . . . . 10 $/\$
1426	1425	adantlr 751	. . . . . . . . 9 $/\$ $/\$
1427	1296	dirkerf 40314	. . . . . . . . . . 11
1428	1427	ad2antlr 763	. . . . . . . . . 10 $/\$ $/\$
1429	787	adantl 482	. . . . . . . . . 10 $/\$ $/\$
1430	1428, 1429	ffvelrnd 6360	. . . . . . . . 9 $/\$ $/\$
1431	1426, 1430	remulcld 10070	. . . . . . . 8 $/\$ $/\$
1432	15	adantr 481	. . . . . . . . . . . 12 $/\$
1433	16	adantr 481	. . . . . . . . . . . . 13 $/\$
1434	214	sseli 3599	. . . . . . . . . . . . . 14
1435	1434	adantl 482	. . . . . . . . . . . . 13 $/\$
1436	1433, 1435	readdcld 10069	. . . . . . . . . . . 12 $/\$
1437	1432, 1436	ffvelrnd 6360	. . . . . . . . . . 11 $/\$
1438	1437	adantlr 751	. . . . . . . . . 10 $/\$ $/\$
1439	1427	ad2antlr 763	. . . . . . . . . . 11 $/\$ $/\$
1440	1434	adantl 482	. . . . . . . . . . 11 $/\$ $/\$
1441	1439, 1440	ffvelrnd 6360	. . . . . . . . . 10 $/\$ $/\$
1442	1438, 1441	remulcld 10070	. . . . . . . . 9 $/\$ $/\$
1443	10	a1i 11	. . . . . . . . . 10 $/\$
1444	1296	dirkercncf 40324	. . . . . . . . . . 11
1445	1444	adantl 482	. . . . . . . . . 10 $/\$
1446		eqid 2622	. . . . . . . . . 10
1447	1304, 1443, 838, 1218, 264, 844, 845, 846, 847, 848, 80, 849, 1445, 1446	fourierdlem84 40407	. . . . . . . . 9 $/\$
1448	814, 816, 1442, 1447	iblss 23571	. . . . . . . 8 $/\$
1449	1431, 1448	itgrecl 23564	. . . . . . 7 $/\$
1450	1415, 1421, 1194, 1449	fvmptd 6288	. . . . . 6 $/\$
1451	1450	eqcomd 2628	. . . . 5 $/\$
1452	1273, 1451	syldan 487	. . . 4 $/\$
1453	1281, 1414, 1452	3eqtrrd 2661	. . 3 $/\$
1454	1, 2, 1258, 1262, 1276, 1279, 1280, 1453	climadd 14362	. 2
1455	1267	addid2d 10237	. 2
1456	1454, 1455	breqtrd 4679	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wtru 1484

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200

csb 3533 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

csn 4177

cpr 4179 class class class wbr 4653

cmpt 4729

cdm 5114

crn 5115

cres 5116

cio 5849

wfn 5883

wf 5884

cfv 5888

wiso 5889

crio 6610 (class class class)co 6650

cmap 7857

cfn 7955

csup 8346

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cpnf 10071

cmnf 10072

cxr 10073

clt 10074

cle 10075

cmin 10266

cneg 10267

cdiv 10684

cn 11020

c2 11070

c3 11071

cn0 11292

cz 11377

cuz 11687

crp 11832

cioo 12175

cicc 12178

cfz 12326 ..^cfzo 12465

cmo 12668

chash 13117

cabs 13974

cli 14215

csu 14416

csin 14794

cpi 14797

ctopn 16082

ctg 16098 ℂ_fldccnfld 19746

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-xnn0 11364 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-ef 14798 df-sin 14800 df-cos 14801 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-t1 21118 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389 df-itg2 23390 df-ibl 23391 df-itg 23392 df-0p 23437 df-limc 23630 df-dv 23631

This theorem is referenced by: fourierdlem112 40435

W3C validator