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 38068

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 2450	. . 3
2		1zzd 10965	. . 3
3		nfv 1760	. . . . 5
4		nfmpt1 4491	. . . . 5
5		nfmpt1 4491	. . . . 5
6		fourierdlem104.e	. . . . . 6
7		nfmpt1 4491	. . . . . 6
8	6, 7	nfcxfr 2589	. . . . 5
9		nnuz 11191	. . . . 5
10		elioore 11663	. . . . . . . . . . . . . . . 16
11	10	adantl 468	. . . . . . . . . . . . . . 15 $/\$
12		pire 23406	. . . . . . . . . . . . . . . 16
13	12	a1i 11	. . . . . . . . . . . . . . 15 $/\$
14		fourierdlem104.f	. . . . . . . . . . . . . . . . . . . 20
15		fourierdlem104.xre	. . . . . . . . . . . . . . . . . . . 20
16		ioossre 11693	. . . . . . . . . . . . . . . . . . . . . . 23
17	16	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
18	14, 17	fssresd 5748	. . . . . . . . . . . . . . . . . . . . 21
19		ioosscn 37585	. . . . . . . . . . . . . . . . . . . . . 22
20	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
21		eqid 2450	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ℂ_fld
22		pnfxr 11409	. . . . . . . . . . . . . . . . . . . . . . 23
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
24	15	ltpnfd 11420	. . . . . . . . . . . . . . . . . . . . . 22
25	21, 23, 15, 24	lptioo1cn 37721	. . . . . . . . . . . . . . . . . . . . 21 ℂ_fld
26		fourierdlem104.y	. . . . . . . . . . . . . . . . . . . . 21 lim
27	18, 20, 25, 26	limcrecl 37703	. . . . . . . . . . . . . . . . . . . 20
28		ioossre 11693	. . . . . . . . . . . . . . . . . . . . . . 23
29	28	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
30	14, 29	fssresd 5748	. . . . . . . . . . . . . . . . . . . . 21
31		ioosscn 37585	. . . . . . . . . . . . . . . . . . . . . 22
32	31	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
33		mnfxr 11411	. . . . . . . . . . . . . . . . . . . . . . 23
34	33	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
35	15	mnfltd 11423	. . . . . . . . . . . . . . . . . . . . . 22
36	21, 34, 15, 35	lptioo2cn 37720	. . . . . . . . . . . . . . . . . . . . 21 ℂ_fld
37		fourierdlem104.w	. . . . . . . . . . . . . . . . . . . . 21 lim
38	30, 32, 36, 37	limcrecl 37703	. . . . . . . . . . . . . . . . . . . 20
39		fourierdlem104.h	. . . . . . . . . . . . . . . . . . . 20
40		fourierdlem104.k	. . . . . . . . . . . . . . . . . . . 20
41		fourierdlem104.u	. . . . . . . . . . . . . . . . . . . 20
42	14, 15, 27, 38, 39, 40, 41	fourierdlem55 38019	. . . . . . . . . . . . . . . . . . 19
43		ax-resscn 9593	. . . . . . . . . . . . . . . . . . . 20
44	43	a1i 11	. . . . . . . . . . . . . . . . . . 19
45	42, 44	fssd 5736	. . . . . . . . . . . . . . . . . 18
46	45	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$
47	12	renegcli 9932	. . . . . . . . . . . . . . . . . . 19
48	47	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$
49	47	a1i 11	. . . . . . . . . . . . . . . . . . . 20
50		0red 9641	. . . . . . . . . . . . . . . . . . . . 21
51		negpilt0 37484	. . . . . . . . . . . . . . . . . . . . . 22
52	51	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
53		0xr 9684	. . . . . . . . . . . . . . . . . . . . . 22
54	12	rexri 9690	. . . . . . . . . . . . . . . . . . . . . 22
55		ioogtlb 37586	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
56	53, 54, 55	mp3an12 1353	. . . . . . . . . . . . . . . . . . . . 21
57	49, 50, 10, 52, 56	lttrd 9793	. . . . . . . . . . . . . . . . . . . 20
58	49, 10, 57	ltled 9780	. . . . . . . . . . . . . . . . . . 19
59	58	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$
60	13	leidd 10177	. . . . . . . . . . . . . . . . . 18 $/\$
61		iccss 11699	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
62	48, 13, 59, 60, 61	syl22anc 1268	. . . . . . . . . . . . . . . . 17 $/\$
63	46, 62	fssresd 5748	. . . . . . . . . . . . . . . 16 $/\$
64		fourierdlem104.o	. . . . . . . . . . . . . . . . . 18
65	64	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
66	65	feq1d 5712	. . . . . . . . . . . . . . . 16 $/\$
67	63, 66	mpbird 236	. . . . . . . . . . . . . . 15 $/\$
68		fourierdlem104.n	. . . . . . . . . . . . . . . . . 18
69	12	elexi 3054	. . . . . . . . . . . . . . . . . . . . . . . . 25
70	69	prid2 4080	. . . . . . . . . . . . . . . . . . . . . . . 24
71		elun1 3600	. . . . . . . . . . . . . . . . . . . . . . . 24
72	70, 71	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . 23
73		fourierdlem104.t	. . . . . . . . . . . . . . . . . . . . . . 23
74	72, 73	eleqtrri 2527	. . . . . . . . . . . . . . . . . . . . . 22
75	74	ne0ii 3737	. . . . . . . . . . . . . . . . . . . . 21
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . 20
77		prfi 7843	. . . . . . . . . . . . . . . . . . . . . . . 24
78	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
79		fzfi 12182	. . . . . . . . . . . . . . . . . . . . . . . . 25
80		fourierdlem104.q	. . . . . . . . . . . . . . . . . . . . . . . . . 26
81	80	rnmptfi 37429	. . . . . . . . . . . . . . . . . . . . . . . . 25
82	79, 81	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24
83		infi 7792	. . . . . . . . . . . . . . . . . . . . . . . 24
84	82, 83	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23
85		unfi 7835	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
86	78, 84, 85	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . 22
87	73, 86	syl5eqel 2532	. . . . . . . . . . . . . . . . . . . . 21
88		hashnncl 12544	. . . . . . . . . . . . . . . . . . . . 21
89	87, 88	syl 17	. . . . . . . . . . . . . . . . . . . 20
90	76, 89	mpbird 236	. . . . . . . . . . . . . . . . . . 19
91		nnm1nn0 10908	. . . . . . . . . . . . . . . . . . 19
92	90, 91	syl 17	. . . . . . . . . . . . . . . . . 18
93	68, 92	syl5eqel 2532	. . . . . . . . . . . . . . . . 17
94	93	adantr 467	. . . . . . . . . . . . . . . 16 $/\$
95		0red 9641	. . . . . . . . . . . . . . . . . 18 $/\$
96		1red 9655	. . . . . . . . . . . . . . . . . 18 $/\$
97	94	nn0red 10923	. . . . . . . . . . . . . . . . . 18 $/\$
98		0lt1 10133	. . . . . . . . . . . . . . . . . . 19
99	98	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$
100		2re 10676	. . . . . . . . . . . . . . . . . . . . 21
101	100	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
102	90	nnred 10621	. . . . . . . . . . . . . . . . . . . . 21
103	102	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$
104		iooltub 37604	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
105	53, 54, 104	mp3an12 1353	. . . . . . . . . . . . . . . . . . . . . . . . 25
106	10, 105	ltned 9768	. . . . . . . . . . . . . . . . . . . . . . . 24
107	106	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
108		hashprg 12569	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
109	11, 12, 108	sylancl 667	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
110	107, 109	mpbid 214	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
111	110	eqcomd 2456	. . . . . . . . . . . . . . . . . . . . 21 $/\$
112	87	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
113		ssun1 3596	. . . . . . . . . . . . . . . . . . . . . . 23
114	113, 73	sseqtr4i 3464	. . . . . . . . . . . . . . . . . . . . . 22
115		hashssle 37509	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
116	112, 114, 115	sylancl 667	. . . . . . . . . . . . . . . . . . . . 21 $/\$
117	111, 116	eqbrtrd 4422	. . . . . . . . . . . . . . . . . . . 20 $/\$
118	101, 103, 96, 117	lesub1dd 10226	. . . . . . . . . . . . . . . . . . 19 $/\$
119		1e2m1 10722	. . . . . . . . . . . . . . . . . . 19
120	118, 119, 68	3brtr4g 4434	. . . . . . . . . . . . . . . . . 18 $/\$
121	95, 96, 97, 99, 120	ltletrd 9792	. . . . . . . . . . . . . . . . 17 $/\$
122	121	gt0ne0d 10175	. . . . . . . . . . . . . . . 16 $/\$
123		elnnne0 10880	. . . . . . . . . . . . . . . 16 $/\$
124	94, 122, 123	sylanbrc 669	. . . . . . . . . . . . . . 15 $/\$
125		fourierdlem104.j	. . . . . . . . . . . . . . . . 17
126	11	leidd 10177	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
127	12	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
128	10, 127, 105	ltled 9780	. . . . . . . . . . . . . . . . . . . . . . 23
129	128	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
130	11, 13, 11, 126, 129	eliccd 37595	. . . . . . . . . . . . . . . . . . . . 21 $/\$
131	11, 13, 13, 129, 60	eliccd 37595	. . . . . . . . . . . . . . . . . . . . 21 $/\$
132	130, 131	jca 535	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
133		vex 3047	. . . . . . . . . . . . . . . . . . . . 21
134	133, 69	prss 4125	. . . . . . . . . . . . . . . . . . . 20 $/\$
135	132, 134	sylib 200	. . . . . . . . . . . . . . . . . . 19 $/\$
136		inss2 3652	. . . . . . . . . . . . . . . . . . . . 21
137	136	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
138		ioossicc 11717	. . . . . . . . . . . . . . . . . . . 20
139	137, 138	syl6ss 3443	. . . . . . . . . . . . . . . . . . 19 $/\$
140	135, 139	unssd 3609	. . . . . . . . . . . . . . . . . 18 $/\$
141	73, 140	syl5eqss 3475	. . . . . . . . . . . . . . . . 17 $/\$
142	133	prid1 4079	. . . . . . . . . . . . . . . . . . . 20
143		elun1 3600	. . . . . . . . . . . . . . . . . . . 20
144	142, 143	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
145	144, 73	eleqtrri 2527	. . . . . . . . . . . . . . . . . 18
146	145	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
147	74	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
148	112, 68, 125, 11, 13, 141, 146, 147	fourierdlem52 38016	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
149	148	simplld 760	. . . . . . . . . . . . . . 15 $/\$
150	148	simplrd 762	. . . . . . . . . . . . . . 15 $/\$
151	148	simprd 465	. . . . . . . . . . . . . . 15 $/\$
152		elfzoelz 11917	. . . . . . . . . . . . . . . . . . 19 ..^
153	152	zred 11037	. . . . . . . . . . . . . . . . . 18 ..^
154	153	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
155	154	ltp1d 10534	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
156	10, 127	jca 535	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
157	133, 69	prss 4125	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158	156, 157	sylib 200	. . . . . . . . . . . . . . . . . . . . . 22
159	158	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 $/\$
160		ioossre 11693	. . . . . . . . . . . . . . . . . . . . . . 23
161	136, 160	sstri 3440	. . . . . . . . . . . . . . . . . . . . . 22
162	161	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
163	159, 162	unssd 3609	. . . . . . . . . . . . . . . . . . . 20 $/\$
164	73, 163	syl5eqss 3475	. . . . . . . . . . . . . . . . . . 19 $/\$
165	112, 164, 125, 68	fourierdlem36 38000	. . . . . . . . . . . . . . . . . 18 $/\$
166	165	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
167		elfzofz 11932	. . . . . . . . . . . . . . . . . 18 ..^
168	167	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
169		fzofzp1 12005	. . . . . . . . . . . . . . . . . 18 ..^
170	169	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
171		isorel 6215	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
172	166, 168, 170, 171	syl12anc 1265	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
173	155, 172	mpbid 214	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^
174	42	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$
175	174, 62	feqresmpt 5917	. . . . . . . . . . . . . . . . . . 19 $/\$
176	62	sselda 3431	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
177	14, 15, 27, 38, 39	fourierdlem9 37972	. . . . . . . . . . . . . . . . . . . . . . . . 25
178	177	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
179	178, 176	ffvelrnd 6021	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
180	40	fourierdlem43 38008	. . . . . . . . . . . . . . . . . . . . . . . . 25
181	180	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
182	181, 176	ffvelrnd 6021	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
183	179, 182	remulcld 9668	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
184	41	fvmpt2 5955	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
185	176, 183, 184	syl2anc 666	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
186		0red 9641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
187	10	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
188	12	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
189		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
190		eliccre 37597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
191	187, 188, 189, 190	syl3anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
192	56	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
193	187	rexrd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
194	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
195		iccgelb 11688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
196	193, 194, 189, 195	syl3anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
197	186, 187, 191, 192, 196	ltletrd 9792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
198	197	gt0ne0d 10175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
199	198	adantll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
200	199	neneqd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
201	200	iffalsed 3891	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
202	197	adantll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
203	202	iftrued 3888	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
204	203	oveq2d 6304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
205	204	oveq1d 6303	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
206	201, 205	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
207	14	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
208	15	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
209		iccssre 11713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
210	47, 12, 209	mp2an 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
211	210, 176	sseldi 3429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
212	208, 211	readdcld 9667	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
213	207, 212	ffvelrnd 6021	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
214	27	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
215	213, 214	resubcld 10044	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
216	215, 211, 199	redivcld 10432	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
217	206, 216	eqeltrd 2528	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
218	39	fvmpt2 5955	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
219	176, 217, 218	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
220	219, 201, 205	3eqtrd 2488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
221	188	renegcld 10043	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
222	51	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
223	221, 186, 191, 222, 197	lttrd 9793	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
224	221, 191, 223	ltled 9780	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
225		iccleub 11687	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
226	193, 194, 189, 225	syl3anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
227	221, 188, 191, 224, 226	eliccd 37595	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
228	198	neneqd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
229	228	iffalsed 3891	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
230	100	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
231	191	rehalfcld 10856	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
232	231	resincld 14190	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
233	230, 232	remulcld 9668	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
234		2cnd 10679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
235	191	recnd 9666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
236	235	halfcld 10854	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
237	236	sincld 14177	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
238		2ne0 10699	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
239	238	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
240		fourierdlem44 38009	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
241	227, 198, 240	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
242	234, 237, 239, 241	mulne0d 10261	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
243	191, 233, 242	redivcld 10432	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
244	229, 243	eqeltrd 2528	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
245	40	fvmpt2 5955	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
246	227, 244, 245	syl2anc 666	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
247	246	adantll 719	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
248	220, 247	oveq12d 6306	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
249	200	iffalsed 3891	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
250	249	oveq2d 6304	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
251	185, 248, 250	3eqtrd 2488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
252	251	mpteq2dva 4488	. . . . . . . . . . . . . . . . . . 19 $/\$
253	65, 175, 252	3eqtrd 2488	. . . . . . . . . . . . . . . . . 18 $/\$
254	253	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
255	254	reseq1d 5103	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
256	14	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
257	15	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
258		fourierdlem104.p	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
259		fourierdlem104.m	. . . . . . . . . . . . . . . . . . 19
260	259	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
261		fourierdlem104.v	. . . . . . . . . . . . . . . . . . 19
262	261	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
263		fourierdlem104.fcn	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
264	263	adantlr 720	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
265		fourierdlem104.r	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ lim
266	265	adantlr 720	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^ lim
267		fourierdlem104.l	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ lim
268	267	adantlr 720	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^ lim
269	105	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$
270	50, 10	ltnled 9779	. . . . . . . . . . . . . . . . . . . . . 22
271	56, 270	mpbid 214	. . . . . . . . . . . . . . . . . . . . 21
272	271	intn3an2d 1379	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
273		elicc2 11696	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
274	10, 12, 273	sylancl 667	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
275	272, 274	mtbird 303	. . . . . . . . . . . . . . . . . . 19
276	275	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$
277	27	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$
278		eqid 2450	. . . . . . . . . . . . . . . . . 18
279		eqid 2450	. . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
280		eqid 2450	. . . . . . . . . . . . . . . . . 18 ..^ ..^ ..^ ..^
281		fveq2 5863	. . . . . . . . . . . . . . . . . . . . 21
282		oveq1 6295	. . . . . . . . . . . . . . . . . . . . . 22
283	282	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . 21
284	281, 283	oveq12d 6306	. . . . . . . . . . . . . . . . . . . 20
285	284	sseq2d 3459	. . . . . . . . . . . . . . . . . . 19
286	285	cbvriotav 6261	. . . . . . . . . . . . . . . . . 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 38050	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^ ..^ ..^ lim $/\$ ..^ ..^ lim $/\$
288	287	simprd 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^
289	255, 288	eqeltrd 2528	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^
290	287	simplld 760	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^ ..^ ..^ lim
291	254	eqcomd 2456	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ ..^
292	291	reseq1d 5103	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ ..^
293	292	oveq1d 6303	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^ lim lim
294	290, 293	eleqtrd 2530	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^ ..^ ..^ lim
295	287	simplrd 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^ ..^ ..^ lim
296	292	oveq1d 6303	. . . . . . . . . . . . . . . 16 $/\$ $/\$ ..^ lim lim
297	295, 296	eleqtrd 2530	. . . . . . . . . . . . . . 15 $/\$ $/\$ ..^ ..^ ..^ lim
298		eqid 2450	. . . . . . . . . . . . . . 15
299	67	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
300	11	ad2antrr 731	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
301	12	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
302		elioore 11663	. . . . . . . . . . . . . . . . . . . . . . . 24
303	302	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
304	62, 210	syl6ss 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
305	304	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
306	149	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
307	306, 168	ffvelrnd 6021	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
308	305, 307	sseldd 3432	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^
309	308	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
310	11	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
311	310	rexrd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
312	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
313		iccgelb 11688	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
314	311, 312, 307, 313	syl3anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^
315	314	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
316	309	rexrd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^ $/\$
317	306, 170	ffvelrnd 6021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ ..^
318	305, 317	sseldd 3432	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ ..^
319	318	rexrd 9687	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ ..^
320	319	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^ $/\$
321		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^ $/\$
322		ioogtlb 37586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
323	316, 320, 321, 322	syl3anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
324	300, 309, 303, 315, 323	lelttrd 9790	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$
325	300, 303, 324	ltled 9780	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
326	318	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
327		iooltub 37604	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
328	316, 320, 321, 327	syl3anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
329		iccleub 11687	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
330	311, 312, 317, 329	syl3anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ ..^
331	330	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^ $/\$
332	303, 326, 301, 328, 331	ltletrd 9792	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^ $/\$
333	303, 301, 332	ltled 9780	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ ..^ $/\$
334	300, 301, 303, 325, 333	eliccd 37595	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
335	334	ralrimiva 2801	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^
336		dfss3 3421	. . . . . . . . . . . . . . . . . . . . 21
337	335, 336	sylibr 216	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ ..^
338	299, 337	feqresmpt 5917	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ ..^
339		simplll 767	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
340		simpllr 768	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
341	64	fveq1i 5864	. . . . . . . . . . . . . . . . . . . . . . . 24
342	341	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
343		fvres 5877	. . . . . . . . . . . . . . . . . . . . . . . 24
344	343	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
345	247, 249	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
346	220, 345	oveq12d 6306	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
347	215	recnd 9666	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
348	235	adantll 719	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
349		2cnd 10679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
350	348	halfcld 10854	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
351	350	sincld 14177	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
352	349, 351	mulcld 9660	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
353	242	adantll 719	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
354	347, 348, 352, 199, 353	dmdcan2d 10410	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
355	185, 346, 354	3eqtrd 2488	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
356	342, 344, 355	3eqtrd 2488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
357	339, 340, 334, 356	syl21anc 1266	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
358	339, 340, 334, 354	syl21anc 1266	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ ..^ $/\$
359	358	eqcomd 2456	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ ..^ $/\$
360		eqidd 2451	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
361		oveq2 6296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
362	361	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
363	362	oveq1d 6303	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
364		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
365	363, 364	oveq12d 6306	. . . . . . . . . . . . . . . . . . . . . . . . . 26
366	365	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
367		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
368		ovex 6316	. . . . . . . . . . . . . . . . . . . . . . . . . 26
369	368	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
370	360, 366, 367, 369	fvmptd 5952	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
371		eqidd 2451	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
372		oveq1 6295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
373	372	fveq2d 5867	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
374	373	oveq2d 6304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
375	364, 374	oveq12d 6306	. . . . . . . . . . . . . . . . . . . . . . . . . 26
376	375	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$