fouriersw - Mathbox for Glauco Siliprandi

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

Theorem fouriersw 37978

Description: Fourier series convergence, for the square wave function. Where

is discontinuous, the series converges to

, the average value of the left and the right limits. Notice that

is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fouriersw.t
fouriersw.f
fouriersw.x
fouriersw.z
fouriersw.y

**Assertion**
Ref	Expression
fouriersw	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

Proof of Theorem fouriersw Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 11140	. . . . . . 7
2		1zzd 10914	. . . . . . 7
3		eqidd 2424	. . . . . . . . 9
4		oveq2 6252	. . . . . . . . . . . . . 14
5	4	oveq1d 6259	. . . . . . . . . . . . 13
6	5	oveq1d 6259	. . . . . . . . . . . 12
7	6	fveq2d 5824	. . . . . . . . . . 11
8	7, 5	oveq12d 6262	. . . . . . . . . 10
9	8	adantl 467	. . . . . . . . 9 $/\$
10		id 22	. . . . . . . . 9
11		ovex 6272	. . . . . . . . . 10
12	11	a1i 11	. . . . . . . . 9
13	3, 9, 10, 12	fvmptd 5909	. . . . . . . 8
14	13	adantl 467	. . . . . . 7 $/\$
15		2z 10915	. . . . . . . . . . . . . . 15
16	15	a1i 11	. . . . . . . . . . . . . 14
17		nnz 10905	. . . . . . . . . . . . . 14
18	16, 17	zmulcld 10992	. . . . . . . . . . . . 13
19		1zzd 10914	. . . . . . . . . . . . 13
20	18, 19	zsubcld 10991	. . . . . . . . . . . 12
21	20	zcnd 10987	. . . . . . . . . . 11
22		fouriersw.x	. . . . . . . . . . . . 13
23	22	recni 9601	. . . . . . . . . . . 12
24	23	a1i 11	. . . . . . . . . . 11
25	21, 24	mulcld 9609	. . . . . . . . . 10
26	25	sincld 14122	. . . . . . . . 9
27		0red 9590	. . . . . . . . . 10
28		2re 10625	. . . . . . . . . . . . . 14
29	28	a1i 11	. . . . . . . . . . . . 13
30		1red 9604	. . . . . . . . . . . . 13
31	29, 30	remulcld 9617	. . . . . . . . . . . 12
32	31, 30	resubcld 9993	. . . . . . . . . . 11
33	20	zred 10986	. . . . . . . . . . 11
34		0lt1 10082	. . . . . . . . . . . . 13
35		2t1e2 10704	. . . . . . . . . . . . . . 15
36	35	oveq1i 6254	. . . . . . . . . . . . . 14
37		2m1e1 10670	. . . . . . . . . . . . . 14
38	36, 37	eqtr2i 2446	. . . . . . . . . . . . 13
39	34, 38	breqtri 4385	. . . . . . . . . . . 12
40	39	a1i 11	. . . . . . . . . . 11
41	18	zred 10986	. . . . . . . . . . . 12
42		nnre 10562	. . . . . . . . . . . . 13
43		0le2 10646	. . . . . . . . . . . . . 14
44	43	a1i 11	. . . . . . . . . . . . 13
45		nnge1 10581	. . . . . . . . . . . . 13
46	30, 42, 29, 44, 45	lemul2ad 10493	. . . . . . . . . . . 12
47	31, 41, 30, 46	lesub1dd 10175	. . . . . . . . . . 11
48	27, 32, 33, 40, 47	ltletrd 9741	. . . . . . . . . 10
49	27, 48	gtned 9716	. . . . . . . . 9
50	26, 21, 49	divcld 10329	. . . . . . . 8
51	50	adantl 467	. . . . . . 7 $/\$
52		picn 23351	. . . . . . . . . . 11
53	52	a1i 11	. . . . . . . . . 10
54		4cn 10633	. . . . . . . . . . 11
55	54	a1i 11	. . . . . . . . . 10
56		4ne0 10652	. . . . . . . . . . 11
57	56	a1i 11	. . . . . . . . . 10
58	53, 55, 57	divcld 10329	. . . . . . . . 9
59		eqid 2423	. . . . . . . . . . . . . . . 16
60		0cnd 9582	. . . . . . . . . . . . . . . . 17
61	54	a1i 11	. . . . . . . . . . . . . . . . . . 19
62		nncn 10563	. . . . . . . . . . . . . . . . . . . 20
63		mulcl 9569	. . . . . . . . . . . . . . . . . . . 20 $/\$
64	62, 52, 63	sylancl 666	. . . . . . . . . . . . . . . . . . 19
65	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20
66		nnne0 10588	. . . . . . . . . . . . . . . . . . . 20
67		0re 9589	. . . . . . . . . . . . . . . . . . . . . 22
68		pipos 23352	. . . . . . . . . . . . . . . . . . . . . 22
69	67, 68	gtneii 9692	. . . . . . . . . . . . . . . . . . . . 21
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . 20
71	62, 65, 66, 70	mulne0d 10210	. . . . . . . . . . . . . . . . . . 19
72	61, 64, 71	divcld 10329	. . . . . . . . . . . . . . . . . 18
73	23	a1i 11	. . . . . . . . . . . . . . . . . . . 20
74	62, 73	mulcld 9609	. . . . . . . . . . . . . . . . . . 19
75	74	sincld 14122	. . . . . . . . . . . . . . . . . 18
76	72, 75	mulcld 9609	. . . . . . . . . . . . . . . . 17
77	60, 76	ifcld 3892	. . . . . . . . . . . . . . . 16
78	59, 77	fmpti 5999	. . . . . . . . . . . . . . 15
79	78	a1i 11	. . . . . . . . . . . . . 14
80		eqidd 2424	. . . . . . . . . . . . . . . . . 18
81		breq2 4365	. . . . . . . . . . . . . . . . . . . 20
82		oveq1 6251	. . . . . . . . . . . . . . . . . . . . . 22
83	82	oveq2d 6260	. . . . . . . . . . . . . . . . . . . . 21
84		oveq1 6251	. . . . . . . . . . . . . . . . . . . . . 22
85	84	fveq2d 5824	. . . . . . . . . . . . . . . . . . . . 21
86	83, 85	oveq12d 6262	. . . . . . . . . . . . . . . . . . . 20
87	81, 86	ifbieq2d 3874	. . . . . . . . . . . . . . . . . . 19
88	87	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$
89		c0ex 9583	. . . . . . . . . . . . . . . . . . . 20
90		ovex 6272	. . . . . . . . . . . . . . . . . . . 20
91	89, 90	ifex 3917	. . . . . . . . . . . . . . . . . . 19
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18
93	80, 88, 10, 92	fvmptd 5909	. . . . . . . . . . . . . . . . 17
94	93	adantr 466	. . . . . . . . . . . . . . . 16 $/\$
95		simpr 462	. . . . . . . . . . . . . . . . . 18 $/\$
96		simpl 458	. . . . . . . . . . . . . . . . . . 19 $/\$
97		2nn 10713	. . . . . . . . . . . . . . . . . . 19
98		nndivdvds 14249	. . . . . . . . . . . . . . . . . . 19 $/\$
99	96, 97, 98	sylancl 666	. . . . . . . . . . . . . . . . . 18 $/\$
100	95, 99	mpbird 235	. . . . . . . . . . . . . . . . 17 $/\$
101	100	iftrued 3857	. . . . . . . . . . . . . . . 16 $/\$
102	94, 101	eqtrd 2457	. . . . . . . . . . . . . . 15 $/\$
103	102	3adant1 1023	. . . . . . . . . . . . . 14 $/\$ $/\$
104		fouriersw.f	. . . . . . . . . . . . . . . . . 18
105		1re 9588	. . . . . . . . . . . . . . . . . . . 20
106	105	renegcli 9881	. . . . . . . . . . . . . . . . . . . 20
107	105, 106	keepel 3916	. . . . . . . . . . . . . . . . . . 19
108	107	a1i 11	. . . . . . . . . . . . . . . . . 18
109	104, 108	fmpti 5999	. . . . . . . . . . . . . . . . 17
110		fouriersw.t	. . . . . . . . . . . . . . . . 17
111		oveq1 6251	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	breq1d 4371	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	ifbid 3871	. . . . . . . . . . . . . . . . . . . . . 22
114	113	cbvmptv 4454	. . . . . . . . . . . . . . . . . . . . 21
115	104, 114	eqtri 2445	. . . . . . . . . . . . . . . . . . . 20
116	115	a1i 11	. . . . . . . . . . . . . . . . . . 19
117		oveq1 6251	. . . . . . . . . . . . . . . . . . . . . . . 24
118		pire 23350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	28, 118	remulcli 9603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	110, 119	eqeltri 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	120	recni 9601	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	121	mulid2i 9592	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
123	122	eqcomi 2432	. . . . . . . . . . . . . . . . . . . . . . . . . 26
124	123	oveq2i 6255	. . . . . . . . . . . . . . . . . . . . . . . . 25
125	124	oveq1i 6254	. . . . . . . . . . . . . . . . . . . . . . . 24
126	117, 125	syl6eq 2473	. . . . . . . . . . . . . . . . . . . . . . 23
127	126	adantl 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
128		simpl 458	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
129		2pos 10647	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
130	28, 118, 129, 68	mulgt0ii 9714	. . . . . . . . . . . . . . . . . . . . . . . . . 26
131	110	eqcomi 2432	. . . . . . . . . . . . . . . . . . . . . . . . . 26
132	130, 131	breqtri 4385	. . . . . . . . . . . . . . . . . . . . . . . . 25
133	120, 132	elrpii 11251	. . . . . . . . . . . . . . . . . . . . . . . 24
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
135		1zzd 10914	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136		modcyc 12077	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
137	128, 134, 135, 136	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
138	127, 137	eqtrd 2457	. . . . . . . . . . . . . . . . . . . . 21 $/\$
139	138	breq1d 4371	. . . . . . . . . . . . . . . . . . . 20 $/\$
140	139	ifbid 3871	. . . . . . . . . . . . . . . . . . 19 $/\$
141		id 22	. . . . . . . . . . . . . . . . . . . 20
142	120	a1i 11	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	readdcld 9616	. . . . . . . . . . . . . . . . . . 19
144	116, 140, 143, 108	fvmptd 5909	. . . . . . . . . . . . . . . . . 18
145	104	fvmpt2 5912	. . . . . . . . . . . . . . . . . . 19 $/\$
146	107, 145	mpan2 675	. . . . . . . . . . . . . . . . . 18
147	144, 146	eqtr4d 2460	. . . . . . . . . . . . . . . . 17
148		eqid 2423	. . . . . . . . . . . . . . . . 17
149		snfi 7599	. . . . . . . . . . . . . . . . . 18
150		eldifi 3525	. . . . . . . . . . . . . . . . . . . . . 22 $\$
151		0xr 9633	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
152	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
153	118	rexri 9639	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
154	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155		elioore 11612	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
156	155	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
157		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
158	118	renegcli 9881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159	158	rexri 9639	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
160		iooltub 37502	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
161	159, 153, 160	mp3an12 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
162	161	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
163	152, 154, 156, 157, 162	eliood 37487	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
164		negpilt0 37387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
165	158, 67, 164	ltleii 9703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
166		iooss1 11617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
167	159, 165, 166	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168	167	sseli 3398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
169	104	reseq1i 5058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
170		ioossre 11642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
171		resmpt 5111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
172	170, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
173		elioore 11612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
174	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
175		0red 9590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
176		ioogtlb 37484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
177	151, 153, 176	mp3an12 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
178	175, 173, 177	ltled 9729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
179	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
180	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
181	168, 161	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
182		pirp 23353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
183		2timesgt 37398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
184	182, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
185	184, 131	breqtri 4385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
187	173, 179, 180, 181, 186	lttrd 9742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
188		modid 12066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
189	173, 174, 178, 187, 188	syl22anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
190	189, 181	eqbrtrd 4382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191	190	iftrued 3857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192	191	mpteq2ia 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193	169, 172, 192	3eqtrri 2450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
194	193	oveq2i 6255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
195		reelprrecn 9577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
196	195	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
197		iooretop 21723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
198		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ℂ_fld
199	198	tgioo2 21758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
200	197, 199	eleqtri 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ℂ_fld ↾_t
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
202		1cnd 9605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
203	196, 201, 202	dvmptconst 37668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
204	203	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
205		ssid 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
206		ax-resscn 9542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
207		fss 5692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
208	109, 206, 207	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
209		dvresioo 37676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
210	205, 208, 209	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	194, 204, 210	3eqtr3i 2453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212	211	dmeqi 4993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
213		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
214	89, 213	dmmpti 5663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
215	212, 214	eqtr3i 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
216		ssdmres 5083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
217	215, 216	mpbir 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
218	217	sseli 3398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
219	168, 218	elind 3588	. . . . . . . . . . . . . . . . . . . . . . . . . 26
220		dmres 5082	. . . . . . . . . . . . . . . . . . . . . . . . . 26
221	219, 220	syl6eleqr 2512	. . . . . . . . . . . . . . . . . . . . . . . . 25
222	163, 221	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
223	222	adantlr 719	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
224	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
225	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
226	155	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
227		ioogtlb 37484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
228	159, 153, 227	mp3an12 1350	. . . . . . . . . . . . . . . . . . . . . . . . . 26
229	228	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
230		0red 9590	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
231		neqne 37290	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
232	231	ad2antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
233		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
234	226, 230, 232, 233	lttri5d 37414	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
235	224, 225, 226, 229, 234	eliood 37487	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
236	67, 118, 68	ltleii 9703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
237		iooss2 11618	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
238	153, 236, 237	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
239	238	sseli 3398	. . . . . . . . . . . . . . . . . . . . . . . . . 26
240	104	reseq1i 5058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
241		ioossre 11642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
242		resmpt 5111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
243	241, 242	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
244	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
245		elioore 11612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
247	245, 246	modcld 12047	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
248	245, 143	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
249	52	2timesi 10676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
250	110, 249	eqtri 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
251	250	oveq2i 6255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
252		negpicn 23354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
253	252, 52, 52	addassi 9597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
254	253	eqcomi 2432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
255	52	negidi 9889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
256	52, 252, 255	addcomli 9771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
257	256	oveq1i 6254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
258	52	addid2i 9767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
259	257, 258	eqtri 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
260	251, 254, 259	3eqtrri 2450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
261	260	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
262	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
263	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
264	239, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
265	262, 245, 263, 264	ltadd1dd 10170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
266	261, 265	eqbrtrd 4382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
267	244, 248, 266	ltled 9729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
268		0red 9590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
269	158, 120	readdcli 9602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
271	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
272	271, 260	syl6breq 4401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
273	268, 270, 248, 272, 265	lttrd 9742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
274	268, 248, 273	ltled 9729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
275	245	recnd 9615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
276	121	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
277	275, 276	addcomd 9781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
278		iooltub 37502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$
279	159, 151, 278	mp3an12 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
280		ltaddneg 37405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
281	245, 120, 280	sylancl 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
282	279, 281	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
283	277, 282	eqbrtrd 4382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
284	274, 283	jca 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
285		modid2 12069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
286	248, 133, 285	sylancl 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
287	284, 286	mpbird 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
288	125	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
289	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
290		1zzd 10914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
291	141, 289, 290, 136	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
292	288, 291	eqtrd 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
293	245, 292	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
294	287, 293	eqtr3d 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
295	267, 294	breqtrd 4386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
296	244, 247, 295	lensymd 9732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
297	296	iffalsed 3860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
298	297	mpteq2ia 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
299	240, 243, 298	3eqtrri 2450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
300	299	oveq2i 6255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
301		iooretop 21723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
302	301, 199	eleqtri 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
303	302	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ℂ_fld ↾_t
304	202	negcld 9919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
305	196, 303, 304	dvmptconst 37668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
306	305	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
307		dvresioo 37676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
308	205, 208, 307	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
309	300, 306, 308	3eqtr3i 2453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
310	309	dmeqi 4993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
311		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
312	89, 311	dmmpti 5663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
313	310, 312	eqtr3i 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314		ssdmres 5083	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
315	313, 314	mpbir 212	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
316	315	sseli 3398	. . . . . . . . . . . . . . . . . . . . . . . . . 26
317	239, 316	elind 3588	. . . . . . . . . . . . . . . . . . . . . . . . 25
318	317, 220	syl6eleqr 2512	. . . . . . . . . . . . . . . . . . . . . . . 24
319	235, 318	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
320	223, 319	pm2.61dan 798	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
321	150, 320	sylan 473	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
322		eldifn 3526	. . . . . . . . . . . . . . . . . . . . . 22 $\$
323	322	adantr 466	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
324	321, 323	condan 801	. . . . . . . . . . . . . . . . . . . 20 $\$
325		elsn 3950	. . . . . . . . . . . . . . . . . . . 20
326	324, 325	sylibr 215	. . . . . . . . . . . . . . . . . . 19 $\$
327	326	ssriv 3406	. . . . . . . . . . . . . . . . . 18 $\$
328		ssfi 7740	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$
329	149, 327, 328	mp2an 676	. . . . . . . . . . . . . . . . 17 $\$
330		inss1 3620	. . . . . . . . . . . . . . . . . . . . . 22
331	220, 330	eqsstri 3432	. . . . . . . . . . . . . . . . . . . . 21
332		ioosscn 37483	. . . . . . . . . . . . . . . . . . . . 21
333	331, 332	sstri 3411	. . . . . . . . . . . . . . . . . . . 20
334	333	a1i 11	. . . . . . . . . . . . . . . . . . 19
335		dvf 22799	. . . . . . . . . . . . . . . . . . . . . 22
336		fresin 5707	. . . . . . . . . . . . . . . . . . . . . 22
337		ffdm 5698	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
338	335, 336, 337	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 $/\$
339	338	simpli 459	. . . . . . . . . . . . . . . . . . . 20
340	339	a1i 11	. . . . . . . . . . . . . . . . . . 19
341	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
342	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
343		ioossre 11642	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
344	331	sseli 3398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
345	343, 344	sseldi 3400	. . . . . . . . . . . . . . . . . . . . . . . . . 26
346	345	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
347	344, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
348	347	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
349		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
350	341, 342, 346, 348, 349	eliood 37487	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
351		elun1 3571	. . . . . . . . . . . . . . . . . . . . . . . 24
352	350, 351	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
353		simpl 458	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
354		0red 9590	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
355	345	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
356		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
357	354, 355, 356	nltled 9731	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
358		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
359	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
360		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
361	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
362		0red 9590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
363		mnfxr 11360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
364	363	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
365	362	mnfltd 11372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
366	360, 364, 362, 365	lptioo2 37594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
367		incom 3593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
368		ioossre 11642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
369		df-ss 3388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
370	368, 369	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
371	367, 370	eqtr2i 2446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
372	371	fveq2i 5823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
373	366, 372	syl6eleq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
374		pnfxr 11358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
376	362	ltpnfd 11369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
377	360, 362, 375, 376	lptioo1 37595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
378		incom 3593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
379		ioossre 11642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
380		df-ss 3388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
381	379, 380	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
382	378, 381	eqtr2i 2446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
383	382	fveq2i 5823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384	377, 383	syl6eleq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
385		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
386		mnfle 11381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
387	159, 386	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
388		iooss1 11617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
389	363, 387, 388	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
390	389	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
391		ioosscn 37483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
392	390, 391	syl6ss 3414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
393		0cnd 9582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
394	385, 392, 304, 393	constlimc 37587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
395		resabs1 5090	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
396	389, 395	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
397	299, 396	eqtr4i 2448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
398	397	oveq1i 6254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
399		fssres 5704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
400	208, 368, 399	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
401	400	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
402	391	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
403		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
404		0le0 10645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
405		elioc2 11643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
406	159, 67, 405	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
407	67, 164, 404, 406	mpbir3an 1187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
408	198	cnfldtop 21741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld
409		ovex 6272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
410		resttop 20113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
411	408, 409, 410	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
412	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
413		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
414	387	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
415	364, 412, 362, 360, 413, 414, 362	iocopn 37513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
416	415	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
417	199	oveq1i 6254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
418		iocssre 11660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
419	363, 67, 418	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
420	195	elexi 3027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
421		restabs 20118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
422	408, 419, 420, 421	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
423	417, 422	eqtri 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
424	416, 423	eleqtri 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
425		isopn3i 20035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
426	411, 424, 425	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
427		mnflt0 11373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
428		snunioo2 37498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
429	363, 151, 427, 428	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
430	429	eqcomi 2432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
431	430	oveq2i 6255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
432	431	fveq2i 5823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
433		snunioo2 37498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
434	159, 151, 164, 433	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
435	434	eqcomi 2432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
436	432, 435	fveq12i 5825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
437	426, 436	eqtr3i 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
438	407, 437	eleqtri 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
439	438	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
440	401, 390, 402, 198, 403, 439	limcres 22778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
441	440	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
442	398, 441	eqtri 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
443	394, 442	syl6eleq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
444		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
445		ioosscn 37483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
446	445	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
447	444, 446, 202, 393	constlimc 37587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
448		ltpnf 11368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
449		xrltle 11394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
450	153, 374, 449	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
451	118, 448, 450	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
452		iooss2 11618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
453	374, 451, 452	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
454		resabs1 5090	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
455	453, 454	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
456	193, 455	eqtr4i 2448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
457	456	oveq1i 6254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
458		fssres 5704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
459	208, 379, 458	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
460	459	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
461	453	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
462		ioosscn 37483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
463	462	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
464		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
465		elico2 11644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
466	67, 153, 465	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
467	67, 404, 68, 466	mpbir3an 1187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
468		ovex 6272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
469		resttop 20113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
470	408, 468, 469	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
471	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
472		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
473	451	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
474	362, 471, 375, 360, 472, 473	icoopn 37518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
475	474	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
476	199	oveq1i 6254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
477		rge0ssre 11686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
478		restabs 20118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
479	408, 477, 420, 478	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
480	476, 479	eqtri 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
481	475, 480	eleqtri 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
482		isopn3i 20035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
483	470, 481, 482	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
484		0ltpnf 11370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
485		snunioo1 37505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
486	151, 374, 484, 485	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
487	486	eqcomi 2432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
488	487	oveq2i 6255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
489	488	fveq2i 5823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
490		snunioo1 37505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
491	151, 153, 68, 490	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
492	491	eqcomi 2432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
493	489, 492	fveq12i 5825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
494	483, 493	eqtr3i 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
495	467, 494	eleqtri 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
496	495	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
497	460, 461, 463, 198, 464, 496	limcres 22778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
498	497	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
499	457, 498	eqtri 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
500	447, 499	syl6eleq 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
501		neg1lt0 10662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
502	106, 67, 105	lttri 9706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
503	501, 34, 502	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
504	106, 503	ltneii 9693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
505	504	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
506	198, 359, 360, 361, 362, 373, 384, 443, 500, 505	jumpncnp 37659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
507	506	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
508	206	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
509	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
510	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
511		inss2 3621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
512	220, 511	eqsstri 3432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
513	512	sseli 3398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
514	199, 198	dvcnp2 22811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ ℂ_fld
515	508, 509, 510, 513, 514	syl31anc 1267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
516	507, 515	mto 179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
517	516	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
518	358, 517	eqneltrd 2520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
519	518	necon2ai 2625	. . . . . . . . . . . . . . . . . . . . . . . . . 26
520	519	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
521	354, 355, 357, 520	leneltd 9735	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
522	344, 163	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
523		elun2 3572	. . . . . . . . . . . . . . . . . . . . . . . . 25
524	522, 523	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
525	353, 521, 524	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
526	352, 525	pm2.61dan 798	. . . . . . . . . . . . . . . . . . . . . 22
527		ovex 6272	. . . . . . . . . . . . . . . . . . . . . . 23
528		ovex 6272	. . . . . . . . . . . . . . . . . . . . . . 23
529	527, 528	unipr 4170	. . . . . . . . . . . . . . . . . . . . . 22
530	526, 529	syl6eleqr 2512	. . . . . . . . . . . . . . . . . . . . 21
531	530	ssriv 3406	. . . . . . . . . . . . . . . . . . . 20
532	531	a1i 11	. . . . . . . . . . . . . . . . . . 19
533		ineq2 3596	. . . . . . . . . . . . . . . . . . . . . . 23
534		retop 21719	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
535		ovex 6272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
536	535	resex 5105	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
537	536	dmex 6679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
538	534, 537	pm3.2i 456	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
539	318	ssriv 3406	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
540		ssid 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
541	301, 539, 540	3pm3.2i 1183	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
542		restopnb 20128	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
543	538, 541, 542	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
544	301, 543	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
545		inss2 3621	. . . . . . . . . . . . . . . . . . . . . . . . 25
546	539, 540	ssini 3623	. . . . . . . . . . . . . . . . . . . . . . . . 25
547	545, 546	eqssi 3418	. . . . . . . . . . . . . . . . . . . . . . . 24
548	199	oveq1i 6254	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t ℂ_fld ↾_t ↾_t
549	331, 343	sstri 3411	. . . . . . . . . . . . . . . . . . . . . . . . . 26
550		restabs 20118	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
551	408, 549, 420, 550	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
552	548, 551	eqtr2i 2446	. . . . . . . . . . . . . . . . . . . . . . . 24 ℂ_fld ↾_t ↾_t
553	544, 547, 552	3eltr4i 2514	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
554	533, 553	syl6eqel 2509	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ↾_t
555	554	adantl 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ℂ_fld ↾_t
556		neqne 37290	. . . . . . . . . . . . . . . . . . . . . . 23
557		elprn1 37596	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
558	556, 557	sylan2 476	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
559		ineq2 3596	. . . . . . . . . . . . . . . . . . . . . . 23
560	221	ssriv 3406	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
561		ssid 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
562	197, 560, 561	3pm3.2i 1183	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
563		restopnb 20128	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
564	538, 562, 563	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
565	197, 564	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
566		inss2 3621	. . . . . . . . . . . . . . . . . . . . . . . . 25
567	560, 561	ssini 3623	. . . . . . . . . . . . . . . . . . . . . . . . 25
568	566, 567	eqssi 3418	. . . . . . . . . . . . . . . . . . . . . . . 24
569	565, 568, 552	3eltr4i 2514	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
570	559, 569	syl6eqel 2509	. . . . . . . . . . . . . . . . . . . . . 22