fourierdlem104 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem104 40427

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

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

**Assertion**
Ref	Expression
fourierdlem104

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

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