fourierdlem81 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem81 40404

Description: The integral of a piecewise continuous periodic function

is unchanged if the domain is shifted by its period

. In this lemma,

is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem81.a
fourierdlem81.b
fourierdlem81.p	$/\$ $/\$ ..^
fourierdlem81.m
fourierdlem81.t
fourierdlem81.q
fourierdlem81.fper	$/\$
fourierdlem81.s
fourierdlem81.f
fourierdlem81.cncf	$/\$ ..^
fourierdlem81.r	$/\$ ..^ lim
fourierdlem81.l	$/\$ ..^ lim
fourierdlem81.g
fourierdlem81.h

**Assertion**
Ref	Expression
fourierdlem81

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem fourierdlem81 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem81.q	. . . . . . . . 9
2		fourierdlem81.m	. . . . . . . . . 10
3		fourierdlem81.p	. . . . . . . . . . 11 $/\$ $/\$ ..^
4	3	fourierdlem2 40326	. . . . . . . . . 10 $/\$ $/\$ $/\$ ..^
5	2, 4	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ ..^
6	1, 5	mpbid 222	. . . . . . . 8 $/\$ $/\$ $/\$ ..^
7	6	simprd 479	. . . . . . 7 $/\$ $/\$ ..^
8	7	simpld 475	. . . . . 6 $/\$
9	8	simpld 475	. . . . 5
10	9	eqcomd 2628	. . . 4
11	8	simprd 479	. . . . 5
12	11	eqcomd 2628	. . . 4
13	10, 12	oveq12d 6668	. . 3
14	13	itgeq1d 40172	. 2
15		0zd 11389	. . 3
16		nnuz 11723	. . . . 5
17		0p1e1 11132	. . . . . 6
18	17	fveq2i 6194	. . . . 5
19	16, 18	eqtr4i 2647	. . . 4
20	2, 19	syl6eleq 2711	. . 3
21	6	simpld 475	. . . 4
22		reex 10027	. . . . . 6
23	22	a1i 11	. . . . 5
24		ovex 6678	. . . . . 6
25	24	a1i 11	. . . . 5
26	23, 25	elmapd 7871	. . . 4
27	21, 26	mpbid 222	. . 3
28	7	simprd 479	. . . 4 ..^
29	28	r19.21bi 2932	. . 3 $/\$ ..^
30		fourierdlem81.f	. . . . 5
31	30	adantr 481	. . . 4 $/\$
32		fourierdlem81.a	. . . . . . 7
33	9, 32	eqeltrd 2701	. . . . . 6
34		fourierdlem81.b	. . . . . . 7
35	11, 34	eqeltrd 2701	. . . . . 6
36	33, 35	iccssred 39727	. . . . 5
37	36	sselda 3603	. . . 4 $/\$
38	31, 37	ffvelrnd 6360	. . 3 $/\$
39	27	adantr 481	. . . . 5 $/\$ ..^
40		elfzofz 12485	. . . . . 6 ..^
41	40	adantl 482	. . . . 5 $/\$ ..^
42	39, 41	ffvelrnd 6360	. . . 4 $/\$ ..^
43		fzofzp1 12565	. . . . . 6 ..^
44	43	adantl 482	. . . . 5 $/\$ ..^
45	39, 44	ffvelrnd 6360	. . . 4 $/\$ ..^
46	30	feqmptd 6249	. . . . . . . 8
47	46	reseq1d 5395	. . . . . . 7
48	47	adantr 481	. . . . . 6 $/\$ ..^
49		ioossre 12235	. . . . . . . 8
50	49	a1i 11	. . . . . . 7 $/\$ ..^
51	50	resmptd 5452	. . . . . 6 $/\$ ..^
52	48, 51	eqtr2d 2657	. . . . 5 $/\$ ..^
53		fourierdlem81.cncf	. . . . . 6 $/\$ ..^
54		fourierdlem81.l	. . . . . 6 $/\$ ..^ lim
55		fourierdlem81.r	. . . . . 6 $/\$ ..^ lim
56	42, 45, 53, 54, 55	iblcncfioo 40194	. . . . 5 $/\$ ..^
57	52, 56	eqeltrd 2701	. . . 4 $/\$ ..^
58	30	ad2antrr 762	. . . . 5 $/\$ ..^ $/\$
59	42, 45	iccssred 39727	. . . . . 6 $/\$ ..^
60	59	sselda 3603	. . . . 5 $/\$ ..^ $/\$
61	58, 60	ffvelrnd 6360	. . . 4 $/\$ ..^ $/\$
62	42, 45, 57, 61	ibliooicc 40187	. . 3 $/\$ ..^
63	15, 20, 27, 29, 38, 62	itgspltprt 40195	. 2 ..^
64		fourierdlem81.s	. . . . . . . 8
65	64	a1i 11	. . . . . . 7
66		fveq2 6191	. . . . . . . . 9
67	66	oveq1d 6665	. . . . . . . 8
68	67	adantl 482	. . . . . . 7 $/\$
69	2	nnnn0d 11351	. . . . . . . . 9
70		nn0uz 11722	. . . . . . . . 9
71	69, 70	syl6eleq 2711	. . . . . . . 8
72		eluzfz1 12348	. . . . . . . 8
73	71, 72	syl 17	. . . . . . 7
74		fourierdlem81.t	. . . . . . . . 9
75	74	rpred 11872	. . . . . . . 8
76	33, 75	readdcld 10069	. . . . . . 7
77	65, 68, 73, 76	fvmptd 6288	. . . . . 6
78	9	oveq1d 6665	. . . . . 6
79	77, 78	eqtr2d 2657	. . . . 5
80		fveq2 6191	. . . . . . . . 9
81	80	oveq1d 6665	. . . . . . . 8
82	81	adantl 482	. . . . . . 7 $/\$
83		eluzfz2 12349	. . . . . . . 8
84	71, 83	syl 17	. . . . . . 7
85	35, 75	readdcld 10069	. . . . . . 7
86	65, 82, 84, 85	fvmptd 6288	. . . . . 6
87	11	oveq1d 6665	. . . . . 6
88	86, 87	eqtr2d 2657	. . . . 5
89	79, 88	oveq12d 6668	. . . 4
90	89	itgeq1d 40172	. . 3
91	27	ffvelrnda 6359	. . . . . 6 $/\$
92	75	adantr 481	. . . . . 6 $/\$
93	91, 92	readdcld 10069	. . . . 5 $/\$
94	93, 64	fmptd 6385	. . . 4
95	75	adantr 481	. . . . . 6 $/\$ ..^
96	42, 45, 95, 29	ltadd1dd 10638	. . . . 5 $/\$ ..^
97	40, 93	sylan2 491	. . . . . 6 $/\$ ..^
98	64	fvmpt2 6291	. . . . . 6 $/\$
99	41, 97, 98	syl2anc 693	. . . . 5 $/\$ ..^
100		fveq2 6191	. . . . . . . . . 10
101	100	oveq1d 6665	. . . . . . . . 9
102	101	cbvmptv 4750	. . . . . . . 8
103	64, 102	eqtri 2644	. . . . . . 7
104	103	a1i 11	. . . . . 6 $/\$ ..^
105		fveq2 6191	. . . . . . . 8
106	105	oveq1d 6665	. . . . . . 7
107	106	adantl 482	. . . . . 6 $/\$ ..^ $/\$
108	45, 95	readdcld 10069	. . . . . 6 $/\$ ..^
109	104, 107, 44, 108	fvmptd 6288	. . . . 5 $/\$ ..^
110	96, 99, 109	3brtr4d 4685	. . . 4 $/\$ ..^
111	30	adantr 481	. . . . 5 $/\$
112	77, 76	eqeltrd 2701	. . . . . . . 8
113	112	adantr 481	. . . . . . 7 $/\$
114	86, 85	eqeltrd 2701	. . . . . . . 8
115	114	adantr 481	. . . . . . 7 $/\$
116	113, 115	iccssred 39727	. . . . . 6 $/\$
117		simpr 477	. . . . . 6 $/\$
118	116, 117	sseldd 3604	. . . . 5 $/\$
119	111, 118	ffvelrnd 6360	. . . 4 $/\$
120	99, 97	eqeltrd 2701	. . . . 5 $/\$ ..^
121	109, 108	eqeltrd 2701	. . . . 5 $/\$ ..^
122		ioosscn 39716	. . . . . . . . 9
123	122	a1i 11	. . . . . . . 8 $/\$ ..^
124		eqeq1 2626	. . . . . . . . . . 11
125	124	rexbidv 3052	. . . . . . . . . 10
126		oveq1 6657	. . . . . . . . . . . 12
127	126	eqeq2d 2632	. . . . . . . . . . 11
128	127	cbvrexv 3172	. . . . . . . . . 10
129	125, 128	syl6bb 276	. . . . . . . . 9
130	129	cbvrabv 3199	. . . . . . . 8
131		fdm 6051	. . . . . . . . . . . 12
132	30, 131	syl 17	. . . . . . . . . . 11
133	132	feq2d 6031	. . . . . . . . . 10
134	30, 133	mpbird 247	. . . . . . . . 9
135	134	adantr 481	. . . . . . . 8 $/\$ ..^
136		elioore 12205	. . . . . . . . . . . . . . . . . 18
137	136	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
138	75	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
139	137, 138	readdcld 10069	. . . . . . . . . . . . . . . 16 $/\$
140	139	adantlr 751	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
141	140	3adant3 1081	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
142		simp3 1063	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
143	132	3ad2ant1 1082	. . . . . . . . . . . . . . 15 $/\$ $/\$
144	143	3adant1r 1319	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
145	141, 142, 144	3eltr4d 2716	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
146	145	3exp 1264	. . . . . . . . . . . 12 $/\$ ..^
147	146	adantr 481	. . . . . . . . . . 11 $/\$ ..^ $/\$
148	147	rexlimdv 3030	. . . . . . . . . 10 $/\$ ..^ $/\$
149	148	ralrimiva 2966	. . . . . . . . 9 $/\$ ..^
150		rabss 3679	. . . . . . . . 9
151	149, 150	sylibr 224	. . . . . . . 8 $/\$ ..^
152		simpll 790	. . . . . . . . 9 $/\$ ..^ $/\$
153	32	rexrd 10089	. . . . . . . . . . 11
154	153	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$
155	34	rexrd 10089	. . . . . . . . . . 11
156	155	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$
157	3, 2, 1	fourierdlem15 40339	. . . . . . . . . . 11
158	157	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$
159		simplr 792	. . . . . . . . . 10 $/\$ ..^ $/\$ ..^
160		ioossicc 12259	. . . . . . . . . . . 12
161	160	sseli 3599	. . . . . . . . . . 11
162	161	adantl 482	. . . . . . . . . 10 $/\$ ..^ $/\$
163	154, 156, 158, 159, 162	fourierdlem1 40325	. . . . . . . . 9 $/\$ ..^ $/\$
164		fourierdlem81.fper	. . . . . . . . 9 $/\$
165	152, 163, 164	syl2anc 693	. . . . . . . 8 $/\$ ..^ $/\$
166	123, 95, 130, 135, 151, 165, 53	cncfperiod 40092	. . . . . . 7 $/\$ ..^
167	125	elrab 3363	. . . . . . . . . . . . 13 $/\$
168	167	simprbi 480	. . . . . . . . . . . 12
169		simpr 477	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
170		nfv 1843	. . . . . . . . . . . . . . . 16 $/\$ ..^
171		nfre1 3005	. . . . . . . . . . . . . . . 16
172	170, 171	nfan 1828	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
173		nfv 1843	. . . . . . . . . . . . . . 15 $/\$ $/\$
174		simp3 1063	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
175	139	3adant3 1081	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
176	174, 175	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
177	176	3adant1r 1319	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
178	42	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
179	136	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
180	75	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
181		simpr 477	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
182	42	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^
183	182	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
184	45	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^
185	184	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
186		elioo2 12216	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
187	183, 185, 186	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$ $/\$
188	181, 187	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
189	188	simp2d 1074	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
190	178, 179, 180, 189	ltadd1dd 10638	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
191	190	3adant3 1081	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
192	99	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
193		simp3 1063	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
194	191, 192, 193	3brtr4d 4685	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
195	45	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
196	188	simp3d 1075	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
197	179, 195, 180, 196	ltadd1dd 10638	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
198	197	3adant3 1081	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
199	109	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
200	198, 193, 199	3brtr4d 4685	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
201	177, 194, 200	3jca 1242	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
202	201	3exp 1264	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$
203	202	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$
204	172, 173, 203	rexlimd 3026	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
205	169, 204	mpd 15	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
206	120	rexrd 10089	. . . . . . . . . . . . . . 15 $/\$ ..^
207	206	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
208	121	rexrd 10089	. . . . . . . . . . . . . . 15 $/\$ ..^
209	208	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
210		elioo2 12216	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
211	207, 209, 210	syl2anc 693	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
212	205, 211	mpbird 247	. . . . . . . . . . . 12 $/\$ ..^ $/\$
213	168, 212	sylan2 491	. . . . . . . . . . 11 $/\$ ..^ $/\$
214		elioore 12205	. . . . . . . . . . . . . 14
215	214	recnd 10068	. . . . . . . . . . . . 13
216	215	adantl 482	. . . . . . . . . . . 12 $/\$ ..^ $/\$
217	182	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
218	184	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
219	214	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
220	75	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
221	219, 220	resubcld 10458	. . . . . . . . . . . . . . 15 $/\$
222	221	adantlr 751	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
223	99	oveq1d 6665	. . . . . . . . . . . . . . . . 17 $/\$ ..^
224	42	recnd 10068	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
225	95	recnd 10068	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
226	224, 225	pncand 10393	. . . . . . . . . . . . . . . . 17 $/\$ ..^
227	223, 226	eqtr2d 2657	. . . . . . . . . . . . . . . 16 $/\$ ..^
228	227	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
229	120	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
230	214	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
231	75	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
232		simpr 477	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
233	206	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
234	208	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
235	233, 234, 210	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
236	232, 235	mpbid 222	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
237	236	simp2d 1074	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
238	229, 230, 231, 237	ltsub1dd 10639	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
239	228, 238	eqbrtrd 4675	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
240	121	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
241	236	simp3d 1075	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
242	230, 240, 231, 241	ltsub1dd 10639	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
243	109	oveq1d 6665	. . . . . . . . . . . . . . . . 17 $/\$ ..^
244	45	recnd 10068	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
245	244, 225	pncand 10393	. . . . . . . . . . . . . . . . 17 $/\$ ..^
246	243, 245	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$ ..^
247	246	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
248	242, 247	breqtrd 4679	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
249	217, 218, 222, 239, 248	eliood 39720	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
250	219	recnd 10068	. . . . . . . . . . . . . . . 16 $/\$
251	220	recnd 10068	. . . . . . . . . . . . . . . 16 $/\$
252	250, 251	npcand 10396	. . . . . . . . . . . . . . 15 $/\$
253	252	eqcomd 2628	. . . . . . . . . . . . . 14 $/\$
254	253	adantlr 751	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
255		oveq1 6657	. . . . . . . . . . . . . . 15
256	255	eqeq2d 2632	. . . . . . . . . . . . . 14
257	256	rspcev 3309	. . . . . . . . . . . . 13 $/\$
258	249, 254, 257	syl2anc 693	. . . . . . . . . . . 12 $/\$ ..^ $/\$
259	216, 258, 167	sylanbrc 698	. . . . . . . . . . 11 $/\$ ..^ $/\$
260	213, 259	impbida 877	. . . . . . . . . 10 $/\$ ..^
261	260	eqrdv 2620	. . . . . . . . 9 $/\$ ..^
262	261	reseq2d 5396	. . . . . . . 8 $/\$ ..^
263	30	adantr 481	. . . . . . . . 9 $/\$ ..^
264		ioossre 12235	. . . . . . . . . 10
265	264	a1i 11	. . . . . . . . 9 $/\$ ..^
266	263, 265	feqresmpt 6250	. . . . . . . 8 $/\$ ..^
267	262, 266	eqtrd 2656	. . . . . . 7 $/\$ ..^
268	261	oveq1d 6665	. . . . . . 7 $/\$ ..^
269	166, 267, 268	3eltr3d 2715	. . . . . 6 $/\$ ..^
270	49, 132	syl5sseqr 3654	. . . . . . . . 9
271	270	adantr 481	. . . . . . . 8 $/\$ ..^
272		eqid 2622	. . . . . . . 8
273		simpll 790	. . . . . . . . 9 $/\$ ..^ $/\$
274	153	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$
275	155	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$
276	157	ad2antrr 762	. . . . . . . . . 10 $/\$ ..^ $/\$
277		simplr 792	. . . . . . . . . 10 $/\$ ..^ $/\$ ..^
278	160, 181	sseldi 3601	. . . . . . . . . 10 $/\$ ..^ $/\$
279	274, 275, 276, 277, 278	fourierdlem1 40325	. . . . . . . . 9 $/\$ ..^ $/\$
280		eleq1 2689	. . . . . . . . . . . 12
281	280	anbi2d 740	. . . . . . . . . . 11 $/\$ $/\$
282		oveq1 6657	. . . . . . . . . . . . 13
283	282	fveq2d 6195	. . . . . . . . . . . 12
284		fveq2 6191	. . . . . . . . . . . 12
285	283, 284	eqeq12d 2637	. . . . . . . . . . 11
286	281, 285	imbi12d 334	. . . . . . . . . 10 $/\$ $/\$
287	286, 164	chvarv 2263	. . . . . . . . 9 $/\$
288	273, 279, 287	syl2anc 693	. . . . . . . 8 $/\$ ..^ $/\$
289	135, 123, 271, 225, 272, 151, 288, 54	limcperiod 39860	. . . . . . 7 $/\$ ..^ lim
290	109	eqcomd 2628	. . . . . . . 8 $/\$ ..^
291	267, 290	oveq12d 6668	. . . . . . 7 $/\$ ..^ lim lim
292	289, 291	eleqtrd 2703	. . . . . 6 $/\$ ..^ lim
293	135, 123, 271, 225, 272, 151, 288, 55	limcperiod 39860	. . . . . . 7 $/\$ ..^ lim
294	99	eqcomd 2628	. . . . . . . 8 $/\$ ..^
295	267, 294	oveq12d 6668	. . . . . . 7 $/\$ ..^ lim lim
296	293, 295	eleqtrd 2703	. . . . . 6 $/\$ ..^ lim
297	120, 121, 269, 292, 296	iblcncfioo 40194	. . . . 5 $/\$ ..^
298	30	ad2antrr 762	. . . . . 6 $/\$ ..^ $/\$
299	120	adantr 481	. . . . . . 7 $/\$ ..^ $/\$
300	121	adantr 481	. . . . . . 7 $/\$ ..^ $/\$
301		simpr 477	. . . . . . 7 $/\$ ..^ $/\$
302		eliccre 39728	. . . . . . 7 $/\$ $/\$
303	299, 300, 301, 302	syl3anc 1326	. . . . . 6 $/\$ ..^ $/\$
304	298, 303	ffvelrnd 6360	. . . . 5 $/\$ ..^ $/\$
305	120, 121, 297, 304	ibliooicc 40187	. . . 4 $/\$ ..^
306	15, 20, 94, 110, 119, 305	itgspltprt 40195	. . 3 ..^
307		iftrue 4092	. . . . . . . . . . . 12
308	307	adantl 482	. . . . . . . . . . 11 $/\$ ..^ $/\$
309		fourierdlem81.g	. . . . . . . . . . . . . . 15
310		iftrue 4092	. . . . . . . . . . . . . . . . . . 19
311		iftrue 4092	. . . . . . . . . . . . . . . . . . 19
312	310, 311	eqtr4d 2659	. . . . . . . . . . . . . . . . . 18
313	312	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
314		iffalse 4095	. . . . . . . . . . . . . . . . . . . . 21
315	314	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
316		iftrue 4092	. . . . . . . . . . . . . . . . . . . . 21
317	316	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
318		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . 22
319	318	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
320		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . 22
321	320	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
322	319, 321	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . 20 $/\$
323	315, 317, 322	3eqtrd 2660	. . . . . . . . . . . . . . . . . . 19 $/\$
324	323	adantll 750	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
325	314	ad2antlr 763	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
326		iffalse 4095	. . . . . . . . . . . . . . . . . . . 20
327	326	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
328	318	ad2antlr 763	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$
329		iffalse 4095	. . . . . . . . . . . . . . . . . . . . 21
330	329	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$
331	182	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
332	184	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
333	60	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
334	42	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
335	60	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
336	182	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
337	184	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
338		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
339		iccgelb 12230	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
340	336, 337, 338, 339	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
341		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . 25
342	341	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
343	334, 335, 340, 342	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
344	343	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
345	45	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$ $/\$
346	182	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
347	184	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
348		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
349		iccleub 12229	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
350	346, 347, 348, 349	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$
351	350	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$ $/\$
352		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . 25
353	352	necomd 2849	. . . . . . . . . . . . . . . . . . . . . . . 24
354	353	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$ $/\$
355	333, 345, 351, 354	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
356	331, 332, 333, 344, 355	eliood 39720	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$
357		fvres 6207	. . . . . . . . . . . . . . . . . . . . 21
358	356, 357	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$
359	328, 330, 358	3eqtrrd 2661	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
360	325, 327, 359	3eqtrd 2660	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
361	324, 360	pm2.61dan 832	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
362	313, 361	pm2.61dan 832	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
363	362	mpteq2dva 4744	. . . . . . . . . . . . . . 15 $/\$ ..^
364	309, 363	syl5eq 2668	. . . . . . . . . . . . . 14 $/\$ ..^
365		eqeq1 2626	. . . . . . . . . . . . . . . 16
366		eqeq1 2626	. . . . . . . . . . . . . . . . 17
367		fveq2 6191	. . . . . . . . . . . . . . . . 17
368	366, 367	ifbieq2d 4111	. . . . . . . . . . . . . . . 16
369	365, 368	ifbieq2d 4111	. . . . . . . . . . . . . . 15
370	369	cbvmptv 4750	. . . . . . . . . . . . . 14
371	364, 370	syl6eq 2672	. . . . . . . . . . . . 13 $/\$ ..^
372	371	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$
373		simpr 477	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
374		oveq1 6657	. . . . . . . . . . . . . . 15
375	374	ad2antlr 763	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
376	227	eqcomd 2628	. . . . . . . . . . . . . . 15 $/\$ ..^
377	376	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
378	373, 375, 377	3eqtrd 2660	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
379	378	iftrued 4094	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
380	374	adantl 482	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
381	42, 45, 29	ltled 10185	. . . . . . . . . . . . . . . 16 $/\$ ..^
382		lbicc2 12288	. . . . . . . . . . . . . . . 16 $/\$ $/\$
383	182, 184, 381, 382	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$ ..^
384	376, 383	eqeltrd 2701	. . . . . . . . . . . . . 14 $/\$ ..^
385	384	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
386	380, 385	eqeltrd 2701	. . . . . . . . . . . 12 $/\$ ..^ $/\$
387		limccl 23639	. . . . . . . . . . . . . 14 lim
388	387, 55	sseldi 3601	. . . . . . . . . . . . 13 $/\$ ..^
389	388	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$
390	372, 379, 386, 389	fvmptd 6288	. . . . . . . . . . 11 $/\$ ..^ $/\$
391	308, 390	eqtr4d 2659	. . . . . . . . . 10 $/\$ ..^ $/\$
392	391	adantlr 751	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$
393		iffalse 4095	. . . . . . . . . . 11
394	393	adantl 482	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
395	371	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
396		eqeq1 2626	. . . . . . . . . . . . . . . . . 18
397		eqeq1 2626	. . . . . . . . . . . . . . . . . . 19
398		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
399	397, 398	ifbieq2d 4111	. . . . . . . . . . . . . . . . . 18
400	396, 399	ifbieq2d 4111	. . . . . . . . . . . . . . . . 17
401	400	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
402		eqeq1 2626	. . . . . . . . . . . . . . . . . . 19
403		iftrue 4092	. . . . . . . . . . . . . . . . . . 19
404	402, 403	ifbieq2d 4111	. . . . . . . . . . . . . . . . . 18
405	246, 404	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ ..^
406	405	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
407	42, 29	gtned 10172	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
408	407	neneqd 2799	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
409	408	iffalsed 4097	. . . . . . . . . . . . . . . . 17 $/\$ ..^
410	409	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
411	401, 406, 410	3eqtrd 2660	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
412	411	adantlr 751	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$
413		ubicc2 12289	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
414	182, 184, 381, 413	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$ ..^
415	246, 414	eqeltrd 2701	. . . . . . . . . . . . . . 15 $/\$ ..^
416	415	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
417		limccl 23639	. . . . . . . . . . . . . . . 16 lim
418	417, 54	sseldi 3601	. . . . . . . . . . . . . . 15 $/\$ ..^
419	418	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
420	395, 412, 416, 419	fvmptd 6288	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
421		oveq1 6657	. . . . . . . . . . . . . . 15
422	421	fveq2d 6195	. . . . . . . . . . . . . 14
423	422	adantl 482	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
424		iftrue 4092	. . . . . . . . . . . . . 14
425	424	adantl 482	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
426	420, 423, 425	3eqtr4rd 2667	. . . . . . . . . . . 12 $/\$ ..^ $/\$
427	426	ad4ant14 1293	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$ $/\$
428		iffalse 4095	. . . . . . . . . . . . 13
429	428	adantl 482	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$ $/\$
430	371	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
431	430	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$
432		eqeq1 2626	. . . . . . . . . . . . . . . . . 18
433		eqeq1 2626	. . . . . . . . . . . . . . . . . . 19
434		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
435	433, 434	ifbieq2d 4111	. . . . . . . . . . . . . . . . . 18
436	432, 435	ifbieq2d 4111	. . . . . . . . . . . . . . . . 17
437	436	adantl 482	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
438	303	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
439	225	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$
440	438, 439	npcand 10396	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
441	440	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
442	441	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
443		oveq1 6657	. . . . . . . . . . . . . . . . . . . . 21
444	443	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
445	294	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
446	442, 444, 445	3eqtrd 2660	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
447	446	stoic1a 1697	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
448	447	iffalsed 4097	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
449	448	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
450	441	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
451		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
452	451	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
453	290	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
454	450, 452, 453	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
455	454	stoic1a 1697	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
456	455	iffalsed 4097	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
457	456	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
458	457	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
459	437, 449, 458	3eqtrd 2660	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
460	42	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
461	45	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
462	75	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
463	303, 462	resubcld 10458	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
464	227	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
465	206	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
466	208	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$
467		iccgelb 12230	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
468	465, 466, 301, 467	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
469	299, 303, 462, 468	lesub1dd 10643	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
470	464, 469	eqbrtrd 4675	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
471		iccleub 12229	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
472	465, 466, 301, 471	syl3anc 1326	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$
473	303, 300, 462, 472	lesub1dd 10643	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
474	246	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
475	473, 474	breqtrd 4679	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
476	460, 461, 463, 470, 475	eliccd 39726	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
477	476	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$
478	135, 271	fssresd 6071	. . . . . . . . . . . . . . . . 17 $/\$ ..^
479	478	ad3antrrr 766	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
480	182	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
481	184	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
482	303	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
483	95	ad3antrrr 766	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
484	482, 483	resubcld 10458	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
485	42	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
486	463	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
487	470	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
488	447	neqned 2801	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
489	485, 486, 487, 488	leneltd 10191	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
490	489	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
491	463	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
492	45	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
493	475	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
494		eqcom 2629	. . . . . . . . . . . . . . . . . . . . . 22
495	454	ex 450	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$
496	494, 495	syl5bir 233	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$
497	496	con3dimp 457	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
498	497	neqned 2801	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
499	491, 492, 493, 498	leneltd 10191	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
500	499	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
501	480, 481, 484, 490, 500	eliood 39720	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
502	479, 501	ffvelrnd 6360	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$
503	431, 459, 477, 502	fvmptd 6288	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
504		fvres 6207	. . . . . . . . . . . . . . 15
505	501, 504	syl 17	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
506	503, 505	eqtrd 2656	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
507	465	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
508	466	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
509	120	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
510	303	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
511	468	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
512		neqne 2802	. . . . . . . . . . . . . . . . . . 19
513	512	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
514	509, 510, 511, 513	leneltd 10191	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$
515	514	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
516	300	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
517	472	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
518		neqne 2802	. . . . . . . . . . . . . . . . . . 19
519	518	necomd 2849	. . . . . . . . . . . . . . . . . 18
520	519	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
521	482, 516, 517, 520	leneltd 10191	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
522	507, 508, 482, 515, 521	eliood 39720	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$
523		fvres 6207	. . . . . . . . . . . . . . 15
524	522, 523	syl 17	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
525	440	fveq2d 6195	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
526	525	eqcomd 2628	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
527	526	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
528	438, 439	subcld 10392	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
529		elex 3212	. . . . . . . . . . . . . . . . 17
530	528, 529	syl 17	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$
531	530	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$
532		simp-4l 806	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
533	153	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
534	155	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
535	157	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^
536		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ ..^
537	533, 534, 535, 536	fourierdlem8 40332	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^
538	537	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$
539	538, 476	sseldd 3604	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
540	539	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
541	532, 540	jca 554	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
542		eleq1 2689	. . . . . . . . . . . . . . . . . 18
543	542	anbi2d 740	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
544		oveq1 6657	. . . . . . . . . . . . . . . . . . 19
545	544	fveq2d 6195	. . . . . . . . . . . . . . . . . 18
546		fveq2 6191	. . . . . . . . . . . . . . . . . 18
547	545, 546	eqeq12d 2637	. . . . . . . . . . . . . . . . 17
548	543, 547	imbi12d 334	. . . . . . . . . . . . . . . 16 $/\$ $/\$
549		eleq1 2689	. . . . . . . . . . . . . . . . . . 19
550	549	anbi2d 740	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
551		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20
552	551	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
553		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
554	552, 553	eqeq12d 2637	. . . . . . . . . . . . . . . . . 18
555	550, 554	imbi12d 334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
556	555, 164	chvarv 2263	. . . . . . . . . . . . . . . 16 $/\$
557	548, 556	vtoclg 3266	. . . . . . . . . . . . . . 15 $/\$
558	531, 541, 557	sylc 65	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
559	524, 527, 558	3eqtrd 2660	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
560	506, 559	eqtr4d 2659	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$ $/\$
561	429, 560	eqtr4d 2659	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$ $/\$
562	427, 561	pm2.61dan 832	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
563	394, 562	eqtrd 2656	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$
564	392, 563	pm2.61dan 832	. . . . . . . 8 $/\$ ..^ $/\$
565	308, 389	eqeltrd 2701	. . . . . . . . . . 11 $/\$ ..^ $/\$
566	565	adantlr 751	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
567	425, 419	eqeltrd 2701	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
568	567	ad4ant14 1293	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$ $/\$
569	263, 265	fssresd 6071	. . . . . . . . . . . . . . 15 $/\$ ..^
570	569	ad3antrrr 766	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
571	570, 522	ffvelrnd 6360	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$ $/\$
572	429, 571	eqeltrd 2701	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$ $/\$
573	568, 572	pm2.61dan 832	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
574	394, 573	eqeltrd 2701	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
575	566, 574	pm2.61dan 832	. . . . . . . . 9 $/\$ ..^ $/\$
576		eqid 2622	. . . . . . . . . 10
577	576	fvmpt2 6291	. . . . . . . . 9 $/\$
578	301, 575, 577	syl2anc 693	. . . . . . . 8 $/\$ ..^ $/\$
579		nfv 1843	. . . . . . . . . . . . . 14 $/\$ ..^
580		eqid 2622	. . . . . . . . . . . . . 14
581	579, 580, 42, 45, 53, 54, 55	cncfiooicc 40107	. . . . . . . . . . . . 13 $/\$ ..^
582	364, 581	eqeltrd 2701	. . . . . . . . . . . 12 $/\$ ..^
583		cncff 22696	. . . . . . . . . . . 12
584	582, 583	syl 17	. . . . . . . . . . 11 $/\$ ..^
585	584	adantr 481	. . . . . . . . . 10 $/\$ ..^ $/\$
586	585, 476	ffvelrnd 6360	. . . . . . . . 9 $/\$ ..^ $/\$
587		fourierdlem81.h	. . . . . . . . . 10
588	587	fvmpt2 6291	. . . . . . . . 9 $/\$
589	301, 586, 588	syl2anc 693	. . . . . . . 8 $/\$ ..^ $/\$
590	564, 578, 589	3eqtr4rd 2667	. . . . . . 7 $/\$ ..^ $/\$
591	590	itgeq2dv 23548	. . . . . 6 $/\$ ..^
592		ioossicc 12259	. . . . . . . . . . . 12
593	592	sseli 3599	. . . . . . . . . . 11
594	593	adantl 482	. . . . . . . . . 10 $/\$ ..^ $/\$
595	593, 575	sylan2 491	. . . . . . . . . 10 $/\$ ..^ $/\$
596	594, 595, 577	syl2anc 693	. . . . . . . . 9 $/\$ ..^ $/\$
597	229, 237	gtned 10172	. . . . . . . . . . 11 $/\$ ..^ $/\$
598	597	neneqd 2799	. . . . . . . . . 10 $/\$ ..^ $/\$
599	598	iffalsed 4097	. . . . . . . . 9 $/\$ ..^ $/\$
600	230, 241	ltned 10173	. . . . . . . . . . . 12 $/\$ ..^ $/\$
601	600	neneqd 2799	. . . . . . . . . . 11 $/\$ ..^ $/\$
602	601	iffalsed 4097	. . . . . . . . . 10 $/\$ ..^ $/\$
603	523	adantl 482	. . . . . . . . . 10 $/\$ ..^ $/\$
604	602, 603	eqtrd 2656	. . . . . . . . 9 $/\$ ..^ $/\$
605	596, 599, 604	3eqtrd 2660	. . . . . . . 8 $/\$ ..^ $/\$
606	605	itgeq2dv 23548	. . . . . . 7 $/\$ ..^
607	578, 575	eqeltrd 2701	. . . . . . . 8 $/\$ ..^ $/\$
608	120, 121, 607	itgioo 23582	. . . . . . 7 $/\$ ..^
609	120, 121, 304	itgioo 23582	. . . . . . 7 $/\$ ..^
610	606, 608, 609	3eqtr3d 2664	. . . . . 6 $/\$ ..^
611	591, 610	eqtr2d 2657	. . . . 5 $/\$ ..^
612	99, 109	oveq12d 6668	. . . . . . 7 $/\$ ..^
613	612	itgeq1d 40172	. . . . . 6 $/\$ ..^
614		simpr 477	. . . . . . . . . 10 $/\$ ..^ $/\$
615	612	eqcomd 2628	. . . . . . . . . . 11 $/\$ ..^
616	615	adantr 481	. . . . . . . . . 10 $/\$ ..^ $/\$
617	614, 616	eleqtrd 2703	. . . . . . . . 9 $/\$ ..^ $/\$
618	584	adantr 481	. . . . . . . . . 10 $/\$ ..^ $/\$
619	42	adantr 481	. . . . . . . . . . 11 $/\$ ..^ $/\$
620	45	adantr 481	. . . . . . . . . . 11 $/\$ ..^ $/\$
621	97	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
622	108	adantr 481	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
623		eliccre 39728	. . . . . . . . . . . . 13 $/\$ $/\$
624	621, 622, 614, 623	syl3anc 1326	. . . . . . . . . . . 12 $/\$ ..^ $/\$
625	75	ad2antrr 762	. . . . . . . . . . . 12 $/\$ ..^ $/\$
626	624, 625	resubcld 10458	. . . . . . . . . . 11 $/\$ ..^ $/\$
627	226	eqcomd 2628	. . . . . . . . . . . . 13 $/\$ ..^
628	627	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$
629	621	rexrd 10089	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
630	622	rexrd 10089	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
631		iccgelb 12230	. . . . . . . . . . . . . 14 $/\$ $/\$
632	629, 630, 614, 631	syl3anc 1326	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
633	621, 624, 625, 632	lesub1dd 10643	. . . . . . . . . . . 12 $/\$ ..^ $/\$
634	628, 633	eqbrtrd 4675	. . . . . . . . . . 11 $/\$ ..^ $/\$
635		iccleub 12229	. . . . . . . . . . . . . 14 $/\$ $/\$
636	629, 630, 614, 635	syl3anc 1326	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
637	624, 622, 625, 636	lesub1dd 10643	. . . . . . . . . . . 12 $/\$ ..^ $/\$
638	245	adantr 481	. . . . . . . . . . . 12 $/\$ ..^ $/\$
639	637, 638	breqtrd 4679	. . . . . . . . . . 11 $/\$ ..^ $/\$
640	619, 620, 626, 634, 639	eliccd 39726	. . . . . . . . . 10 $/\$ ..^ $/\$
641	618, 640	ffvelrnd 6360	. . . . . . . . 9 $/\$ ..^ $/\$
642	617, 641, 588	syl2anc 693	. . . . . . . 8 $/\$ ..^ $/\$
643		eqidd 2623	. . . . . . . . 9 $/\$ ..^ $/\$
644		oveq1 6657	. . . . . . . . . . 11
645	644	fveq2d 6195	. . . . . . . . . 10
646	645	adantl 482	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$
647	643, 646, 614, 641	fvmptd 6288	. . . . . . . 8 $/\$ ..^ $/\$
648	642, 647	eqtr4d 2659	. . . . . . 7 $/\$ ..^ $/\$
649	648	itgeq2dv 23548	. . . . . 6 $/\$ ..^
650	74	adantr 481	. . . . . . 7 $/\$ ..^
651	645	cbvmptv 4750	. . . . . . 7
652	42, 45, 381, 582, 650, 651	itgiccshift 40196	. . . . . 6 $/\$ ..^
653	613, 649, 652	3eqtrd 2660	. . . . 5 $/\$ ..^
654	132	adantr 481	. . . . . . . 8 $/\$ ..^
655	59, 654	sseqtr4d 3642	. . . . . . 7 $/\$ ..^
656	42, 45, 135, 53, 655, 55, 54, 309	itgioocnicc 40193	. . . . . 6 $/\$ ..^ $/\$
657	656	simprd 479	. . . . 5 $/\$ ..^
658	611, 653, 657	3eqtrd 2660	. . . 4 $/\$ ..^
659	658	sumeq2dv 14433	. . 3 ..^ ..^
660	90, 306, 659	3eqtrrd 2661	. 2 ..^
661	14, 63, 660	3eqtrrd 2661	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200

wss 3574

cif 4086 class class class wbr 4653

cmpt 4729

cdm 5114

cres 5116

wf 5884

cfv 5888 (class class class)co 6650

cmap 7857

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cxr 10073

clt 10074

cle 10075

cmin 10266

cn 11020

cn0 11292

cuz 11687

crp 11832

cioo 12175

cicc 12178

cfz 12326 ..^cfzo 12465

csu 14416

ccncf 22679

cibl 23386

citg 23387 lim

climc 23626

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cc 9257 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-ofr 6898 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-omul 7565 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-acn 8768 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 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-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389 df-itg2 23390 df-ibl 23391 df-itg 23392 df-0p 23437 df-ditg 23611 df-limc 23630 df-dv 23631

This theorem is referenced by: fourierdlem92 40415

W3C validator