fourierdlem62 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem62 31792

Description: The function

is continuous (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypothesis**
Ref	Expression
fourierdlem62.k

**Assertion**
Ref	Expression
fourierdlem62

Proof of Theorem fourierdlem62 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem62.k	. . . 4
2		eqeq1 2471	. . . . . 6
3		eqidd 2468	. . . . . 6
4		id 22	. . . . . . 7
5		oveq1 6302	. . . . . . . . 9
6	5	fveq2d 5876	. . . . . . . 8
7	6	oveq2d 6311	. . . . . . 7
8	4, 7	oveq12d 6313	. . . . . 6
9	2, 3, 8	ifeq123d 31337	. . . . 5
10	9	cbvmptv 4544	. . . 4
11	1, 10	eqtri 2496	. . 3
12	11	fourierdlem43 31773	. 2
13		ax-resscn 9561	. . 3
14		fss 5745	. . . . . 6 $/\$
15	12, 13, 14	mp2an 672	. . . . 5
16	15	a1i 11	. . . . . . . . . 10
17		difss 3636	. . . . . . . . . . . . . . . . . 18 $\$
18		elioore 11571	. . . . . . . . . . . . . . . . . . 19
19	18	ssriv 3513	. . . . . . . . . . . . . . . . . 18
20	17, 19	sstri 3518	. . . . . . . . . . . . . . . . 17 $\$
21	20	a1i 11	. . . . . . . . . . . . . . . 16 $\$
22		eqid 2467	. . . . . . . . . . . . . . . . . 18 $\$ $\$
23	20	sseli 3505	. . . . . . . . . . . . . . . . . 18 $\$
24	22, 23	fmpti 6055	. . . . . . . . . . . . . . . . 17 $\$ $\$
25	24	a1i 11	. . . . . . . . . . . . . . . 16 $\$ $\$
26		eqid 2467	. . . . . . . . . . . . . . . . . 18 $\$ $\$
27		2re 10617	. . . . . . . . . . . . . . . . . . . . 21
28	27	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $\$
29		rehalfcl 10777	. . . . . . . . . . . . . . . . . . . . . 22
30	23, 29	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $\$
31		resincl 13753	. . . . . . . . . . . . . . . . . . . . 21
32	30, 31	syl 16	. . . . . . . . . . . . . . . . . . . 20 $\$
33	28, 32	jca 532	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
34		remulcl 9589	. . . . . . . . . . . . . . . . . . 19 $/\$
35	33, 34	syl 16	. . . . . . . . . . . . . . . . . 18 $\$
36	26, 35	fmpti 6055	. . . . . . . . . . . . . . . . 17 $\$ $\$
37	36	a1i 11	. . . . . . . . . . . . . . . 16 $\$ $\$
38		iooretop 21141	. . . . . . . . . . . . . . . . 17
39	38	a1i 11	. . . . . . . . . . . . . . . 16
40		0re 9608	. . . . . . . . . . . . . . . . . . 19
41		negpilt0 31362	. . . . . . . . . . . . . . . . . . 19
42		pipos 22720	. . . . . . . . . . . . . . . . . . 19
43	40, 41, 42	3pm3.2i 1174	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
44		pire 22718	. . . . . . . . . . . . . . . . . . . . 21
45	44	renegcli 9892	. . . . . . . . . . . . . . . . . . . 20
46	45	rexri 9658	. . . . . . . . . . . . . . . . . . 19
47	44	rexri 9658	. . . . . . . . . . . . . . . . . . 19
48		elioo2 11582	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
49	46, 47, 48	mp2an 672	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
50	43, 49	mpbir 209	. . . . . . . . . . . . . . . . 17
51	50	a1i 11	. . . . . . . . . . . . . . . 16
52		eqid 2467	. . . . . . . . . . . . . . . 16 $\$ $\$
53		1ex 9603	. . . . . . . . . . . . . . . . . . . . 21
54		eqid 2467	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
55	53, 54	dmmpti 5716	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
56	55	eqcomi 2480	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
57		reex 9595	. . . . . . . . . . . . . . . . . . . . . . . . 25
58	57	prid1 4141	. . . . . . . . . . . . . . . . . . . . . . . 24
59	58	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
60	13	sseli 3505	. . . . . . . . . . . . . . . . . . . . . . . 24
61	60	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
62		1re 9607	. . . . . . . . . . . . . . . . . . . . . . . 24
63	62	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
64	59	dvmptid 22228	. . . . . . . . . . . . . . . . . . . . . . 23
65		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . 24 ℂ_fld ℂ_fld
66	65	tgioo2 21176	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
67		sncldre 31338	. . . . . . . . . . . . . . . . . . . . . . . . . 26
68	40, 67	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25
69		retopon 21138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 TopOn
70	69	toponunii 19302	. . . . . . . . . . . . . . . . . . . . . . . . . 26
71	70	difopn 19403	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$
72	38, 68, 71	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
73	72	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
74	59, 61, 63, 64, 21, 66, 65, 73	dvmptres 22234	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
75	74	trud 1388	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
76	75	eqcomi 2480	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
77	76	dmeqi 5210	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
78	56, 77	eqtri 2496	. . . . . . . . . . . . . . . . . 18 $\$ $\$
79	78	eqimssi 3563	. . . . . . . . . . . . . . . . 17 $\$ $\$
80	79	a1i 11	. . . . . . . . . . . . . . . 16 $\$ $\$
81		fvex 5882	. . . . . . . . . . . . . . . . . . . . 21
82		eqid 2467	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
83	81, 82	dmmpti 5716	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
84	83	eqcomi 2480	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
85		2cn 10618	. . . . . . . . . . . . . . . . . . . . . . . . . 26
86	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
87		halfcl 10776	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	61, 87	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
89		sincl 13739	. . . . . . . . . . . . . . . . . . . . . . . . . 26
90	88, 89	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
91	86, 90	jca 532	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
92		mulcl 9588	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
93	91, 92	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
94		coscl 13740	. . . . . . . . . . . . . . . . . . . . . . . 24
95	88, 94	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
96	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
97		2ne0 10640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
99	60, 96, 98	divrec2d 10336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
100	99	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
101	100	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
102	101	mpteq2ia 4535	. . . . . . . . . . . . . . . . . . . . . . . . . 26
103	102	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . . . . 25
104		resmpt 5329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
105	13, 104	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
106	105	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
107	106	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . . . . . 26
108		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
109	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
110	85, 97	reccli 10286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
111	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
112		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
113	111, 112	mulcld 9628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
114	113	sincld 13743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
115	109, 114	mulcld 9628	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
116	108, 115	fmpti 6055	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
117		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
118	85, 110	mulcli 9613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
120		coscl 13740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
121	113, 120	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	119, 121	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
123		mulcl 9588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
124	122, 123	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	124	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
126	117, 125	dmmptd 5717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
127	126	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
128	13, 127	sseqtr4i 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
129		dvasinbx 31573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
130	85, 110, 129	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
131	130	dmeqi 5210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
132	128, 131	sseqtr4i 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
133		dvcnre 31567	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
134	116, 132, 133	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . 26
135	130	reseq1i 5275	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
136		resmpt 5329	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
137	13, 136	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
138	85, 97	recidi 10287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
139	138	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
140	99	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
141	140	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
142	139, 141	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
143	60, 87	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
144	143, 94	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
145	144	mulid2d 9626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
146	142, 145	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
147	146	mpteq2ia 4535	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
148	135, 137, 147	3eqtri 2500	. . . . . . . . . . . . . . . . . . . . . . . . . 26
149	107, 134, 148	3eqtri 2500	. . . . . . . . . . . . . . . . . . . . . . . . 25
150	103, 149	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . 24
151	150	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
152	59, 93, 95, 151, 21, 66, 65, 73	dvmptres 22234	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
153	152	trud 1388	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
154	153	eqcomi 2480	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
155	154	dmeqi 5210	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
156	84, 155	eqtri 2496	. . . . . . . . . . . . . . . . . 18 $\$ $\$
157	156	eqimssi 3563	. . . . . . . . . . . . . . . . 17 $\$ $\$
158	157	a1i 11	. . . . . . . . . . . . . . . 16 $\$ $\$
159		id 22	. . . . . . . . . . . . . . . . . . . . . 22
160		eqid 2467	. . . . . . . . . . . . . . . . . . . . . 22
161	40	elexi 3128	. . . . . . . . . . . . . . . . . . . . . 22
162	159, 160, 161	fvmpt 5957	. . . . . . . . . . . . . . . . . . . . 21
163	50, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
164	163	eqcomi 2480	. . . . . . . . . . . . . . . . . . 19
165		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . 24
166	112	ssriv 3513	. . . . . . . . . . . . . . . . . . . . . . . . . 26
167		cncfmptid 21284	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
168	166, 166, 167	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . 25
169	168	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
170	13, 18	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . 26
171	170	ssriv 3513	. . . . . . . . . . . . . . . . . . . . . . . . 25
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
173	166	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
174	19	sseli 3505	. . . . . . . . . . . . . . . . . . . . . . . . . 26
175	174, 60	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25
176	175	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
177	165, 169, 172, 173, 176	cncfmptssg 31531	. . . . . . . . . . . . . . . . . . . . . . 23
178	177	trud 1388	. . . . . . . . . . . . . . . . . . . . . 22
179		cnlimc 22160	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ lim
180	171, 179	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ lim
181	178, 180	mpbi 208	. . . . . . . . . . . . . . . . . . . . 21 $/\$ lim
182	181	simpri 462	. . . . . . . . . . . . . . . . . . . 20 lim
183		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . 22
184		oveq2 6303	. . . . . . . . . . . . . . . . . . . . . 22 lim lim
185	183, 184	eleq12d 2549	. . . . . . . . . . . . . . . . . . . . 21 lim lim
186	185	rspccva 3218	. . . . . . . . . . . . . . . . . . . 20 lim $/\$ lim
187	182, 50, 186	mp2an 672	. . . . . . . . . . . . . . . . . . 19 lim
188	164, 187	eqeltri 2551	. . . . . . . . . . . . . . . . . 18 lim
189	160, 175	fmpti 6055	. . . . . . . . . . . . . . . . . . . . . 22
190	189	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
191	190	limcdif 22148	. . . . . . . . . . . . . . . . . . . 20 lim $\$ lim
192	191	trud 1388	. . . . . . . . . . . . . . . . . . 19 lim $\$ lim
193		resmpt 5329	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
194	17, 193	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
195	194	oveq1i 6305	. . . . . . . . . . . . . . . . . . 19 $\$ lim $\$ lim
196	192, 195	eqtri 2496	. . . . . . . . . . . . . . . . . 18 lim $\$ lim
197	188, 196	eleqtri 2553	. . . . . . . . . . . . . . . . 17 $\$ lim
198	197	a1i 11	. . . . . . . . . . . . . . . 16 $\$ lim
199		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
200	85, 97	div0i 10290	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
202	199, 201	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . 26
203	202	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . 25
204		sin0 13762	. . . . . . . . . . . . . . . . . . . . . . . . . 26
205	204	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
206	203, 205	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . 24
207	206	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . 23
208	85	mul01i 9781	. . . . . . . . . . . . . . . . . . . . . . . 24
209	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
210	207, 209	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . 22
211		eqid 2467	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211, 161	fvmpt 5957	. . . . . . . . . . . . . . . . . . . . 21
213	50, 212	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
214	213	eqcomi 2480	. . . . . . . . . . . . . . . . . . 19
215		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
216	166	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
217	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
218	216, 217, 216	constcncfg 31532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
219	85, 218	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
220	219	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
221	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
222	215, 220, 172, 173, 221	cncfmptssg 31531	. . . . . . . . . . . . . . . . . . . . . . . . . 26
223	222	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . 25
224	223	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
225		sincn 22706	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
226	225	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
227		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
228	227	divccncf 21278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
229	85, 97, 228	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
230	229	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
231	176, 87	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
232	227, 230, 172, 173, 231	cncfmptssg 31531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
233	232	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
234	233	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
235	226, 234	cncfmpt1f 21285	. . . . . . . . . . . . . . . . . . . . . . . . . 26
236	235	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . 25
237	236	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
238	224, 237	mulcncf 21727	. . . . . . . . . . . . . . . . . . . . . . 23
239	238	trud 1388	. . . . . . . . . . . . . . . . . . . . . 22
240		cnlimc 22160	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ lim
241	171, 240	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ lim
242	239, 241	mpbi 208	. . . . . . . . . . . . . . . . . . . . 21 $/\$ lim
243	242	simpri 462	. . . . . . . . . . . . . . . . . . . 20 lim
244		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . 22
245		oveq2 6303	. . . . . . . . . . . . . . . . . . . . . 22 lim lim
246	244, 245	eleq12d 2549	. . . . . . . . . . . . . . . . . . . . 21 lim lim
247	246	rspccva 3218	. . . . . . . . . . . . . . . . . . . 20 lim $/\$ lim
248	243, 50, 247	mp2an 672	. . . . . . . . . . . . . . . . . . 19 lim
249	214, 248	eqeltri 2551	. . . . . . . . . . . . . . . . . 18 lim
250	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
251	175, 87	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26
252	251, 89	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25
253	250, 252	jca 532	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
254	253, 92	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23
255	211, 254	fmpti 6055	. . . . . . . . . . . . . . . . . . . . . 22
256	255	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
257	256	limcdif 22148	. . . . . . . . . . . . . . . . . . . 20 lim $\$ lim
258	257	trud 1388	. . . . . . . . . . . . . . . . . . 19 lim $\$ lim
259		resmpt 5329	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
260	17, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
261	260	oveq1i 6305	. . . . . . . . . . . . . . . . . . 19 $\$ lim $\$ lim
262	258, 261	eqtri 2496	. . . . . . . . . . . . . . . . . 18 lim $\$ lim
263	249, 262	eleqtri 2553	. . . . . . . . . . . . . . . . 17 $\$ lim
264	263	a1i 11	. . . . . . . . . . . . . . . 16 $\$ lim
265		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
266		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . 26
267	266	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . 25
268	267	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . 24
269	268	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
270		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
271	27	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
272	20	sseli 3505	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
273	272	rehalfcld 10797	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
274		resincl 13753	. . . . . . . . . . . . . . . . . . . . . . . . . 26
275	273, 274	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
276	271, 275	jca 532	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
277		remulcl 9589	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
278	276, 277	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
279	265, 269, 270, 278	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
280	85	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
281	13, 275	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
282	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
283		ioossicc 11622	. . . . . . . . . . . . . . . . . . . . . . . . 25
284	270	eldifad 3493	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
285	283, 284	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
286		eldifsni 4159	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
287		fourierdlem44 31774	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
288	285, 286, 287	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
289	280, 281, 282, 288	mulne0d 10213	. . . . . . . . . . . . . . . . . . . . . 22 $\$
290	279, 289	eqnetrd 2760	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
291	290	neneqd 2669	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
292	291	rgen 2827	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
293		ralnex 2913	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$
294	292, 293	mpbi 208	. . . . . . . . . . . . . . . . . 18 $\$ $\$
295	35	rgen 2827	. . . . . . . . . . . . . . . . . . . 20 $\$
296	26	fnmpt 5713	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
297	295, 296	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
298		ssid 3528	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
299		fvelimab 5930	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
300	297, 298, 299	mp2an 672	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $\$
301	294, 300	mtbir 299	. . . . . . . . . . . . . . . . 17 $\$ $\$
302	301	a1i 11	. . . . . . . . . . . . . . . 16 $\$ $\$
303		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
304	266	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . 25
305	304	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
306	13	sseli 3505	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
307	272, 306	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
308	307, 280, 282	divcld 10332	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
309	308	coscld 13744	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
310	303, 305, 270, 309	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
311	273	rered 13037	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
312		halfpire 22723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
313	312	renegcli 9892	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314	313	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
315	314	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
316	312	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
317	316	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
318	13, 44	sselii 3506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
319		divneg 10251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
320	318, 85, 97, 319	mp3an 1324	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
321	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
322	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
323	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
324		ioogtlb 31415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
325	322, 323, 284, 324	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
326	45	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
327		2rp 11237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
328	327	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
329	326, 272, 328	ltdiv1d 11309	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
330	325, 329	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
331	321, 330	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
332		iooltub 31435	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
333	322, 323, 284, 332	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
334	44	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
335	272, 334, 328	ltdiv1d 11309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
336	333, 335	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
337	315, 317, 273, 331, 336	eliood 31418	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
338	311, 337	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
339		cosne0 22783	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
340	308, 338, 339	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
341	310, 340	eqnetrd 2760	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
342	341	neneqd 2669	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
343	342	rgen 2827	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
344		ralnex 2913	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$
345	343, 344	mpbi 208	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
346	81, 82	fnmpti 5715	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
347		fvelimab 5930	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $/\$ $\$ $\$ $\$ $\$ $\$ $\$
348	346, 298, 347	mp2an 672	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$
349	345, 348	mtbir 299	. . . . . . . . . . . . . . . . . 18 $\$ $\$
350	153	imaeq1i 5340	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$ $\$
351	350	eleq2i 2545	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$
352	351	notbii 296	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$ $\$
353	349, 352	mpbir 209	. . . . . . . . . . . . . . . . 17 $\$ $\$
354	353	a1i 11	. . . . . . . . . . . . . . . 16 $\$ $\$
355		ax-1cn 9562	. . . . . . . . . . . . . . . . . . . . 21
356	355	div1i 10284	. . . . . . . . . . . . . . . . . . . 20
357	356	eqcomi 2480	. . . . . . . . . . . . . . . . . . 19
358		eqid 2467	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
359		eqid 2467	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
360	20	sseli 3505	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
361	13, 360	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
362	361	halfcld 10795	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
363	362	coscld 13744	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
364	27	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
365	97	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
366	360, 364, 365	redivcld 10384	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
367	366	rered 13037	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
368	313	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
369	368	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
370	312	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
371	370	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
372	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
373	44	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
374	373	renegcld 9998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
375	327	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
376	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
377	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
378		eldif 3491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $/\$
379	378	simplbi 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
380		ioogtlb 31415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
381	376, 377, 379, 380	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
382	374, 360, 375, 381	ltdiv1dd 11321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
383	372, 382	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
384		iooltub 31435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
385	376, 377, 379, 384	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
386	360, 373, 375, 385	ltdiv1dd 11321	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
387	369, 371, 366, 383, 386	eliood 31418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
388	367, 387	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
389		cosne0 22783	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
390	362, 388, 389	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
391	390	neneqd 2669	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
392	366	recoscld 13757	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
393		elsncg 4056	. . . . . . . . . . . . . . . . . . . . . . . . 25
394	392, 393	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
395	391, 394	mtbird 301	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
396	363, 395	eldifd 3492	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
397	396	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$
398	362	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$
399		cosf 13738	. . . . . . . . . . . . . . . . . . . . . . . 24
400	399	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
401	400	ffvelrnda 6032	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
402		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
403	402	divccncf 21278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
404	85, 97, 403	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
405	404	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
406	170	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
407	406	halfcld 10795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
408	402, 405, 172, 173, 407	cncfmptssg 31531	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
409	408	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
410	409	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
411		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
412	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
413	411, 412	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . 26
414	410, 51, 413	cnmptlimc 22162	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim
415	414	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . 24 lim
416		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
417		halfcl 10776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
418	170, 417	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
419	416, 418	fmpti 6055	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
420	419	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
421	420	limcdif 22148	. . . . . . . . . . . . . . . . . . . . . . . . . 26 lim $\$ lim
422	421	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim $\$ lim
423		resmpt 5329	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $\$ $\$
424	17, 423	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
425	424	oveq1i 6305	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ lim $\$ lim
426	422, 425	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . 24 lim $\$ lim
427	415, 426	eleqtri 2553	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ lim
428	427	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $\$ lim
429		ffn 5737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
430	399, 429	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
431		dffn5 5919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
432	430, 431	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
433	432	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
434		coscn 22707	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
435	433, 434	eqeltri 2551	. . . . . . . . . . . . . . . . . . . . . . . . . 26
436	435	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
437	171, 51	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . 25
438		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . 26
439		cos0 13763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
440	439	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
441	438, 440	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . 25
442	436, 437, 441	cnmptlimc 22162	. . . . . . . . . . . . . . . . . . . . . . . 24 lim
443	442	trud 1388	. . . . . . . . . . . . . . . . . . . . . . 23 lim
444	443	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 lim
445		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . 22
446		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . 24
447	439	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
448	446, 447	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . 23
449	448	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$
450	398, 401, 428, 444, 445, 449	limcco 22165	. . . . . . . . . . . . . . . . . . . . 21 $\$ lim
451		ax-1ne0 9573	. . . . . . . . . . . . . . . . . . . . . 22
452	451	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
453	358, 359, 397, 450, 452	reclimc 31518	. . . . . . . . . . . . . . . . . . . 20 $\$ lim
454	453	trud 1388	. . . . . . . . . . . . . . . . . . 19 $\$