fouriersw - Mathbox for Glauco Siliprandi

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

Theorem fouriersw 38132

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 11222	. . . . . . 7
2		1zzd 10996	. . . . . . 7
3		eqidd 2462	. . . . . . . . 9
4		oveq2 6322	. . . . . . . . . . . . . 14
5	4	oveq1d 6329	. . . . . . . . . . . . 13
6	5	oveq1d 6329	. . . . . . . . . . . 12
7	6	fveq2d 5891	. . . . . . . . . . 11
8	7, 5	oveq12d 6332	. . . . . . . . . 10
9	8	adantl 472	. . . . . . . . 9 $/\$
10		id 22	. . . . . . . . 9
11		ovex 6342	. . . . . . . . . 10
12	11	a1i 11	. . . . . . . . 9
13	3, 9, 10, 12	fvmptd 5976	. . . . . . . 8
14	13	adantl 472	. . . . . . 7 $/\$
15		2z 10997	. . . . . . . . . . . . . . 15
16	15	a1i 11	. . . . . . . . . . . . . 14
17		nnz 10987	. . . . . . . . . . . . . 14
18	16, 17	zmulcld 11074	. . . . . . . . . . . . 13
19		1zzd 10996	. . . . . . . . . . . . 13
20	18, 19	zsubcld 11073	. . . . . . . . . . . 12
21	20	zcnd 11069	. . . . . . . . . . 11
22		fouriersw.x	. . . . . . . . . . . . 13
23	22	recni 9680	. . . . . . . . . . . 12
24	23	a1i 11	. . . . . . . . . . 11
25	21, 24	mulcld 9688	. . . . . . . . . 10
26	25	sincld 14232	. . . . . . . . 9
27		0red 9669	. . . . . . . . . 10
28		2re 10706	. . . . . . . . . . . . . 14
29	28	a1i 11	. . . . . . . . . . . . 13
30		1red 9683	. . . . . . . . . . . . 13
31	29, 30	remulcld 9696	. . . . . . . . . . . 12
32	31, 30	resubcld 10074	. . . . . . . . . . 11
33	20	zred 11068	. . . . . . . . . . 11
34		0lt1 10163	. . . . . . . . . . . . 13
35		2t1e2 10786	. . . . . . . . . . . . . . 15
36	35	oveq1i 6324	. . . . . . . . . . . . . 14
37		2m1e1 10751	. . . . . . . . . . . . . 14
38	36, 37	eqtr2i 2484	. . . . . . . . . . . . 13
39	34, 38	breqtri 4439	. . . . . . . . . . . 12
40	39	a1i 11	. . . . . . . . . . 11
41	18	zred 11068	. . . . . . . . . . . 12
42		nnre 10643	. . . . . . . . . . . . 13
43		0le2 10727	. . . . . . . . . . . . . 14
44	43	a1i 11	. . . . . . . . . . . . 13
45		nnge1 10662	. . . . . . . . . . . . 13
46	30, 42, 29, 44, 45	lemul2ad 10574	. . . . . . . . . . . 12
47	31, 41, 30, 46	lesub1dd 10256	. . . . . . . . . . 11
48	27, 32, 33, 40, 47	ltletrd 9820	. . . . . . . . . 10
49	27, 48	gtned 9795	. . . . . . . . 9
50	26, 21, 49	divcld 10410	. . . . . . . 8
51	50	adantl 472	. . . . . . 7 $/\$
52		picn 23462	. . . . . . . . . . 11
53	52	a1i 11	. . . . . . . . . 10
54		4cn 10714	. . . . . . . . . . 11
55	54	a1i 11	. . . . . . . . . 10
56		4ne0 10733	. . . . . . . . . . 11
57	56	a1i 11	. . . . . . . . . 10
58	53, 55, 57	divcld 10410	. . . . . . . . 9
59		eqid 2461	. . . . . . . . . . . . . . . 16
60		0cnd 9661	. . . . . . . . . . . . . . . . 17
61	54	a1i 11	. . . . . . . . . . . . . . . . . . 19
62		nncn 10644	. . . . . . . . . . . . . . . . . . . 20
63		mulcl 9648	. . . . . . . . . . . . . . . . . . . 20 $/\$
64	62, 52, 63	sylancl 673	. . . . . . . . . . . . . . . . . . 19
65	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20
66		nnne0 10669	. . . . . . . . . . . . . . . . . . . 20
67		0re 9668	. . . . . . . . . . . . . . . . . . . . . 22
68		pipos 23463	. . . . . . . . . . . . . . . . . . . . . 22
69	67, 68	gtneii 9771	. . . . . . . . . . . . . . . . . . . . 21
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . 20
71	62, 65, 66, 70	mulne0d 10291	. . . . . . . . . . . . . . . . . . 19
72	61, 64, 71	divcld 10410	. . . . . . . . . . . . . . . . . 18
73	23	a1i 11	. . . . . . . . . . . . . . . . . . . 20
74	62, 73	mulcld 9688	. . . . . . . . . . . . . . . . . . 19
75	74	sincld 14232	. . . . . . . . . . . . . . . . . 18
76	72, 75	mulcld 9688	. . . . . . . . . . . . . . . . 17
77	60, 76	ifcld 3935	. . . . . . . . . . . . . . . 16
78	59, 77	fmpti 6067	. . . . . . . . . . . . . . 15
79	78	a1i 11	. . . . . . . . . . . . . 14
80		eqidd 2462	. . . . . . . . . . . . . . . . . 18
81		breq2 4419	. . . . . . . . . . . . . . . . . . . 20
82		oveq1 6321	. . . . . . . . . . . . . . . . . . . . . 22
83	82	oveq2d 6330	. . . . . . . . . . . . . . . . . . . . 21
84		oveq1 6321	. . . . . . . . . . . . . . . . . . . . . 22
85	84	fveq2d 5891	. . . . . . . . . . . . . . . . . . . . 21
86	83, 85	oveq12d 6332	. . . . . . . . . . . . . . . . . . . 20
87	81, 86	ifbieq2d 3917	. . . . . . . . . . . . . . . . . . 19
88	87	adantl 472	. . . . . . . . . . . . . . . . . 18 $/\$
89		c0ex 9662	. . . . . . . . . . . . . . . . . . . 20
90		ovex 6342	. . . . . . . . . . . . . . . . . . . 20
91	89, 90	ifex 3960	. . . . . . . . . . . . . . . . . . 19
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18
93	80, 88, 10, 92	fvmptd 5976	. . . . . . . . . . . . . . . . 17
94	93	adantr 471	. . . . . . . . . . . . . . . 16 $/\$
95		simpr 467	. . . . . . . . . . . . . . . . . 18 $/\$
96		simpl 463	. . . . . . . . . . . . . . . . . . 19 $/\$
97		2nn 10795	. . . . . . . . . . . . . . . . . . 19
98		nndivdvds 14359	. . . . . . . . . . . . . . . . . . 19 $/\$
99	96, 97, 98	sylancl 673	. . . . . . . . . . . . . . . . . 18 $/\$
100	95, 99	mpbird 240	. . . . . . . . . . . . . . . . 17 $/\$
101	100	iftrued 3900	. . . . . . . . . . . . . . . 16 $/\$
102	94, 101	eqtrd 2495	. . . . . . . . . . . . . . 15 $/\$
103	102	3adant1 1032	. . . . . . . . . . . . . 14 $/\$ $/\$
104		fouriersw.f	. . . . . . . . . . . . . . . . . 18
105		1re 9667	. . . . . . . . . . . . . . . . . . . 20
106	105	renegcli 9960	. . . . . . . . . . . . . . . . . . . 20
107	105, 106	keepel 3959	. . . . . . . . . . . . . . . . . . 19
108	107	a1i 11	. . . . . . . . . . . . . . . . . 18
109	104, 108	fmpti 6067	. . . . . . . . . . . . . . . . 17
110		fouriersw.t	. . . . . . . . . . . . . . . . 17
111		oveq1 6321	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	breq1d 4425	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	ifbid 3914	. . . . . . . . . . . . . . . . . . . . . 22
114	113	cbvmptv 4508	. . . . . . . . . . . . . . . . . . . . 21
115	104, 114	eqtri 2483	. . . . . . . . . . . . . . . . . . . 20
116	115	a1i 11	. . . . . . . . . . . . . . . . . . 19
117		oveq1 6321	. . . . . . . . . . . . . . . . . . . . . . . 24
118		pire 23461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	28, 118	remulcli 9682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	110, 119	eqeltri 2535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	120	recni 9680	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	121	mulid2i 9671	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
123	122	eqcomi 2470	. . . . . . . . . . . . . . . . . . . . . . . . . 26
124	123	oveq2i 6325	. . . . . . . . . . . . . . . . . . . . . . . . 25
125	124	oveq1i 6324	. . . . . . . . . . . . . . . . . . . . . . . 24
126	117, 125	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . 23
127	126	adantl 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
128		simpl 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
129		2pos 10728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
130	28, 118, 129, 68	mulgt0ii 9793	. . . . . . . . . . . . . . . . . . . . . . . . . 26
131	110	eqcomi 2470	. . . . . . . . . . . . . . . . . . . . . . . . . 26
132	130, 131	breqtri 4439	. . . . . . . . . . . . . . . . . . . . . . . . 25
133	120, 132	elrpii 11333	. . . . . . . . . . . . . . . . . . . . . . . 24
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
135		1zzd 10996	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136		modcyc 12163	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
137	128, 134, 135, 136	syl3anc 1276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
138	127, 137	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . 21 $/\$
139	138	breq1d 4425	. . . . . . . . . . . . . . . . . . . 20 $/\$
140	139	ifbid 3914	. . . . . . . . . . . . . . . . . . 19 $/\$
141		id 22	. . . . . . . . . . . . . . . . . . . 20
142	120	a1i 11	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	readdcld 9695	. . . . . . . . . . . . . . . . . . 19
144	116, 140, 143, 108	fvmptd 5976	. . . . . . . . . . . . . . . . . 18
145	104	fvmpt2 5979	. . . . . . . . . . . . . . . . . . 19 $/\$
146	107, 145	mpan2 682	. . . . . . . . . . . . . . . . . 18
147	144, 146	eqtr4d 2498	. . . . . . . . . . . . . . . . 17
148		eqid 2461	. . . . . . . . . . . . . . . . 17
149		snfi 7675	. . . . . . . . . . . . . . . . . 18
150		eldifi 3566	. . . . . . . . . . . . . . . . . . . . . 22 $\$
151		0xr 9712	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
152	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
153	118	rexri 9718	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
154	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155		elioore 11694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
156	155	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
157		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
158	118	renegcli 9960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159	158	rexri 9718	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
160		iooltub 37647	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
161	159, 153, 160	mp3an12 1363	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
162	161	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
163	152, 154, 156, 157, 162	eliood 37632	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
164		negpilt0 37527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
165	158, 67, 164	ltleii 9782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
166		iooss1 11699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
167	159, 165, 166	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168	167	sseli 3439	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
169	104	reseq1i 5119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
170		ioossre 11724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
171		resmpt 5172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
172	170, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
173		elioore 11694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
174	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
175		0red 9669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
176		ioogtlb 37629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
177	151, 153, 176	mp3an12 1363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
178	175, 173, 177	ltled 9808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
179	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
180	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
181	168, 161	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
182		pirp 23464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
183		2timesgt 37538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
184	182, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
185	184, 131	breqtri 4439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
187	173, 179, 180, 181, 186	lttrd 9821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
188		modid 12152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
189	173, 174, 178, 187, 188	syl22anc 1277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
190	189, 181	eqbrtrd 4436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191	190	iftrued 3900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192	191	mpteq2ia 4498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193	169, 172, 192	3eqtrri 2488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
194	193	oveq2i 6325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
195		reelprrecn 9656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
196	195	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
197		iooretop 21834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
198		eqid 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ℂ_fld
199	198	tgioo2 21869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
200	197, 199	eleqtri 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ℂ_fld ↾_t
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
202		1cnd 9684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
203	196, 201, 202	dvmptconst 37822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
204	203	trud 1463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
205		ssid 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
206		ax-resscn 9621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
207		fss 5759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
208	109, 206, 207	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
209		dvresioo 37830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
210	205, 208, 209	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	194, 204, 210	3eqtr3i 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212	211	dmeqi 5054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
213		eqid 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
214	89, 213	dmmpti 5728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
215	212, 214	eqtr3i 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
216		ssdmres 5144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
217	215, 216	mpbir 214	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
218	217	sseli 3439	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
219	168, 218	elind 3629	. . . . . . . . . . . . . . . . . . . . . . . . . 26
220		dmres 5143	. . . . . . . . . . . . . . . . . . . . . . . . . 26
221	219, 220	syl6eleqr 2550	. . . . . . . . . . . . . . . . . . . . . . . . 25
222	163, 221	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
223	222	adantlr 726	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
224	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
225	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
226	155	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
227		ioogtlb 37629	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
228	159, 153, 227	mp3an12 1363	. . . . . . . . . . . . . . . . . . . . . . . . . 26
229	228	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
230		0red 9669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
231		neqne 2642	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
232	231	ad2antlr 738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
233		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
234	226, 230, 232, 233	lttri5d 37554	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
235	224, 225, 226, 229, 234	eliood 37632	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
236	67, 118, 68	ltleii 9782	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
237		iooss2 11700	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
238	153, 236, 237	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
239	238	sseli 3439	. . . . . . . . . . . . . . . . . . . . . . . . . 26
240	104	reseq1i 5119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
241		ioossre 11724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
242		resmpt 5172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
243	241, 242	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
244	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
245		elioore 11694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
247	245, 246	modcld 12133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
248	245, 143	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
249	52	2timesi 10758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
250	110, 249	eqtri 2483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
251	250	oveq2i 6325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
252		negpicn 23465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
253	252, 52, 52	addassi 9676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
254	253	eqcomi 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
255	52	negidi 9968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
256	52, 252, 255	addcomli 9850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
257	256	oveq1i 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
258	52	addid2i 9846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
259	257, 258	eqtri 2483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
260	251, 254, 259	3eqtrri 2488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
266	261, 265	eqbrtrd 4436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
267	244, 248, 266	ltled 9808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
268		0red 9669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
269	158, 120	readdcli 9681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
271	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
272	271, 260	syl6breq 4455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
273	268, 270, 248, 272, 265	lttrd 9821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
274	268, 248, 273	ltled 9808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
275	245	recnd 9694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
276	121	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
277	275, 276	addcomd 9860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
278		iooltub 37647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$
279	159, 151, 278	mp3an12 1363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
280		ltaddneg 37545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
281	245, 120, 280	sylancl 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
282	279, 281	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
283	277, 282	eqbrtrd 4436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
284	274, 283	jca 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
285		modid2 12155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
286	248, 133, 285	sylancl 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
287	284, 286	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
288	125	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
289	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
290		1zzd 10996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
291	141, 289, 290, 136	syl3anc 1276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
292	288, 291	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
293	245, 292	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
294	287, 293	eqtr3d 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
295	267, 294	breqtrd 4440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
296	244, 247, 295	lensymd 9811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
297	296	iffalsed 3903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
298	297	mpteq2ia 4498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
299	240, 243, 298	3eqtrri 2488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
300	299	oveq2i 6325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
301		iooretop 21834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
302	301, 199	eleqtri 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
303	302	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ℂ_fld ↾_t
304	202	negcld 9998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
305	196, 303, 304	dvmptconst 37822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
306	305	trud 1463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
307		dvresioo 37830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
308	205, 208, 307	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
309	300, 306, 308	3eqtr3i 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
310	309	dmeqi 5054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
311		eqid 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
312	89, 311	dmmpti 5728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
313	310, 312	eqtr3i 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314		ssdmres 5144	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
315	313, 314	mpbir 214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
316	315	sseli 3439	. . . . . . . . . . . . . . . . . . . . . . . . . 26
317	239, 316	elind 3629	. . . . . . . . . . . . . . . . . . . . . . . . 25
318	317, 220	syl6eleqr 2550	. . . . . . . . . . . . . . . . . . . . . . . 24
319	235, 318	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
320	223, 319	pm2.61dan 805	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
321	150, 320	sylan 478	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
322		eldifn 3567	. . . . . . . . . . . . . . . . . . . . . 22 $\$
323	322	adantr 471	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
324	321, 323	condan 808	. . . . . . . . . . . . . . . . . . . 20 $\$
325		elsn 3993	. . . . . . . . . . . . . . . . . . . 20
326	324, 325	sylibr 217	. . . . . . . . . . . . . . . . . . 19 $\$
327	326	ssriv 3447	. . . . . . . . . . . . . . . . . 18 $\$
328		ssfi 7817	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$
329	149, 327, 328	mp2an 683	. . . . . . . . . . . . . . . . 17 $\$
330		inss1 3663	. . . . . . . . . . . . . . . . . . . . . 22
331	220, 330	eqsstri 3473	. . . . . . . . . . . . . . . . . . . . 21
332		ioosscn 37628	. . . . . . . . . . . . . . . . . . . . 21
333	331, 332	sstri 3452	. . . . . . . . . . . . . . . . . . . 20
334	333	a1i 11	. . . . . . . . . . . . . . . . . . 19
335		dvf 22910	. . . . . . . . . . . . . . . . . . . . . 22
336		fresin 5774	. . . . . . . . . . . . . . . . . . . . . 22
337		ffdm 5765	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
338	335, 336, 337	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 $/\$
339	338	simpli 464	. . . . . . . . . . . . . . . . . . . 20
340	339	a1i 11	. . . . . . . . . . . . . . . . . . 19
341	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
342	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
343		ioossre 11724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
344	331	sseli 3439	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
345	343, 344	sseldi 3441	. . . . . . . . . . . . . . . . . . . . . . . . . 26
346	345	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
347	344, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
348	347	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
349		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
350	341, 342, 346, 348, 349	eliood 37632	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
351		elun1 3612	. . . . . . . . . . . . . . . . . . . . . . . 24
352	350, 351	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
353		simpl 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
354		0red 9669	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
355	345	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
356		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
357	354, 355, 356	nltled 9810	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
358		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
359	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
360		eqid 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
361	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
362		0red 9669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
363		mnfxr 11442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
364	363	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
365	362	mnfltd 11454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
366	360, 364, 362, 365	lptioo2 37748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
367		incom 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
368		ioossre 11724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
369		df-ss 3429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
370	368, 369	mpbi 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
371	367, 370	eqtr2i 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
372	371	fveq2i 5890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
373	366, 372	syl6eleq 2549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
374		pnfxr 11440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
376	362	ltpnfd 11451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
377	360, 362, 375, 376	lptioo1 37749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
378		incom 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
379		ioossre 11724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
380		df-ss 3429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
381	379, 380	mpbi 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
382	378, 381	eqtr2i 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
383	382	fveq2i 5890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384	377, 383	syl6eleq 2549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
385		eqid 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
386		mnfle 11463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
387	159, 386	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
388		iooss1 11699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
389	363, 387, 388	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
390	389	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
391		ioosscn 37628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
392	390, 391	syl6ss 3455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
393		0cnd 9661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
394	385, 392, 304, 393	constlimc 37741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
395		resabs1 5151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
396	389, 395	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
397	299, 396	eqtr4i 2486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
398	397	oveq1i 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
399		fssres 5771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
400	208, 368, 399	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
401	400	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
402	391	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
403		eqid 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
404		0le0 10726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
405		elioc2 11725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
406	159, 67, 405	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
407	67, 164, 404, 406	mpbir3an 1196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
408	198	cnfldtop 21852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld
409		ovex 6342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
410		resttop 20224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
411	408, 409, 410	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
412	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
413		eqid 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
414	387	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
415	364, 412, 362, 360, 413, 414, 362	iocopn 37658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
416	415	trud 1463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
417	199	oveq1i 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
418		iocssre 11742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
419	363, 67, 418	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
420	195	elexi 3066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
421		restabs 20229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
422	408, 419, 420, 421	mp3an 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
423	417, 422	eqtri 2483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
424	416, 423	eleqtri 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
425		isopn3i 20146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
426	411, 424, 425	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
427		mnflt0 11455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
428		snunioo2 37643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
429	363, 151, 427, 428	mp3an 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
430	429	eqcomi 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
431	430	oveq2i 6325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
432	431	fveq2i 5890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
433		snunioo2 37643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
434	159, 151, 164, 433	mp3an 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
435	434	eqcomi 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
436	432, 435	fveq12i 5892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
437	426, 436	eqtr3i 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
438	407, 437	eleqtri 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
439	438	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
440	401, 390, 402, 198, 403, 439	limcres 22889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
441	440	trud 1463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
442	398, 441	eqtri 2483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
443	394, 442	syl6eleq 2549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
444		eqid 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
445		ioosscn 37628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
446	445	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
447	444, 446, 202, 393	constlimc 37741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
448		ltpnf 11450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
449		xrltle 11476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
450	153, 374, 449	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
451	118, 448, 450	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
452		iooss2 11700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
453	374, 451, 452	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
454		resabs1 5151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
455	453, 454	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
456	193, 455	eqtr4i 2486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
457	456	oveq1i 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
458		fssres 5771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
459	208, 379, 458	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
460	459	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
461	453	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
462		ioosscn 37628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
463	462	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
464		eqid 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
465		elico2 11726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
466	67, 153, 465	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
467	67, 404, 68, 466	mpbir3an 1196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
468		ovex 6342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
469		resttop 20224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
470	408, 468, 469	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
471	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
472		eqid 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
473	451	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
474	362, 471, 375, 360, 472, 473	icoopn 37663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
475	474	trud 1463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
476	199	oveq1i 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
477		rge0ssre 11768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
478		restabs 20229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
479	408, 477, 420, 478	mp3an 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
480	476, 479	eqtri 2483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
481	475, 480	eleqtri 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
482		isopn3i 20146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
483	470, 481, 482	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
484		0ltpnf 11452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
485		snunioo1 37650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
486	151, 374, 484, 485	mp3an 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
487	486	eqcomi 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
488	487	oveq2i 6325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
489	488	fveq2i 5890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
490		snunioo1 37650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
491	151, 153, 68, 490	mp3an 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
492	491	eqcomi 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
493	489, 492	fveq12i 5892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
494	483, 493	eqtr3i 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
495	467, 494	eleqtri 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
496	495	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
497	460, 461, 463, 198, 464, 496	limcres 22889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
498	497	trud 1463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
499	457, 498	eqtri 2483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
500	447, 499	syl6eleq 2549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
501		neg1lt0 10743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
502	106, 67, 105	lttri 9785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
503	501, 34, 502	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
504	106, 503	ltneii 9772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
505	504	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
506	198, 359, 360, 361, 362, 373, 384, 443, 500, 505	jumpncnp 37813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
507	506	trud 1463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
508	206	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
509	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
510	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
511		inss2 3664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
512	220, 511	eqsstri 3473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
513	512	sseli 3439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
514	199, 198	dvcnp2 22922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ ℂ_fld
515	508, 509, 510, 513, 514	syl31anc 1279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
516	507, 515	mto 181	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
517	516	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
518	358, 517	eqneltrd 2558	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
519	518	necon2ai 2664	. . . . . . . . . . . . . . . . . . . . . . . . . 26
520	519	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
521	354, 355, 357, 520	leneltd 9814	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
522	344, 163	sylan 478	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
523		elun2 3613	. . . . . . . . . . . . . . . . . . . . . . . . 25
524	522, 523	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
525	353, 521, 524	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
526	352, 525	pm2.61dan 805	. . . . . . . . . . . . . . . . . . . . . 22
527		ovex 6342	. . . . . . . . . . . . . . . . . . . . . . 23
528		ovex 6342	. . . . . . . . . . . . . . . . . . . . . . 23
529	527, 528	unipr 4224	. . . . . . . . . . . . . . . . . . . . . 22
530	526, 529	syl6eleqr 2550	. . . . . . . . . . . . . . . . . . . . 21
531	530	ssriv 3447	. . . . . . . . . . . . . . . . . . . 20
532	531	a1i 11	. . . . . . . . . . . . . . . . . . 19
533		ineq2 3639	. . . . . . . . . . . . . . . . . . . . . . 23
534		retop 21830	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
535		ovex 6342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
536	535	resex 5166	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
537	536	dmex 6752	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
538	534, 537	pm3.2i 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
539	318	ssriv 3447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
540		ssid 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
541	301, 539, 540	3pm3.2i 1192	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
542		restopnb 20239	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
543	538, 541, 542	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
544	301, 543	mpbi 213	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
545		inss2 3664	. . . . . . . . . . . . . . . . . . . . . . . . 25
546	539, 540	ssini 3666	. . . . . . . . . . . . . . . . . . . . . . . . 25
547	545, 546	eqssi 3459	. . . . . . . . . . . . . . . . . . . . . . . 24
548	199	oveq1i 6324	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t ℂ_fld ↾_t ↾_t
549	331, 343	sstri 3452	. . . . . . . . . . . . . . . . . . . . . . . . . 26
550		restabs 20229	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
551	408, 549, 420, 550	mp3an 1373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
552	548, 551	eqtr2i 2484	. . . . . . . . . . . . . . . . . . . . . . . 24 ℂ_fld ↾_t ↾_t
553	544, 547, 552	3eltr4i 2552	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
554	533, 553	syl6eqel 2547	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ↾_t
555	554	adantl 472	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ℂ_fld ↾_t
556		neqne 2642	. . . . . . . . . . . . . . . . . . . . . . 23
557		elprn1 37750	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
558	556, 557	sylan2 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
559		ineq2 3639	. . . . . . . . . . . . . . . . . . . . . . 23
560	221	ssriv 3447	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
561		ssid 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
562	197, 560, 561	3pm3.2i 1192	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
563		restopnb 20239	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
564	538, 562, 563	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
565	197, 564	mpbi 213	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
566		inss2 3664	. . . . . . . . . . . . . . . . . . . . . . . . 25
567	560, 561	ssini 3666	. . . . . . . . . . . . . . . . . . . . . . . . 25
568	566, 567	eqssi 3459	. . . . . . . . . . . . . . . . . . . . . . . 24
569	565, 568, 552	3eltr4i 2552	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
570	559, 569	syl6eqel 2547	. . . . . . . . . . . . . . . . . . . . . 22