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 31903

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 11126	. . . . . . 7
2		1zzd 10902	. . . . . . 7
3		eqidd 2444	. . . . . . . . 9
4		oveq2 6289	. . . . . . . . . . . . . 14
5	4	oveq1d 6296	. . . . . . . . . . . . 13
6	5	oveq1d 6296	. . . . . . . . . . . 12
7	6	fveq2d 5860	. . . . . . . . . . 11
8	7, 5	oveq12d 6299	. . . . . . . . . 10
9	8	adantl 466	. . . . . . . . 9 $/\$
10		id 22	. . . . . . . . 9
11		ovex 6309	. . . . . . . . . 10
12	11	a1i 11	. . . . . . . . 9
13	3, 9, 10, 12	fvmptd 5946	. . . . . . . 8
14	13	adantl 466	. . . . . . 7 $/\$
15		2z 10903	. . . . . . . . . . . . . . 15
16	15	a1i 11	. . . . . . . . . . . . . 14
17		nnz 10893	. . . . . . . . . . . . . 14
18	16, 17	zmulcld 10981	. . . . . . . . . . . . 13
19		1zzd 10902	. . . . . . . . . . . . 13
20	18, 19	zsubcld 10980	. . . . . . . . . . . 12
21	20	zcnd 10976	. . . . . . . . . . 11
22		fouriersw.x	. . . . . . . . . . . . 13
23	22	recni 9611	. . . . . . . . . . . 12
24	23	a1i 11	. . . . . . . . . . 11
25	21, 24	mulcld 9619	. . . . . . . . . 10
26	25	sincld 13846	. . . . . . . . 9
27		0red 9600	. . . . . . . . . 10
28		2re 10612	. . . . . . . . . . . . . 14
29	28	a1i 11	. . . . . . . . . . . . 13
30		1red 9614	. . . . . . . . . . . . 13
31	29, 30	remulcld 9627	. . . . . . . . . . . 12
32	31, 30	resubcld 9994	. . . . . . . . . . 11
33	20	zred 10975	. . . . . . . . . . 11
34		0lt1 10082	. . . . . . . . . . . . 13
35		2t1e2 10691	. . . . . . . . . . . . . . 15
36	35	oveq1i 6291	. . . . . . . . . . . . . 14
37		2m1e1 10657	. . . . . . . . . . . . . 14
38	36, 37	eqtr2i 2473	. . . . . . . . . . . . 13
39	34, 38	breqtri 4460	. . . . . . . . . . . 12
40	39	a1i 11	. . . . . . . . . . 11
41	18	zred 10975	. . . . . . . . . . . 12
42		nnre 10550	. . . . . . . . . . . . 13
43		0le2 10633	. . . . . . . . . . . . . 14
44	43	a1i 11	. . . . . . . . . . . . 13
45		nnge1 10569	. . . . . . . . . . . . 13
46	30, 42, 29, 44, 45	lemul2ad 10493	. . . . . . . . . . . 12
47	31, 41, 30, 46	lesub1dd 10175	. . . . . . . . . . 11
48	27, 32, 33, 40, 47	ltletrd 9745	. . . . . . . . . 10
49	27, 48	gtned 9723	. . . . . . . . 9
50	26, 21, 49	divcld 10327	. . . . . . . 8
51	50	adantl 466	. . . . . . 7 $/\$
52		picn 22828	. . . . . . . . . . 11
53	52	a1i 11	. . . . . . . . . 10
54		4cn 10620	. . . . . . . . . . 11
55	54	a1i 11	. . . . . . . . . 10
56		4ne0 10639	. . . . . . . . . . 11
57	56	a1i 11	. . . . . . . . . 10
58	53, 55, 57	divcld 10327	. . . . . . . . 9
59		eqid 2443	. . . . . . . . . . . . . . . 16
60		0cnd 9592	. . . . . . . . . . . . . . . . 17
61	54	a1i 11	. . . . . . . . . . . . . . . . . . 19
62		nncn 10551	. . . . . . . . . . . . . . . . . . . 20
63		mulcl 9579	. . . . . . . . . . . . . . . . . . . 20 $/\$
64	62, 52, 63	sylancl 662	. . . . . . . . . . . . . . . . . . 19
65	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20
66		nnne0 10575	. . . . . . . . . . . . . . . . . . . 20
67		0re 9599	. . . . . . . . . . . . . . . . . . . . . 22
68		pipos 22829	. . . . . . . . . . . . . . . . . . . . . 22
69	67, 68	gtneii 9699	. . . . . . . . . . . . . . . . . . . . 21
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . 20
71	62, 65, 66, 70	mulne0d 10208	. . . . . . . . . . . . . . . . . . 19
72	61, 64, 71	divcld 10327	. . . . . . . . . . . . . . . . . 18
73	23	a1i 11	. . . . . . . . . . . . . . . . . . . 20
74	62, 73	mulcld 9619	. . . . . . . . . . . . . . . . . . 19
75	74	sincld 13846	. . . . . . . . . . . . . . . . . 18
76	72, 75	mulcld 9619	. . . . . . . . . . . . . . . . 17
77	60, 76	ifcld 3969	. . . . . . . . . . . . . . . 16
78	59, 77	fmpti 6039	. . . . . . . . . . . . . . 15
79	78	a1i 11	. . . . . . . . . . . . . 14
80		eqidd 2444	. . . . . . . . . . . . . . . . . 18
81		breq2 4441	. . . . . . . . . . . . . . . . . . . 20
82		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . 22
83	82	oveq2d 6297	. . . . . . . . . . . . . . . . . . . . 21
84		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . 22
85	84	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . 21
86	83, 85	oveq12d 6299	. . . . . . . . . . . . . . . . . . . 20
87	81, 86	ifbieq2d 3951	. . . . . . . . . . . . . . . . . . 19
88	87	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$
89		c0ex 9593	. . . . . . . . . . . . . . . . . . . 20
90		ovex 6309	. . . . . . . . . . . . . . . . . . . 20
91	89, 90	ifex 3995	. . . . . . . . . . . . . . . . . . 19
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18
93	80, 88, 10, 92	fvmptd 5946	. . . . . . . . . . . . . . . . 17
94	93	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
95		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$
96		simpl 457	. . . . . . . . . . . . . . . . . . 19 $/\$
97		2nn 10700	. . . . . . . . . . . . . . . . . . 19
98		nndivdvds 13973	. . . . . . . . . . . . . . . . . . 19 $/\$
99	96, 97, 98	sylancl 662	. . . . . . . . . . . . . . . . . 18 $/\$
100	95, 99	mpbird 232	. . . . . . . . . . . . . . . . 17 $/\$
101	100	iftrued 3934	. . . . . . . . . . . . . . . 16 $/\$
102	94, 101	eqtrd 2484	. . . . . . . . . . . . . . 15 $/\$
103	102	3adant1 1015	. . . . . . . . . . . . . 14 $/\$ $/\$
104		fouriersw.f	. . . . . . . . . . . . . . . . . 18
105		1re 9598	. . . . . . . . . . . . . . . . . . . 20
106	105	renegcli 9885	. . . . . . . . . . . . . . . . . . . 20
107	105, 106	keepel 3994	. . . . . . . . . . . . . . . . . . 19
108	107	a1i 11	. . . . . . . . . . . . . . . . . 18
109	104, 108	fmpti 6039	. . . . . . . . . . . . . . . . 17
110		fouriersw.t	. . . . . . . . . . . . . . . . 17
111		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	breq1d 4447	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	ifbid 3948	. . . . . . . . . . . . . . . . . . . . . 22
114	113	cbvmptv 4528	. . . . . . . . . . . . . . . . . . . . 21
115	104, 114	eqtri 2472	. . . . . . . . . . . . . . . . . . . 20
116	115	a1i 11	. . . . . . . . . . . . . . . . . . 19
117		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . . . 24
118		pire 22827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	28, 118	remulcli 9613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	110, 119	eqeltri 2527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	120	recni 9611	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	121	mulid2i 9602	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
123	122	eqcomi 2456	. . . . . . . . . . . . . . . . . . . . . . . . . 26
124	123	oveq2i 6292	. . . . . . . . . . . . . . . . . . . . . . . . 25
125	124	oveq1i 6291	. . . . . . . . . . . . . . . . . . . . . . . 24
126	117, 125	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . 23
127	126	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
128		simpl 457	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
129		2pos 10634	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
130	28, 118, 129, 68	mulgt0ii 9721	. . . . . . . . . . . . . . . . . . . . . . . . . 26
131	110	eqcomi 2456	. . . . . . . . . . . . . . . . . . . . . . . . . 26
132	130, 131	breqtri 4460	. . . . . . . . . . . . . . . . . . . . . . . . 25
133	120, 132	elrpii 11233	. . . . . . . . . . . . . . . . . . . . . . . 24
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
135		1zzd 10902	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136		modcyc 12012	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
137	128, 134, 135, 136	syl3anc 1229	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
138	127, 137	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . 21 $/\$
139	138	breq1d 4447	. . . . . . . . . . . . . . . . . . . 20 $/\$
140	139	ifbid 3948	. . . . . . . . . . . . . . . . . . 19 $/\$
141		id 22	. . . . . . . . . . . . . . . . . . . 20
142	120	a1i 11	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	readdcld 9626	. . . . . . . . . . . . . . . . . . 19
144	116, 140, 143, 108	fvmptd 5946	. . . . . . . . . . . . . . . . . 18
145	104	fvmpt2 5948	. . . . . . . . . . . . . . . . . . 19 $/\$
146	107, 145	mpan2 671	. . . . . . . . . . . . . . . . . 18
147	144, 146	eqtr4d 2487	. . . . . . . . . . . . . . . . 17
148		eqid 2443	. . . . . . . . . . . . . . . . 17
149		snfi 7598	. . . . . . . . . . . . . . . . . 18
150		eldifi 3611	. . . . . . . . . . . . . . . . . . . . . 22 $\$
151		0xr 9643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
152	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
153	118	rexri 9649	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
154	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155		elioore 11569	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
156	155	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
157		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
158	118	renegcli 9885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159	158	rexri 9649	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
160		iooltub 31484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
161	159, 153, 160	mp3an12 1315	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
162	161	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
163	152, 154, 156, 157, 162	eliood 31467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
164		negpilt0 31411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
165	158, 67, 164	ltleii 9710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
166		iooss1 11574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
167	159, 165, 166	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168	167	sseli 3485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
169	104	reseq1i 5259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
170		ioossre 11596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
171		resmpt 5313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
172	170, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
173		elioore 11569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
174	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
175		0red 9600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
176		ioogtlb 31464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
177	151, 153, 176	mp3an12 1315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
178	175, 173, 177	ltled 9736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
179	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
180	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
181	168, 161	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
182		pirp 22830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
183		2timesgt 31424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
184	182, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
185	184, 131	breqtri 4460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
187	173, 179, 180, 181, 186	lttrd 9746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
188		modid 12001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
189	173, 174, 178, 187, 188	syl22anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
190	189, 181	eqbrtrd 4457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191	190	iftrued 3934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192	191	mpteq2ia 4519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193	169, 172, 192	3eqtrri 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
194	193	oveq2i 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
195		reelprrecn 9587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
196	195	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
197		iooretop 21250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
198		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ℂ_fld
199	198	tgioo2 21285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
200	197, 199	eleqtri 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ℂ_fld ↾_t
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
202		1cnd 9615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
203	196, 201, 202	dvmptconst 31614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
204	203	trud 1392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
205		ssid 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
206		ax-resscn 9552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
207		fss 5729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
208	109, 206, 207	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
209		dvresioo 31622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
210	205, 208, 209	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	194, 204, 210	3eqtr3i 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212	211	dmeqi 5194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
213		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
214	89, 213	dmmpti 5700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
215	212, 214	eqtr3i 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
216		ssdmres 5285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
217	215, 216	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
218	217	sseli 3485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
219	168, 218	elind 3673	. . . . . . . . . . . . . . . . . . . . . . . . . 26
220		dmres 5284	. . . . . . . . . . . . . . . . . . . . . . . . . 26
221	219, 220	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . . . . . . . 25
222	163, 221	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
223	222	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
224	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
225	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
226	155	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
227		ioogtlb 31464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
228	159, 153, 227	mp3an12 1315	. . . . . . . . . . . . . . . . . . . . . . . . . 26
229	228	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
230		0red 9600	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
231		neqne 31388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
232	231	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
233		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
234	226, 230, 232, 233	lttri5d 31448	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
235	224, 225, 226, 229, 234	eliood 31467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
236	67, 118, 68	ltleii 9710	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
237		iooss2 11575	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
238	153, 236, 237	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
239	238	sseli 3485	. . . . . . . . . . . . . . . . . . . . . . . . . 26
240	104	reseq1i 5259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
241		ioossre 11596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
242		resmpt 5313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
243	241, 242	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
244	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
245		elioore 11569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
247	245, 246	modcld 11983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
248	245, 143	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
249	52	2timesi 10663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
250	110, 249	eqtri 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
251	250	oveq2i 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
252		negpicn 22831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
253	252, 52, 52	addassi 9607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
254	253	eqcomi 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
255	52	negidi 9893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
256	52, 252, 255	addcomli 9775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
257	256	oveq1i 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
258	52	addid2i 9771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
259	257, 258	eqtri 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
260	251, 254, 259	3eqtrri 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
266	261, 265	eqbrtrd 4457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
267	244, 248, 266	ltled 9736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
268		0red 9600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
269	158, 120	readdcli 9612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
271	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
272	271, 260	syl6breq 4476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
273	268, 270, 248, 272, 265	lttrd 9746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
274	268, 248, 273	ltled 9736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
275	245	recnd 9625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
276	121	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
277	275, 276	addcomd 9785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
278		iooltub 31484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$
279	159, 151, 278	mp3an12 1315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
280		ltaddneg 31433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
281	245, 120, 280	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
282	279, 281	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
283	277, 282	eqbrtrd 4457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
284	274, 283	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
285		modid2 12004	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
286	248, 133, 285	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
287	284, 286	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
288	125	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
289	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
290		1zzd 10902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
291	141, 289, 290, 136	syl3anc 1229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
292	288, 291	eqtrd 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
293	245, 292	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
294	287, 293	eqtr3d 2486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
295	267, 294	breqtrd 4461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
296	244, 247, 295	leimnltd 31421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
297	296	iffalsed 3937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
298	297	mpteq2ia 4519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
299	240, 243, 298	3eqtrri 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
300	299	oveq2i 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
301		iooretop 21250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
302	301, 199	eleqtri 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
303	302	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ℂ_fld ↾_t
304	202	negcld 9923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
305	196, 303, 304	dvmptconst 31614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
306	305	trud 1392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
307		dvresioo 31622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
308	205, 208, 307	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
309	300, 306, 308	3eqtr3i 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
310	309	dmeqi 5194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
311		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
312	89, 311	dmmpti 5700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
313	310, 312	eqtr3i 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314		ssdmres 5285	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
315	313, 314	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
316	315	sseli 3485	. . . . . . . . . . . . . . . . . . . . . . . . . 26
317	239, 316	elind 3673	. . . . . . . . . . . . . . . . . . . . . . . . 25
318	317, 220	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . . . . . . 24
319	235, 318	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
320	223, 319	pm2.61dan 791	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
321	150, 320	sylan 471	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
322		eldifn 3612	. . . . . . . . . . . . . . . . . . . . . 22 $\$
323	322	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
324	321, 323	condan 794	. . . . . . . . . . . . . . . . . . . 20 $\$
325		elsn 4028	. . . . . . . . . . . . . . . . . . . 20
326	324, 325	sylibr 212	. . . . . . . . . . . . . . . . . . 19 $\$
327	326	ssriv 3493	. . . . . . . . . . . . . . . . . 18 $\$
328		ssfi 7742	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$
329	149, 327, 328	mp2an 672	. . . . . . . . . . . . . . . . 17 $\$
330		inss1 3703	. . . . . . . . . . . . . . . . . . . . . 22
331	220, 330	eqsstri 3519	. . . . . . . . . . . . . . . . . . . . 21
332		ioosscn 31463	. . . . . . . . . . . . . . . . . . . . 21
333	331, 332	sstri 3498	. . . . . . . . . . . . . . . . . . . 20
334	333	a1i 11	. . . . . . . . . . . . . . . . . . 19
335		dvf 22288	. . . . . . . . . . . . . . . . . . . . . 22
336		fresin 5744	. . . . . . . . . . . . . . . . . . . . . 22
337		ffdm 5735	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
338	335, 336, 337	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 $/\$
339	338	simpli 458	. . . . . . . . . . . . . . . . . . . 20
340	339	a1i 11	. . . . . . . . . . . . . . . . . . 19
341	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
342	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
343		ioossre 11596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
344	331	sseli 3485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
345	343, 344	sseldi 3487	. . . . . . . . . . . . . . . . . . . . . . . . . 26
346	345	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
347	344, 228	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26
348	347	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
349		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
350	341, 342, 346, 348, 349	eliood 31467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
351		elun1 3656	. . . . . . . . . . . . . . . . . . . . . . . 24
352	350, 351	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
353		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
354		0red 9600	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
355	345	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
356		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
357	354, 355, 356	nltled 31426	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
358		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
359	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
360		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
361	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
362		0red 9600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
363		mnfxr 11333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
364	363	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
365	362	mnfltd 31440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
366	360, 364, 362, 365	lptioo2 31545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
367		incom 3676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
368		ioossre 11596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
369		df-ss 3475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
370	368, 369	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
371	367, 370	eqtr2i 2473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
372	371	fveq2i 5859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
373	366, 372	syl6eleq 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
374		pnfxr 11331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
376	362	ltpnfd 31429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
377	360, 362, 375, 376	lptioo1 31546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
378		incom 3676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
379		ioossre 11596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
380		df-ss 3475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
381	379, 380	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
382	378, 381	eqtr2i 2473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
383	382	fveq2i 5859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384	377, 383	syl6eleq 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
385		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
386		mnfle 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
387	159, 386	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
388		iooss1 11574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
389	363, 387, 388	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
390	389	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
391		ioosscn 31463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
392	390, 391	syl6ss 3501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
393		0cnd 9592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
394	385, 392, 304, 393	constlimc 31538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
395		resabs1 5292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
396	389, 395	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
397	299, 396	eqtr4i 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
398	397	oveq1i 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
399		fssres 5741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
400	208, 368, 399	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
401	400	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
402	391	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
403		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
404		0le0 10632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
405		elioc2 11597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
406	159, 67, 405	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
407	67, 164, 404, 406	mpbir3an 1179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
408	198	cnfldtop 21268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld
409		ovex 6309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
410		resttop 19638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
411	408, 409, 410	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
412	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
413		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
414	387	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
415	364, 412, 362, 360, 413, 414, 362	iocopn 31496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
416	415	trud 1392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
417	199	oveq1i 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
418		iocssre 11614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
419	363, 67, 418	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
420	195	elexi 3105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
421		restabs 19643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
422	408, 419, 420, 421	mp3an 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
423	417, 422	eqtri 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
424	416, 423	eleqtri 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
425		isopn3i 19560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
426	411, 424, 425	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
427		mnflt0 11344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
428		snunioo2 31480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
429	363, 151, 427, 428	mp3an 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
430	429	eqcomi 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
431	430	oveq2i 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
432	431	fveq2i 5859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
433		snunioo2 31480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
434	159, 151, 164, 433	mp3an 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
435	434	eqcomi 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
436	432, 435	fveq12i 5861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
437	426, 436	eqtr3i 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
438	407, 437	eleqtri 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
439	438	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
440	401, 390, 402, 198, 403, 439	limcres 22267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
441	440	trud 1392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
442	398, 441	eqtri 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
443	394, 442	syl6eleq 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
444		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
445		ioosscn 31463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
446	445	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
447	444, 446, 202, 393	constlimc 31538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
448		ltpnf 11341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
449		xrltle 11365	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
450	153, 374, 449	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
451	118, 448, 450	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
452		iooss2 11575	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
453	374, 451, 452	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
454		resabs1 5292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
455	453, 454	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
456	193, 455	eqtr4i 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
457	456	oveq1i 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
458		fssres 5741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
459	208, 379, 458	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
460	459	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
461	453	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
462		ioosscn 31463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
463	462	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
464		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
465		elico2 11598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
466	67, 153, 465	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
467	67, 404, 68, 466	mpbir3an 1179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
468		ovex 6309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
469		resttop 19638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
470	408, 468, 469	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
471	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
472		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
473	451	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
474	362, 471, 375, 360, 472, 473	icoopn 31501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
475	474	trud 1392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
476	199	oveq1i 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
477		rge0ssre 11638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
478		restabs 19643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
479	408, 477, 420, 478	mp3an 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
480	476, 479	eqtri 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
481	475, 480	eleqtri 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
482		isopn3i 19560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
483	470, 481, 482	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
484		0ltpnf 11342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
485		snunioo1 31488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
486	151, 374, 484, 485	mp3an 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
487	486	eqcomi 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
488	487	oveq2i 6292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
489	488	fveq2i 5859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
490		snunioo1 31488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
491	151, 153, 68, 490	mp3an 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
492	491	eqcomi 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
493	489, 492	fveq12i 5861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
494	483, 493	eqtr3i 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
495	467, 494	eleqtri 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
496	495	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
497	460, 461, 463, 198, 464, 496	limcres 22267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
498	497	trud 1392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
499	457, 498	eqtri 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
500	447, 499	syl6eleq 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
501		neg1lt0 10649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
502	106, 67, 105	lttri 9713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
503	501, 34, 502	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
504	106, 503	ltneii 9700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
505	504	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
506	198, 359, 360, 361, 362, 373, 384, 443, 500, 505	jumpncnp 31608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
507	506	trud 1392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
508	206	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
509	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
510	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
511		inss2 3704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
512	220, 511	eqsstri 3519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
513	512	sseli 3485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
514	199, 198	dvcnp2 22300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ ℂ_fld
515	508, 509, 510, 513, 514	syl31anc 1232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
516	507, 515	mto 176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
517	516	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
518	358, 517	eqneltrd 2552	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
519	518	necon2ai 2678	. . . . . . . . . . . . . . . . . . . . . . . . . 26
520	519	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
521	354, 355, 357, 520	leneltd 31443	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
522	344, 163	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
523		elun2 3657	. . . . . . . . . . . . . . . . . . . . . . . . 25
524	522, 523	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
525	353, 521, 524	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
526	352, 525	pm2.61dan 791	. . . . . . . . . . . . . . . . . . . . . 22
527		ovex 6309	. . . . . . . . . . . . . . . . . . . . . . 23
528		ovex 6309	. . . . . . . . . . . . . . . . . . . . . . 23
529	527, 528	unipr 4247	. . . . . . . . . . . . . . . . . . . . . 22
530	526, 529	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . . . 21
531	530	ssriv 3493	. . . . . . . . . . . . . . . . . . . 20
532	531	a1i 11	. . . . . . . . . . . . . . . . . . 19
533		ineq2 3679	. . . . . . . . . . . . . . . . . . . . . . 23
534		retop 21245	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
535		ovex 6309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
536	535	resex 5307	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
537	536	dmex 6718	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
538	534, 537	pm3.2i 455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
539	318	ssriv 3493	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
540		ssid 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
541	301, 539, 540	3pm3.2i 1175	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
542		restopnb 19653	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
543	538, 541, 542	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
544	301, 543	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
545		inss2 3704	. . . . . . . . . . . . . . . . . . . . . . . . 25
546	539, 540	ssini 3706	. . . . . . . . . . . . . . . . . . . . . . . . 25
547	545, 546	eqssi 3505	. . . . . . . . . . . . . . . . . . . . . . . 24
548	199	oveq1i 6291	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t ℂ_fld ↾_t ↾_t
549	331, 343	sstri 3498	. . . . . . . . . . . . . . . . . . . . . . . . . 26
550		restabs 19643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
551	408, 549, 420, 550	mp3an 1325	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
552	548, 551	eqtr2i 2473	. . . . . . . . . . . . . . . . . . . . . . . 24 ℂ_fld ↾_t ↾_t
553	544, 547, 552	3eltr4i 2544	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
554	533, 553	syl6eqel 2539	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ↾_t
555	554	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ℂ_fld ↾_t
556		neqne 31388	. . . . . . . . . . . . . . . . . . . . . . 23
557		elprn1 31547	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
558	556, 557	sylan2 474	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
559		ineq2 3679	. . . . . . . . . . . . . . . . . . . . . . 23
560	221	ssriv 3493	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
561		ssid 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
562	197, 560, 561	3pm3.2i 1175	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
563		restopnb 19653	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
564	538, 562, 563	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
565	197, 564	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
566		inss2 3704	. . . . . . . . . . . . . . . . . . . . . . . . 25
567	560, 561	ssini 3706	. . . . . . . . . . . . . . . . . . . . . . . . 25
568	566, 567	eqssi 3505	. . . . . . . . . . . . . . . . . . . . . . . 24
569	565, 568, 552	3eltr4i 2544	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
570	559, 569	syl6eqel 2539	. . . . . . . . . . . . . . . . . . . . . 22