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 32180

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 11036	. . . . . . 7
2		1zzd 10812	. . . . . . 7
3		eqidd 2383	. . . . . . . . 9
4		oveq2 6204	. . . . . . . . . . . . . 14
5	4	oveq1d 6211	. . . . . . . . . . . . 13
6	5	oveq1d 6211	. . . . . . . . . . . 12
7	6	fveq2d 5778	. . . . . . . . . . 11
8	7, 5	oveq12d 6214	. . . . . . . . . 10
9	8	adantl 464	. . . . . . . . 9 $/\$
10		id 22	. . . . . . . . 9
11		ovex 6224	. . . . . . . . . 10
12	11	a1i 11	. . . . . . . . 9
13	3, 9, 10, 12	fvmptd 5862	. . . . . . . 8
14	13	adantl 464	. . . . . . 7 $/\$
15		2z 10813	. . . . . . . . . . . . . . 15
16	15	a1i 11	. . . . . . . . . . . . . 14
17		nnz 10803	. . . . . . . . . . . . . 14
18	16, 17	zmulcld 10890	. . . . . . . . . . . . 13
19		1zzd 10812	. . . . . . . . . . . . 13
20	18, 19	zsubcld 10889	. . . . . . . . . . . 12
21	20	zcnd 10885	. . . . . . . . . . 11
22		fouriersw.x	. . . . . . . . . . . . 13
23	22	recni 9519	. . . . . . . . . . . 12
24	23	a1i 11	. . . . . . . . . . 11
25	21, 24	mulcld 9527	. . . . . . . . . 10
26	25	sincld 13867	. . . . . . . . 9
27		0red 9508	. . . . . . . . . 10
28		2re 10522	. . . . . . . . . . . . . 14
29	28	a1i 11	. . . . . . . . . . . . 13
30		1red 9522	. . . . . . . . . . . . 13
31	29, 30	remulcld 9535	. . . . . . . . . . . 12
32	31, 30	resubcld 9905	. . . . . . . . . . 11
33	20	zred 10884	. . . . . . . . . . 11
34		0lt1 9992	. . . . . . . . . . . . 13
35		2t1e2 10601	. . . . . . . . . . . . . . 15
36	35	oveq1i 6206	. . . . . . . . . . . . . 14
37		2m1e1 10567	. . . . . . . . . . . . . 14
38	36, 37	eqtr2i 2412	. . . . . . . . . . . . 13
39	34, 38	breqtri 4390	. . . . . . . . . . . 12
40	39	a1i 11	. . . . . . . . . . 11
41	18	zred 10884	. . . . . . . . . . . 12
42		nnre 10459	. . . . . . . . . . . . 13
43		0le2 10543	. . . . . . . . . . . . . 14
44	43	a1i 11	. . . . . . . . . . . . 13
45		nnge1 10478	. . . . . . . . . . . . 13
46	30, 42, 29, 44, 45	lemul2ad 10402	. . . . . . . . . . . 12
47	31, 41, 30, 46	lesub1dd 10085	. . . . . . . . . . 11
48	27, 32, 33, 40, 47	ltletrd 9653	. . . . . . . . . 10
49	27, 48	gtned 9631	. . . . . . . . 9
50	26, 21, 49	divcld 10237	. . . . . . . 8
51	50	adantl 464	. . . . . . 7 $/\$
52		picn 22937	. . . . . . . . . . 11
53	52	a1i 11	. . . . . . . . . 10
54		4cn 10530	. . . . . . . . . . 11
55	54	a1i 11	. . . . . . . . . 10
56		4ne0 10549	. . . . . . . . . . 11
57	56	a1i 11	. . . . . . . . . 10
58	53, 55, 57	divcld 10237	. . . . . . . . 9
59		eqid 2382	. . . . . . . . . . . . . . . 16
60		0cnd 9500	. . . . . . . . . . . . . . . . 17
61	54	a1i 11	. . . . . . . . . . . . . . . . . . 19
62		nncn 10460	. . . . . . . . . . . . . . . . . . . 20
63		mulcl 9487	. . . . . . . . . . . . . . . . . . . 20 $/\$
64	62, 52, 63	sylancl 660	. . . . . . . . . . . . . . . . . . 19
65	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20
66		nnne0 10485	. . . . . . . . . . . . . . . . . . . 20
67		0re 9507	. . . . . . . . . . . . . . . . . . . . . 22
68		pipos 22938	. . . . . . . . . . . . . . . . . . . . . 22
69	67, 68	gtneii 9607	. . . . . . . . . . . . . . . . . . . . 21
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . 20
71	62, 65, 66, 70	mulne0d 10118	. . . . . . . . . . . . . . . . . . 19
72	61, 64, 71	divcld 10237	. . . . . . . . . . . . . . . . . 18
73	23	a1i 11	. . . . . . . . . . . . . . . . . . . 20
74	62, 73	mulcld 9527	. . . . . . . . . . . . . . . . . . 19
75	74	sincld 13867	. . . . . . . . . . . . . . . . . 18
76	72, 75	mulcld 9527	. . . . . . . . . . . . . . . . 17
77	60, 76	ifcld 3900	. . . . . . . . . . . . . . . 16
78	59, 77	fmpti 5956	. . . . . . . . . . . . . . 15
79	78	a1i 11	. . . . . . . . . . . . . 14
80		eqidd 2383	. . . . . . . . . . . . . . . . . 18
81		breq2 4371	. . . . . . . . . . . . . . . . . . . 20
82		oveq1 6203	. . . . . . . . . . . . . . . . . . . . . 22
83	82	oveq2d 6212	. . . . . . . . . . . . . . . . . . . . 21
84		oveq1 6203	. . . . . . . . . . . . . . . . . . . . . 22
85	84	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . 21
86	83, 85	oveq12d 6214	. . . . . . . . . . . . . . . . . . . 20
87	81, 86	ifbieq2d 3882	. . . . . . . . . . . . . . . . . . 19
88	87	adantl 464	. . . . . . . . . . . . . . . . . 18 $/\$
89		c0ex 9501	. . . . . . . . . . . . . . . . . . . 20
90		ovex 6224	. . . . . . . . . . . . . . . . . . . 20
91	89, 90	ifex 3925	. . . . . . . . . . . . . . . . . . 19
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18
93	80, 88, 10, 92	fvmptd 5862	. . . . . . . . . . . . . . . . 17
94	93	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
95		simpr 459	. . . . . . . . . . . . . . . . . 18 $/\$
96		simpl 455	. . . . . . . . . . . . . . . . . . 19 $/\$
97		2nn 10610	. . . . . . . . . . . . . . . . . . 19
98		nndivdvds 13994	. . . . . . . . . . . . . . . . . . 19 $/\$
99	96, 97, 98	sylancl 660	. . . . . . . . . . . . . . . . . 18 $/\$
100	95, 99	mpbird 232	. . . . . . . . . . . . . . . . 17 $/\$
101	100	iftrued 3865	. . . . . . . . . . . . . . . 16 $/\$
102	94, 101	eqtrd 2423	. . . . . . . . . . . . . . 15 $/\$
103	102	3adant1 1012	. . . . . . . . . . . . . 14 $/\$ $/\$
104		fouriersw.f	. . . . . . . . . . . . . . . . . 18
105		1re 9506	. . . . . . . . . . . . . . . . . . . 20
106	105	renegcli 9793	. . . . . . . . . . . . . . . . . . . 20
107	105, 106	keepel 3924	. . . . . . . . . . . . . . . . . . 19
108	107	a1i 11	. . . . . . . . . . . . . . . . . 18
109	104, 108	fmpti 5956	. . . . . . . . . . . . . . . . 17
110		fouriersw.t	. . . . . . . . . . . . . . . . 17
111		oveq1 6203	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	breq1d 4377	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	ifbid 3879	. . . . . . . . . . . . . . . . . . . . . 22
114	113	cbvmptv 4458	. . . . . . . . . . . . . . . . . . . . 21
115	104, 114	eqtri 2411	. . . . . . . . . . . . . . . . . . . 20
116	115	a1i 11	. . . . . . . . . . . . . . . . . . 19
117		oveq1 6203	. . . . . . . . . . . . . . . . . . . . . . . 24
118		pire 22936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	28, 118	remulcli 9521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	110, 119	eqeltri 2466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	120	recni 9519	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	121	mulid2i 9510	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
123	122	eqcomi 2395	. . . . . . . . . . . . . . . . . . . . . . . . . 26
124	123	oveq2i 6207	. . . . . . . . . . . . . . . . . . . . . . . . 25
125	124	oveq1i 6206	. . . . . . . . . . . . . . . . . . . . . . . 24
126	117, 125	syl6eq 2439	. . . . . . . . . . . . . . . . . . . . . . 23
127	126	adantl 464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
128		simpl 455	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
129		2pos 10544	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
130	28, 118, 129, 68	mulgt0ii 9629	. . . . . . . . . . . . . . . . . . . . . . . . . 26
131	110	eqcomi 2395	. . . . . . . . . . . . . . . . . . . . . . . . . 26
132	130, 131	breqtri 4390	. . . . . . . . . . . . . . . . . . . . . . . . 25
133	120, 132	elrpii 11142	. . . . . . . . . . . . . . . . . . . . . . . 24
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
135		1zzd 10812	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136		modcyc 11932	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
137	128, 134, 135, 136	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
138	127, 137	eqtrd 2423	. . . . . . . . . . . . . . . . . . . . 21 $/\$
139	138	breq1d 4377	. . . . . . . . . . . . . . . . . . . 20 $/\$
140	139	ifbid 3879	. . . . . . . . . . . . . . . . . . 19 $/\$
141		id 22	. . . . . . . . . . . . . . . . . . . 20
142	120	a1i 11	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	readdcld 9534	. . . . . . . . . . . . . . . . . . 19
144	116, 140, 143, 108	fvmptd 5862	. . . . . . . . . . . . . . . . . 18
145	104	fvmpt2 5865	. . . . . . . . . . . . . . . . . . 19 $/\$
146	107, 145	mpan2 669	. . . . . . . . . . . . . . . . . 18
147	144, 146	eqtr4d 2426	. . . . . . . . . . . . . . . . 17
148		eqid 2382	. . . . . . . . . . . . . . . . 17
149		snfi 7515	. . . . . . . . . . . . . . . . . 18
150		eldifi 3540	. . . . . . . . . . . . . . . . . . . . . 22 $\$
151		0xr 9551	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
152	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
153	118	rexri 9557	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
154	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155		elioore 11480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
156	155	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
157		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
158	118	renegcli 9793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159	158	rexri 9557	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
160		iooltub 31714	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
161	159, 153, 160	mp3an12 1312	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
162	161	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
163	152, 154, 156, 157, 162	eliood 31697	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
164		negpilt0 31629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
165	158, 67, 164	ltleii 9618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
166		iooss1 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
167	159, 165, 166	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168	167	sseli 3413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
169	104	reseq1i 5182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
170		ioossre 11507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
171		resmpt 5235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
172	170, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
173		elioore 11480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
174	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
175		0red 9508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
176		ioogtlb 31694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
177	151, 153, 176	mp3an12 1312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
178	175, 173, 177	ltled 9644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
179	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
180	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
181	168, 161	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
182		pirp 22939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
183		2timesgt 31642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
184	182, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
185	184, 131	breqtri 4390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
187	173, 179, 180, 181, 186	lttrd 9654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
188		modid 11921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
189	173, 174, 178, 187, 188	syl22anc 1227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
190	189, 181	eqbrtrd 4387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191	190	iftrued 3865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192	191	mpteq2ia 4449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193	169, 172, 192	3eqtrri 2416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
194	193	oveq2i 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
195		reelprrecn 9495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
196	195	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
197		iooretop 21358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
198		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ℂ_fld
199	198	tgioo2 21393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
200	197, 199	eleqtri 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ℂ_fld ↾_t
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
202		1cnd 9523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
203	196, 201, 202	dvmptconst 31876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
204	203	trud 1408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
205		ssid 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
206		ax-resscn 9460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
207		fss 5647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
208	109, 206, 207	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
209		dvresioo 31884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
210	205, 208, 209	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	194, 204, 210	3eqtr3i 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212	211	dmeqi 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
213		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
214	89, 213	dmmpti 5618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
215	212, 214	eqtr3i 2413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
216		ssdmres 5207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
217	215, 216	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
218	217	sseli 3413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
219	168, 218	elind 3602	. . . . . . . . . . . . . . . . . . . . . . . . . 26
220		dmres 5206	. . . . . . . . . . . . . . . . . . . . . . . . . 26
221	219, 220	syl6eleqr 2481	. . . . . . . . . . . . . . . . . . . . . . . . 25
222	163, 221	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
223	222	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
224	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
225	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
226	155	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
227		ioogtlb 31694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
228	159, 153, 227	mp3an12 1312	. . . . . . . . . . . . . . . . . . . . . . . . . 26
229	228	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
230		0red 9508	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
231		neqne 31601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
232	231	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
233		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
234	226, 230, 232, 233	lttri5d 31665	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
235	224, 225, 226, 229, 234	eliood 31697	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
236	67, 118, 68	ltleii 9618	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
237		iooss2 11486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
238	153, 236, 237	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
239	238	sseli 3413	. . . . . . . . . . . . . . . . . . . . . . . . . 26
240	104	reseq1i 5182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
241		ioossre 11507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
242		resmpt 5235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
243	241, 242	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
244	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
245		elioore 11480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
247	245, 246	modcld 11902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
248	245, 143	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
249	52	2timesi 10573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
250	110, 249	eqtri 2411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
251	250	oveq2i 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
252		negpicn 22940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
253	252, 52, 52	addassi 9515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
254	253	eqcomi 2395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
255	52	negidi 9801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
256	52, 252, 255	addcomli 9683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
257	256	oveq1i 6206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
258	52	addid2i 9679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
259	257, 258	eqtri 2411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
260	251, 254, 259	3eqtrri 2416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
261	260	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
262	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
263	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
264	239, 228	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
265	262, 245, 263, 264	ltadd1dd 10080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
266	261, 265	eqbrtrd 4387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
267	244, 248, 266	ltled 9644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
268		0red 9508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
269	158, 120	readdcli 9520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
271	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
272	271, 260	syl6breq 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
273	268, 270, 248, 272, 265	lttrd 9654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
274	268, 248, 273	ltled 9644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
275	245	recnd 9533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
276	121	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
277	275, 276	addcomd 9693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
278		iooltub 31714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$
279	159, 151, 278	mp3an12 1312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
280		ltaddneg 31651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
281	245, 120, 280	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
282	279, 281	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
283	277, 282	eqbrtrd 4387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
284	274, 283	jca 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
285		modid2 11924	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
286	248, 133, 285	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
287	284, 286	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
288	125	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
289	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
290		1zzd 10812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
291	141, 289, 290, 136	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
292	288, 291	eqtrd 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
293	245, 292	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
294	287, 293	eqtr3d 2425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
295	267, 294	breqtrd 4391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
296	244, 247, 295	leimnltd 31639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
297	296	iffalsed 3868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
298	297	mpteq2ia 4449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
299	240, 243, 298	3eqtrri 2416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
300	299	oveq2i 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
301		iooretop 21358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
302	301, 199	eleqtri 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
303	302	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ℂ_fld ↾_t
304	202	negcld 9831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
305	196, 303, 304	dvmptconst 31876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
306	305	trud 1408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
307		dvresioo 31884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
308	205, 208, 307	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
309	300, 306, 308	3eqtr3i 2419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
310	309	dmeqi 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
311		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
312	89, 311	dmmpti 5618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
313	310, 312	eqtr3i 2413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314		ssdmres 5207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
315	313, 314	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
316	315	sseli 3413	. . . . . . . . . . . . . . . . . . . . . . . . . 26
317	239, 316	elind 3602	. . . . . . . . . . . . . . . . . . . . . . . . 25
318	317, 220	syl6eleqr 2481	. . . . . . . . . . . . . . . . . . . . . . . 24
319	235, 318	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
320	223, 319	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
321	150, 320	sylan 469	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
322		eldifn 3541	. . . . . . . . . . . . . . . . . . . . . 22 $\$
323	322	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
324	321, 323	condan 792	. . . . . . . . . . . . . . . . . . . 20 $\$
325		elsn 3958	. . . . . . . . . . . . . . . . . . . 20
326	324, 325	sylibr 212	. . . . . . . . . . . . . . . . . . 19 $\$
327	326	ssriv 3421	. . . . . . . . . . . . . . . . . 18 $\$
328		ssfi 7656	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$
329	149, 327, 328	mp2an 670	. . . . . . . . . . . . . . . . 17 $\$
330		inss1 3632	. . . . . . . . . . . . . . . . . . . . . 22
331	220, 330	eqsstri 3447	. . . . . . . . . . . . . . . . . . . . 21
332		ioosscn 31693	. . . . . . . . . . . . . . . . . . . . 21
333	331, 332	sstri 3426	. . . . . . . . . . . . . . . . . . . 20
334	333	a1i 11	. . . . . . . . . . . . . . . . . . 19
335		dvf 22396	. . . . . . . . . . . . . . . . . . . . . 22
336		fresin 5662	. . . . . . . . . . . . . . . . . . . . . 22
337		ffdm 5653	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
338	335, 336, 337	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 $/\$
339	338	simpli 456	. . . . . . . . . . . . . . . . . . . 20
340	339	a1i 11	. . . . . . . . . . . . . . . . . . 19
341	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
342	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
343		ioossre 11507	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
344	331	sseli 3413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
345	343, 344	sseldi 3415	. . . . . . . . . . . . . . . . . . . . . . . . . 26
346	345	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
347	344, 228	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26
348	347	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
349		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
350	341, 342, 346, 348, 349	eliood 31697	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
351		elun1 3585	. . . . . . . . . . . . . . . . . . . . . . . 24
352	350, 351	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
353		simpl 455	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
354		0red 9508	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
355	345	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
356		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
357	354, 355, 356	nltled 31644	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
358		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
359	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
360		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
361	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
362		0red 9508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
363		mnfxr 11244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
364	363	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
365	362	mnfltd 31657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
366	360, 364, 362, 365	lptioo2 31803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
367		incom 3605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
368		ioossre 11507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
369		df-ss 3403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
370	368, 369	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
371	367, 370	eqtr2i 2412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
372	371	fveq2i 5777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
373	366, 372	syl6eleq 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
374		pnfxr 11242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
376	362	ltpnfd 31647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
377	360, 362, 375, 376	lptioo1 31804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
378		incom 3605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
379		ioossre 11507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
380		df-ss 3403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
381	379, 380	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
382	378, 381	eqtr2i 2412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
383	382	fveq2i 5777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384	377, 383	syl6eleq 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
385		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
386		mnfle 11263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
387	159, 386	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
388		iooss1 11485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
389	363, 387, 388	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
390	389	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
391		ioosscn 31693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
392	390, 391	syl6ss 3429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
393		0cnd 9500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
394	385, 392, 304, 393	constlimc 31796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
395		resabs1 5214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
396	389, 395	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
397	299, 396	eqtr4i 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
398	397	oveq1i 6206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
399		fssres 5659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
400	208, 368, 399	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
401	400	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
402	391	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
403		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
404		0le0 10542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
405		elioc2 11508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
406	159, 67, 405	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
407	67, 164, 404, 406	mpbir3an 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
408	198	cnfldtop 21376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld
409		ovex 6224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
410		resttop 19747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
411	408, 409, 410	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
412	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
413		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
414	387	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
415	364, 412, 362, 360, 413, 414, 362	iocopn 31726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
416	415	trud 1408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
417	199	oveq1i 6206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
418		iocssre 11525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
419	363, 67, 418	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
420	195	elexi 3044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
421		restabs 19752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
422	408, 419, 420, 421	mp3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
423	417, 422	eqtri 2411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
424	416, 423	eleqtri 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
425		isopn3i 19669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
426	411, 424, 425	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
427		mnflt0 11255	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
428		snunioo2 31710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
429	363, 151, 427, 428	mp3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
430	429	eqcomi 2395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
431	430	oveq2i 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
432	431	fveq2i 5777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
433		snunioo2 31710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
434	159, 151, 164, 433	mp3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
435	434	eqcomi 2395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
436	432, 435	fveq12i 5779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
437	426, 436	eqtr3i 2413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
438	407, 437	eleqtri 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
439	438	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
440	401, 390, 402, 198, 403, 439	limcres 22375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
441	440	trud 1408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
442	398, 441	eqtri 2411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
443	394, 442	syl6eleq 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
444		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
445		ioosscn 31693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
446	445	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
447	444, 446, 202, 393	constlimc 31796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
448		ltpnf 11252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
449		xrltle 11276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
450	153, 374, 449	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
451	118, 448, 450	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
452		iooss2 11486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
453	374, 451, 452	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
454		resabs1 5214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
455	453, 454	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
456	193, 455	eqtr4i 2414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
457	456	oveq1i 6206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
458		fssres 5659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
459	208, 379, 458	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
460	459	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
461	453	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
462		ioosscn 31693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
463	462	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
464		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
465		elico2 11509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
466	67, 153, 465	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
467	67, 404, 68, 466	mpbir3an 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
468		ovex 6224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
469		resttop 19747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
470	408, 468, 469	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
471	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
472		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
473	451	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
474	362, 471, 375, 360, 472, 473	icoopn 31731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
475	474	trud 1408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
476	199	oveq1i 6206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
477		rge0ssre 11549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
478		restabs 19752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
479	408, 477, 420, 478	mp3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
480	476, 479	eqtri 2411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
481	475, 480	eleqtri 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
482		isopn3i 19669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
483	470, 481, 482	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
484		0ltpnf 11253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
485		snunioo1 31718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
486	151, 374, 484, 485	mp3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
487	486	eqcomi 2395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
488	487	oveq2i 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
489	488	fveq2i 5777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
490		snunioo1 31718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
491	151, 153, 68, 490	mp3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
492	491	eqcomi 2395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
493	489, 492	fveq12i 5779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
494	483, 493	eqtr3i 2413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
495	467, 494	eleqtri 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
496	495	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
497	460, 461, 463, 198, 464, 496	limcres 22375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
498	497	trud 1408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
499	457, 498	eqtri 2411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
500	447, 499	syl6eleq 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
501		neg1lt0 10559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
502	106, 67, 105	lttri 9621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
503	501, 34, 502	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
504	106, 503	ltneii 9608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
505	504	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
506	198, 359, 360, 361, 362, 373, 384, 443, 500, 505	jumpncnp 31867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
507	506	trud 1408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
508	206	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
509	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
510	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
511		inss2 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
512	220, 511	eqsstri 3447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
513	512	sseli 3413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
514	199, 198	dvcnp2 22408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ ℂ_fld
515	508, 509, 510, 513, 514	syl31anc 1229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
516	507, 515	mto 176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
517	516	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
518	358, 517	eqneltrd 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
519	518	necon2ai 2617	. . . . . . . . . . . . . . . . . . . . . . . . . 26
520	519	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
521	354, 355, 357, 520	leneltd 31660	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
522	344, 163	sylan 469	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
523		elun2 3586	. . . . . . . . . . . . . . . . . . . . . . . . 25
524	522, 523	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
525	353, 521, 524	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
526	352, 525	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . . . 22
527		ovex 6224	. . . . . . . . . . . . . . . . . . . . . . 23
528		ovex 6224	. . . . . . . . . . . . . . . . . . . . . . 23
529	527, 528	unipr 4176	. . . . . . . . . . . . . . . . . . . . . 22
530	526, 529	syl6eleqr 2481	. . . . . . . . . . . . . . . . . . . . 21
531	530	ssriv 3421	. . . . . . . . . . . . . . . . . . . 20
532	531	a1i 11	. . . . . . . . . . . . . . . . . . 19
533		ineq2 3608	. . . . . . . . . . . . . . . . . . . . . . 23
534		retop 21353	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
535		ovex 6224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
536	535	resex 5229	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
537	536	dmex 6632	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
538	534, 537	pm3.2i 453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
539	318	ssriv 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
540		ssid 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
541	301, 539, 540	3pm3.2i 1172	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
542		restopnb 19762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
543	538, 541, 542	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
544	301, 543	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
545		inss2 3633	. . . . . . . . . . . . . . . . . . . . . . . . 25
546	539, 540	ssini 3635	. . . . . . . . . . . . . . . . . . . . . . . . 25
547	545, 546	eqssi 3433	. . . . . . . . . . . . . . . . . . . . . . . 24
548	199	oveq1i 6206	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t ℂ_fld ↾_t ↾_t
549	331, 343	sstri 3426	. . . . . . . . . . . . . . . . . . . . . . . . . 26
550		restabs 19752	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
551	408, 549, 420, 550	mp3an 1322	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
552	548, 551	eqtr2i 2412	. . . . . . . . . . . . . . . . . . . . . . . 24 ℂ_fld ↾_t ↾_t
553	544, 547, 552	3eltr4i 2483	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
554	533, 553	syl6eqel 2478	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ↾_t
555	554	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ℂ_fld ↾_t
556		neqne 31601	. . . . . . . . . . . . . . . . . . . . . . 23
557		elprn1 31805	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
558	556, 557	sylan2 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
559		ineq2 3608	. . . . . . . . . . . . . . . . . . . . . . 23
560	221	ssriv 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
561		ssid 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
562	197, 560, 561	3pm3.2i 1172	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
563		restopnb 19762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
564	538, 562, 563	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
565	197, 564	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
566		inss2 3633	. . . . . . . . . . . . . . . . . . . . . . . . 25
567	560, 561	ssini 3635	. . . . . . . . . . . . . . . . . . . . . . . . 25
568	566, 567	eqssi 3433	. . . . . . . . . . . . . . . . . . . . . . . 24
569	565, 568, 552	3eltr4i 2483	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
570	559, 569	syl6eqel 2478	. . . . . . . . . . . . . . . . . . . . . 22 <