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 37662

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 11194	. . . . . . 7
2		1zzd 10968	. . . . . . 7
3		eqidd 2430	. . . . . . . . 9
4		oveq2 6313	. . . . . . . . . . . . . 14
5	4	oveq1d 6320	. . . . . . . . . . . . 13
6	5	oveq1d 6320	. . . . . . . . . . . 12
7	6	fveq2d 5885	. . . . . . . . . . 11
8	7, 5	oveq12d 6323	. . . . . . . . . 10
9	8	adantl 467	. . . . . . . . 9 $/\$
10		id 23	. . . . . . . . 9
11		ovex 6333	. . . . . . . . . 10
12	11	a1i 11	. . . . . . . . 9
13	3, 9, 10, 12	fvmptd 5970	. . . . . . . 8
14	13	adantl 467	. . . . . . 7 $/\$
15		2z 10969	. . . . . . . . . . . . . . 15
16	15	a1i 11	. . . . . . . . . . . . . 14
17		nnz 10959	. . . . . . . . . . . . . 14
18	16, 17	zmulcld 11046	. . . . . . . . . . . . 13
19		1zzd 10968	. . . . . . . . . . . . 13
20	18, 19	zsubcld 11045	. . . . . . . . . . . 12
21	20	zcnd 11041	. . . . . . . . . . 11
22		fouriersw.x	. . . . . . . . . . . . 13
23	22	recni 9654	. . . . . . . . . . . 12
24	23	a1i 11	. . . . . . . . . . 11
25	21, 24	mulcld 9662	. . . . . . . . . 10
26	25	sincld 14162	. . . . . . . . 9
27		0red 9643	. . . . . . . . . 10
28		2re 10679	. . . . . . . . . . . . . 14
29	28	a1i 11	. . . . . . . . . . . . 13
30		1red 9657	. . . . . . . . . . . . 13
31	29, 30	remulcld 9670	. . . . . . . . . . . 12
32	31, 30	resubcld 10046	. . . . . . . . . . 11
33	20	zred 11040	. . . . . . . . . . 11
34		0lt1 10135	. . . . . . . . . . . . 13
35		2t1e2 10758	. . . . . . . . . . . . . . 15
36	35	oveq1i 6315	. . . . . . . . . . . . . 14
37		2m1e1 10724	. . . . . . . . . . . . . 14
38	36, 37	eqtr2i 2459	. . . . . . . . . . . . 13
39	34, 38	breqtri 4449	. . . . . . . . . . . 12
40	39	a1i 11	. . . . . . . . . . 11
41	18	zred 11040	. . . . . . . . . . . 12
42		nnre 10616	. . . . . . . . . . . . 13
43		0le2 10700	. . . . . . . . . . . . . 14
44	43	a1i 11	. . . . . . . . . . . . 13
45		nnge1 10635	. . . . . . . . . . . . 13
46	30, 42, 29, 44, 45	lemul2ad 10547	. . . . . . . . . . . 12
47	31, 41, 30, 46	lesub1dd 10228	. . . . . . . . . . 11
48	27, 32, 33, 40, 47	ltletrd 9794	. . . . . . . . . 10
49	27, 48	gtned 9769	. . . . . . . . 9
50	26, 21, 49	divcld 10382	. . . . . . . 8
51	50	adantl 467	. . . . . . 7 $/\$
52		picn 23279	. . . . . . . . . . 11
53	52	a1i 11	. . . . . . . . . 10
54		4cn 10687	. . . . . . . . . . 11
55	54	a1i 11	. . . . . . . . . 10
56		4ne0 10706	. . . . . . . . . . 11
57	56	a1i 11	. . . . . . . . . 10
58	53, 55, 57	divcld 10382	. . . . . . . . 9
59		eqid 2429	. . . . . . . . . . . . . . . 16
60		0cnd 9635	. . . . . . . . . . . . . . . . 17
61	54	a1i 11	. . . . . . . . . . . . . . . . . . 19
62		nncn 10617	. . . . . . . . . . . . . . . . . . . 20
63		mulcl 9622	. . . . . . . . . . . . . . . . . . . 20 $/\$
64	62, 52, 63	sylancl 666	. . . . . . . . . . . . . . . . . . 19
65	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20
66		nnne0 10642	. . . . . . . . . . . . . . . . . . . 20
67		0re 9642	. . . . . . . . . . . . . . . . . . . . . 22
68		pipos 23280	. . . . . . . . . . . . . . . . . . . . . 22
69	67, 68	gtneii 9745	. . . . . . . . . . . . . . . . . . . . 21
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . 20
71	62, 65, 66, 70	mulne0d 10263	. . . . . . . . . . . . . . . . . . 19
72	61, 64, 71	divcld 10382	. . . . . . . . . . . . . . . . . 18
73	23	a1i 11	. . . . . . . . . . . . . . . . . . . 20
74	62, 73	mulcld 9662	. . . . . . . . . . . . . . . . . . 19
75	74	sincld 14162	. . . . . . . . . . . . . . . . . 18
76	72, 75	mulcld 9662	. . . . . . . . . . . . . . . . 17
77	60, 76	ifcld 3958	. . . . . . . . . . . . . . . 16
78	59, 77	fmpti 6060	. . . . . . . . . . . . . . 15
79	78	a1i 11	. . . . . . . . . . . . . 14
80		eqidd 2430	. . . . . . . . . . . . . . . . . 18
81		breq2 4430	. . . . . . . . . . . . . . . . . . . 20
82		oveq1 6312	. . . . . . . . . . . . . . . . . . . . . 22
83	82	oveq2d 6321	. . . . . . . . . . . . . . . . . . . . 21
84		oveq1 6312	. . . . . . . . . . . . . . . . . . . . . 22
85	84	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . 21
86	83, 85	oveq12d 6323	. . . . . . . . . . . . . . . . . . . 20
87	81, 86	ifbieq2d 3940	. . . . . . . . . . . . . . . . . . 19
88	87	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$
89		c0ex 9636	. . . . . . . . . . . . . . . . . . . 20
90		ovex 6333	. . . . . . . . . . . . . . . . . . . 20
91	89, 90	ifex 3983	. . . . . . . . . . . . . . . . . . 19
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18
93	80, 88, 10, 92	fvmptd 5970	. . . . . . . . . . . . . . . . 17
94	93	adantr 466	. . . . . . . . . . . . . . . 16 $/\$
95		simpr 462	. . . . . . . . . . . . . . . . . 18 $/\$
96		simpl 458	. . . . . . . . . . . . . . . . . . 19 $/\$
97		2nn 10767	. . . . . . . . . . . . . . . . . . 19
98		nndivdvds 14289	. . . . . . . . . . . . . . . . . . 19 $/\$
99	96, 97, 98	sylancl 666	. . . . . . . . . . . . . . . . . 18 $/\$
100	95, 99	mpbird 235	. . . . . . . . . . . . . . . . 17 $/\$
101	100	iftrued 3923	. . . . . . . . . . . . . . . 16 $/\$
102	94, 101	eqtrd 2470	. . . . . . . . . . . . . . 15 $/\$
103	102	3adant1 1023	. . . . . . . . . . . . . 14 $/\$ $/\$
104		fouriersw.f	. . . . . . . . . . . . . . . . . 18
105		1re 9641	. . . . . . . . . . . . . . . . . . . 20
106	105	renegcli 9934	. . . . . . . . . . . . . . . . . . . 20
107	105, 106	keepel 3982	. . . . . . . . . . . . . . . . . . 19
108	107	a1i 11	. . . . . . . . . . . . . . . . . 18
109	104, 108	fmpti 6060	. . . . . . . . . . . . . . . . 17
110		fouriersw.t	. . . . . . . . . . . . . . . . 17
111		oveq1 6312	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	breq1d 4436	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	ifbid 3937	. . . . . . . . . . . . . . . . . . . . . 22
114	113	cbvmptv 4518	. . . . . . . . . . . . . . . . . . . . 21
115	104, 114	eqtri 2458	. . . . . . . . . . . . . . . . . . . 20
116	115	a1i 11	. . . . . . . . . . . . . . . . . . 19
117		oveq1 6312	. . . . . . . . . . . . . . . . . . . . . . . 24
118		pire 23278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	28, 118	remulcli 9656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	110, 119	eqeltri 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	120	recni 9654	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	121	mulid2i 9645	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
123	122	eqcomi 2442	. . . . . . . . . . . . . . . . . . . . . . . . . 26
124	123	oveq2i 6316	. . . . . . . . . . . . . . . . . . . . . . . . 25
125	124	oveq1i 6315	. . . . . . . . . . . . . . . . . . . . . . . 24
126	117, 125	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . . . 23
127	126	adantl 467	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
128		simpl 458	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
129		2pos 10701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
130	28, 118, 129, 68	mulgt0ii 9767	. . . . . . . . . . . . . . . . . . . . . . . . . 26
131	110	eqcomi 2442	. . . . . . . . . . . . . . . . . . . . . . . . . 26
132	130, 131	breqtri 4449	. . . . . . . . . . . . . . . . . . . . . . . . 25
133	120, 132	elrpii 11305	. . . . . . . . . . . . . . . . . . . . . . . 24
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
135		1zzd 10968	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136		modcyc 12129	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
137	128, 134, 135, 136	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
138	127, 137	eqtrd 2470	. . . . . . . . . . . . . . . . . . . . 21 $/\$
139	138	breq1d 4436	. . . . . . . . . . . . . . . . . . . 20 $/\$
140	139	ifbid 3937	. . . . . . . . . . . . . . . . . . 19 $/\$
141		id 23	. . . . . . . . . . . . . . . . . . . 20
142	120	a1i 11	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	readdcld 9669	. . . . . . . . . . . . . . . . . . 19
144	116, 140, 143, 108	fvmptd 5970	. . . . . . . . . . . . . . . . . 18
145	104	fvmpt2 5973	. . . . . . . . . . . . . . . . . . 19 $/\$
146	107, 145	mpan2 675	. . . . . . . . . . . . . . . . . 18
147	144, 146	eqtr4d 2473	. . . . . . . . . . . . . . . . 17
148		eqid 2429	. . . . . . . . . . . . . . . . 17
149		snfi 7657	. . . . . . . . . . . . . . . . . 18
150		eldifi 3593	. . . . . . . . . . . . . . . . . . . . . 22 $\$
151		0xr 9686	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
152	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
153	118	rexri 9692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
154	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155		elioore 11666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
156	155	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
157		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
158	118	renegcli 9934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159	158	rexri 9692	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
160		iooltub 37194	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
161	159, 153, 160	mp3an12 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
162	161	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
163	152, 154, 156, 157, 162	eliood 37179	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
164		negpilt0 37098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
165	158, 67, 164	ltleii 9756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
166		iooss1 11671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
167	159, 165, 166	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168	167	sseli 3466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
169	104	reseq1i 5121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
170		ioossre 11696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
171		resmpt 5174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
172	170, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
173		elioore 11666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
174	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
175		0red 9643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
176		ioogtlb 37176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
177	151, 153, 176	mp3an12 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
178	175, 173, 177	ltled 9782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
179	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
180	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
181	168, 161	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
182		pirp 23281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
183		2timesgt 37109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
184	182, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
185	184, 131	breqtri 4449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
187	173, 179, 180, 181, 186	lttrd 9795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
188		modid 12118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
189	173, 174, 178, 187, 188	syl22anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
190	189, 181	eqbrtrd 4446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191	190	iftrued 3923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192	191	mpteq2ia 4508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193	169, 172, 192	3eqtrri 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
194	193	oveq2i 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
195		reelprrecn 9630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
196	195	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
197		iooretop 21697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
198		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ℂ_fld
199	198	tgioo2 21732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
200	197, 199	eleqtri 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ℂ_fld ↾_t
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
202		1cnd 9658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
203	196, 201, 202	dvmptconst 37356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
204	203	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
205		ssid 3489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
206		ax-resscn 9595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
207		fss 5754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
208	109, 206, 207	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
209		dvresioo 37364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
210	205, 208, 209	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	194, 204, 210	3eqtr3i 2466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212	211	dmeqi 5056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
213		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
214	89, 213	dmmpti 5725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
215	212, 214	eqtr3i 2460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
216		ssdmres 5146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
217	215, 216	mpbir 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
218	217	sseli 3466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
219	168, 218	elind 3656	. . . . . . . . . . . . . . . . . . . . . . . . . 26
220		dmres 5145	. . . . . . . . . . . . . . . . . . . . . . . . . 26
221	219, 220	syl6eleqr 2528	. . . . . . . . . . . . . . . . . . . . . . . . 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 37176	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
228	159, 153, 227	mp3an12 1350	. . . . . . . . . . . . . . . . . . . . . . . . . 26
229	228	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
230		0red 9643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
231		neqne 37013	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
232	231	ad2antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
233		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
234	226, 230, 232, 233	lttri5d 37125	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
235	224, 225, 226, 229, 234	eliood 37179	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
236	67, 118, 68	ltleii 9756	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
237		iooss2 11672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
238	153, 236, 237	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
239	238	sseli 3466	. . . . . . . . . . . . . . . . . . . . . . . . . 26
240	104	reseq1i 5121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
241		ioossre 11696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
242		resmpt 5174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
243	241, 242	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
244	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
245		elioore 11666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
247	245, 246	modcld 12099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
248	245, 143	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
249	52	2timesi 10730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
250	110, 249	eqtri 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
251	250	oveq2i 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
252		negpicn 23282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
253	252, 52, 52	addassi 9650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
254	253	eqcomi 2442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
255	52	negidi 9942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
256	52, 252, 255	addcomli 9824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
257	256	oveq1i 6315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
258	52	addid2i 9820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
259	257, 258	eqtri 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
260	251, 254, 259	3eqtrri 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
266	261, 265	eqbrtrd 4446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
267	244, 248, 266	ltled 9782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
268		0red 9643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
269	158, 120	readdcli 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
271	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
272	271, 260	syl6breq 4465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
273	268, 270, 248, 272, 265	lttrd 9795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
274	268, 248, 273	ltled 9782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
275	245	recnd 9668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
276	121	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
277	275, 276	addcomd 9834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
278		iooltub 37194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$
279	159, 151, 278	mp3an12 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
280		ltaddneg 37116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
281	245, 120, 280	sylancl 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
282	279, 281	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
283	277, 282	eqbrtrd 4446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
284	274, 283	jca 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
285		modid2 12121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
291	141, 289, 290, 136	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
292	288, 291	eqtrd 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
293	245, 292	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
294	287, 293	eqtr3d 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
295	267, 294	breqtrd 4450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
296	244, 247, 295	lensymd 9785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
297	296	iffalsed 3926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
298	297	mpteq2ia 4508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
299	240, 243, 298	3eqtrri 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
300	299	oveq2i 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
301		iooretop 21697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
302	301, 199	eleqtri 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
303	302	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ℂ_fld ↾_t
304	202	negcld 9972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
305	196, 303, 304	dvmptconst 37356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
306	305	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
307		dvresioo 37364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
308	205, 208, 307	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
309	300, 306, 308	3eqtr3i 2466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
310	309	dmeqi 5056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
311		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
312	89, 311	dmmpti 5725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
313	310, 312	eqtr3i 2460	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314		ssdmres 5146	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
315	313, 314	mpbir 212	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
316	315	sseli 3466	. . . . . . . . . . . . . . . . . . . . . . . . . 26
317	239, 316	elind 3656	. . . . . . . . . . . . . . . . . . . . . . . . 25
318	317, 220	syl6eleqr 2528	. . . . . . . . . . . . . . . . . . . . . . . 24
319	235, 318	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
320	223, 319	pm2.61dan 798	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
321	150, 320	sylan 473	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
322		eldifn 3594	. . . . . . . . . . . . . . . . . . . . . 22 $\$
323	322	adantr 466	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
324	321, 323	condan 801	. . . . . . . . . . . . . . . . . . . 20 $\$
325		elsn 4016	. . . . . . . . . . . . . . . . . . . 20
326	324, 325	sylibr 215	. . . . . . . . . . . . . . . . . . 19 $\$
327	326	ssriv 3474	. . . . . . . . . . . . . . . . . 18 $\$
328		ssfi 7798	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$
329	149, 327, 328	mp2an 676	. . . . . . . . . . . . . . . . 17 $\$
330		inss1 3688	. . . . . . . . . . . . . . . . . . . . . 22
331	220, 330	eqsstri 3500	. . . . . . . . . . . . . . . . . . . . 21
332		ioosscn 37175	. . . . . . . . . . . . . . . . . . . . 21
333	331, 332	sstri 3479	. . . . . . . . . . . . . . . . . . . 20
334	333	a1i 11	. . . . . . . . . . . . . . . . . . 19
335		dvf 22739	. . . . . . . . . . . . . . . . . . . . . 22
336		fresin 5769	. . . . . . . . . . . . . . . . . . . . . 22
337		ffdm 5760	. . . . . . . . . . . . . . . . . . . . . 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 11696	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
344	331	sseli 3466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
345	343, 344	sseldi 3468	. . . . . . . . . . . . . . . . . . . . . . . . . 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 37179	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
351		elun1 3639	. . . . . . . . . . . . . . . . . . . . . . . 24
352	350, 351	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
353		simpl 458	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
354		0red 9643	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
355	345	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
356		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
357	354, 355, 356	nltled 9784	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
358		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
359	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
360		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
361	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
362		0red 9643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
363		mnfxr 11414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
364	363	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
365	362	mnfltd 11426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
366	360, 364, 362, 365	lptioo2 37282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
367		incom 3661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
368		ioossre 11696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
369		df-ss 3456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
370	368, 369	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
371	367, 370	eqtr2i 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
372	371	fveq2i 5884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
373	366, 372	syl6eleq 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
374		pnfxr 11412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
376	362	ltpnfd 11423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
377	360, 362, 375, 376	lptioo1 37283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
378		incom 3661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
379		ioossre 11696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
380		df-ss 3456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
381	379, 380	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
382	378, 381	eqtr2i 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
383	382	fveq2i 5884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384	377, 383	syl6eleq 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
385		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
386		mnfle 11435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
387	159, 386	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
388		iooss1 11671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
389	363, 387, 388	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
390	389	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
391		ioosscn 37175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
392	390, 391	syl6ss 3482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
393		0cnd 9635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
394	385, 392, 304, 393	constlimc 37275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
395		resabs1 5153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
396	389, 395	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
397	299, 396	eqtr4i 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
398	397	oveq1i 6315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
399		fssres 5766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
400	208, 368, 399	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
401	400	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
402	391	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
403		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
404		0le0 10699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
405		elioc2 11697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
406	159, 67, 405	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
407	67, 164, 404, 406	mpbir3an 1187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
408	198	cnfldtop 21715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld
409		ovex 6333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
410		resttop 20107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
411	408, 409, 410	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
412	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
413		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
414	387	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
415	364, 412, 362, 360, 413, 414, 362	iocopn 37205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
416	415	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
417	199	oveq1i 6315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
418		iocssre 11714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
419	363, 67, 418	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
420	195	elexi 3097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
421		restabs 20112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
422	408, 419, 420, 421	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
423	417, 422	eqtri 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
424	416, 423	eleqtri 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
425		isopn3i 20029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
426	411, 424, 425	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
427		mnflt0 11427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
428		snunioo2 37190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
429	363, 151, 427, 428	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
430	429	eqcomi 2442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
431	430	oveq2i 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
432	431	fveq2i 5884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
433		snunioo2 37190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
434	159, 151, 164, 433	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
435	434	eqcomi 2442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
436	432, 435	fveq12i 5886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
437	426, 436	eqtr3i 2460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
438	407, 437	eleqtri 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
439	438	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
440	401, 390, 402, 198, 403, 439	limcres 22718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
441	440	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
442	398, 441	eqtri 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
443	394, 442	syl6eleq 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
444		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
445		ioosscn 37175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
446	445	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
447	444, 446, 202, 393	constlimc 37275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
448		ltpnf 11422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
449		xrltle 11448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
450	153, 374, 449	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
451	118, 448, 450	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
452		iooss2 11672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
453	374, 451, 452	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
454		resabs1 5153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
455	453, 454	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
456	193, 455	eqtr4i 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
457	456	oveq1i 6315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
458		fssres 5766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
459	208, 379, 458	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
460	459	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
461	453	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
462		ioosscn 37175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
463	462	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
464		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
465		elico2 11698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
466	67, 153, 465	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
467	67, 404, 68, 466	mpbir3an 1187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
468		ovex 6333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
469		resttop 20107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
470	408, 468, 469	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
471	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
472		eqid 2429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
473	451	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
474	362, 471, 375, 360, 472, 473	icoopn 37210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
475	474	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
476	199	oveq1i 6315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
477		rge0ssre 11738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
478		restabs 20112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
479	408, 477, 420, 478	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
480	476, 479	eqtri 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
481	475, 480	eleqtri 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
482		isopn3i 20029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
483	470, 481, 482	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
484		0ltpnf 11424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
485		snunioo1 37197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
486	151, 374, 484, 485	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
487	486	eqcomi 2442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
488	487	oveq2i 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
489	488	fveq2i 5884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
490		snunioo1 37197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
491	151, 153, 68, 490	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
492	491	eqcomi 2442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
493	489, 492	fveq12i 5886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
494	483, 493	eqtr3i 2460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
495	467, 494	eleqtri 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
496	495	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
497	460, 461, 463, 198, 464, 496	limcres 22718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
498	497	trud 1446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
499	457, 498	eqtri 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
500	447, 499	syl6eleq 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
501		neg1lt0 10716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
502	106, 67, 105	lttri 9759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
503	501, 34, 502	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
504	106, 503	ltneii 9746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
505	504	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
506	198, 359, 360, 361, 362, 373, 384, 443, 500, 505	jumpncnp 37347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
512	220, 511	eqsstri 3500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
513	512	sseli 3466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
514	199, 198	dvcnp2 22751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2538	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
519	518	necon2ai 2666	. . . . . . . . . . . . . . . . . . . . . . . . . 26
520	519	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
521	354, 355, 357, 520	leneltd 9788	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
522	344, 163	sylan 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
523		elun2 3640	. . . . . . . . . . . . . . . . . . . . . . . . 25
524	522, 523	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
525	353, 521, 524	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
526	352, 525	pm2.61dan 798	. . . . . . . . . . . . . . . . . . . . . 22
527		ovex 6333	. . . . . . . . . . . . . . . . . . . . . . 23
528		ovex 6333	. . . . . . . . . . . . . . . . . . . . . . 23
529	527, 528	unipr 4235	. . . . . . . . . . . . . . . . . . . . . 22
530	526, 529	syl6eleqr 2528	. . . . . . . . . . . . . . . . . . . . 21
531	530	ssriv 3474	. . . . . . . . . . . . . . . . . . . 20
532	531	a1i 11	. . . . . . . . . . . . . . . . . . 19
533		ineq2 3664	. . . . . . . . . . . . . . . . . . . . . . 23
534		retop 21693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
535		ovex 6333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
536	535	resex 5168	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
537	536	dmex 6740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
538	534, 537	pm3.2i 456	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
539	318	ssriv 3474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
540		ssid 3489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
541	301, 539, 540	3pm3.2i 1183	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
542		restopnb 20122	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
543	538, 541, 542	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
544	301, 543	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
545		inss2 3689	. . . . . . . . . . . . . . . . . . . . . . . . 25
546	539, 540	ssini 3691	. . . . . . . . . . . . . . . . . . . . . . . . 25
547	545, 546	eqssi 3486	. . . . . . . . . . . . . . . . . . . . . . . 24
548	199	oveq1i 6315	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t ℂ_fld ↾_t ↾_t
549	331, 343	sstri 3479	. . . . . . . . . . . . . . . . . . . . . . . . . 26
550		restabs 20112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
551	408, 549, 420, 550	mp3an 1360	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
552	548, 551	eqtr2i 2459	. . . . . . . . . . . . . . . . . . . . . . . 24 ℂ_fld ↾_t ↾_t
553	544, 547, 552	3eltr4i 2530	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
554	533, 553	syl6eqel 2525	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ↾_t
555	554	adantl 467	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ℂ_fld ↾_t
556		neqne 37013	. . . . . . . . . . . . . . . . . . . . . . 23
557		elprn1 37284	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
558	556, 557	sylan2 476	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
559		ineq2 3664	. . . . . . . . . . . . . . . . . . . . . . 23
560	221	ssriv 3474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
561		ssid 3489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
562	197, 560, 561	3pm3.2i 1183	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
563		restopnb 20122	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
564	538, 562, 563	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
565	197, 564	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
566		inss2 3689	. . . . . . . . . . . . . . . . . . . . . . . . 25
567	560, 561	ssini 3691	. . . . . . . . . . . . . . . . . . . . . . . . 25
568	566, 567	eqssi 3486	. . . . . . . . . . . . . . . . . . . . . . . 24
569	565, 568, 552	3eltr4i 2530	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
570	559, 569	syl6eqel 2525	. . . . . . . . . . . . . . . . . . . . . 22