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 31855

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 variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 11129	. . . . . . 7
2		1zzd 10907	. . . . . . 7
3		eqidd 2468	. . . . . . . . 9
4		oveq2 6303	. . . . . . . . . . . . . 14
5	4	oveq1d 6310	. . . . . . . . . . . . 13
6	5	oveq1d 6310	. . . . . . . . . . . 12
7	6	fveq2d 5876	. . . . . . . . . . 11
8	7, 5	oveq12d 6313	. . . . . . . . . 10
9	8	adantl 466	. . . . . . . . 9 $/\$
10		id 22	. . . . . . . . 9
11		ovex 6320	. . . . . . . . . 10
12	11	a1i 11	. . . . . . . . 9
13	3, 9, 10, 12	fvmptd 5962	. . . . . . . 8
14	13	adantl 466	. . . . . . 7 $/\$
15		ax-resscn 9561	. . . . . . . . . . . . 13
16		2z 10908	. . . . . . . . . . . . . . . . 17
17	16	a1i 11	. . . . . . . . . . . . . . . 16
18		nnz 10898	. . . . . . . . . . . . . . . 16
19	17, 18	zmulcld 10984	. . . . . . . . . . . . . . 15
20		1zzd 10907	. . . . . . . . . . . . . . 15
21	19, 20	zsubcld 10983	. . . . . . . . . . . . . 14
22	21	zred 10978	. . . . . . . . . . . . 13
23	15, 22	sseldi 3507	. . . . . . . . . . . 12
24		fouriersw.x	. . . . . . . . . . . . . 14
25	15, 24	sselii 3506	. . . . . . . . . . . . 13
26	25	a1i 11	. . . . . . . . . . . 12
27	23, 26	jca 532	. . . . . . . . . . 11 $/\$
28		mulcl 9588	. . . . . . . . . . 11 $/\$
29	27, 28	syl 16	. . . . . . . . . 10
30		sincl 13739	. . . . . . . . . 10
31	29, 30	syl 16	. . . . . . . . 9
32		0re 9608	. . . . . . . . . . 11
33	32	a1i 11	. . . . . . . . . 10
34		2re 10617	. . . . . . . . . . . . . 14
35	34	a1i 11	. . . . . . . . . . . . 13
36		1re 9607	. . . . . . . . . . . . . 14
37	36	a1i 11	. . . . . . . . . . . . 13
38	35, 37	remulcld 9636	. . . . . . . . . . . 12
39	38, 37	resubcld 9999	. . . . . . . . . . 11
40		0lt1 10087	. . . . . . . . . . . . 13
41	15, 34	sselii 3506	. . . . . . . . . . . . . . . 16
42	41	mulid1i 9610	. . . . . . . . . . . . . . 15
43	42	oveq1i 6305	. . . . . . . . . . . . . 14
44		2m1e1 10662	. . . . . . . . . . . . . 14
45	43, 44	eqtr2i 2497	. . . . . . . . . . . . 13
46	40, 45	breqtri 4476	. . . . . . . . . . . 12
47	46	a1i 11	. . . . . . . . . . 11
48	19	zred 10978	. . . . . . . . . . . 12
49		nnre 10555	. . . . . . . . . . . . 13
50		2pos 10639	. . . . . . . . . . . . . . 15
51	32, 34, 50	ltleii 9719	. . . . . . . . . . . . . 14
52	51	a1i 11	. . . . . . . . . . . . 13
53		nnge1 10574	. . . . . . . . . . . . 13
54	37, 49, 35, 52, 53	lemul2ad 10498	. . . . . . . . . . . 12
55	38, 48, 37, 54	lesub1dd 10180	. . . . . . . . . . 11
56	33, 39, 22, 47, 55	ltletrd 9753	. . . . . . . . . 10
57	33, 56	gtned 9731	. . . . . . . . 9
58	31, 23, 57	divcld 10332	. . . . . . . 8
59	58	adantl 466	. . . . . . 7 $/\$
60		pire 22718	. . . . . . . . . . . . . 14
61	15, 60	sselii 3506	. . . . . . . . . . . . 13
62	61	a1i 11	. . . . . . . . . . . 12
63		4cn 10625	. . . . . . . . . . . . 13
64	63	a1i 11	. . . . . . . . . . . 12
65		4ne0 10644	. . . . . . . . . . . . 13
66	65	a1i 11	. . . . . . . . . . . 12
67	62, 64, 66	divcld 10332	. . . . . . . . . . 11
68	32	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
69	15, 68	sseldi 3507	. . . . . . . . . . . . . . . . . . . 20
70	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
71		nncn 10556	. . . . . . . . . . . . . . . . . . . . . . 23
72		mulcl 9588	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
73	71, 61, 72	sylancl 662	. . . . . . . . . . . . . . . . . . . . . 22
74	61	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
75		nnne0 10580	. . . . . . . . . . . . . . . . . . . . . . 23
76		pipos 22720	. . . . . . . . . . . . . . . . . . . . . . . . 25
77	32, 76	gtneii 9708	. . . . . . . . . . . . . . . . . . . . . . . 24
78	77	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
79	71, 74, 75, 78	mulne0d 10213	. . . . . . . . . . . . . . . . . . . . . 22
80	70, 73, 79	divcld 10332	. . . . . . . . . . . . . . . . . . . . 21
81	25	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
82	71, 81	mulcld 9628	. . . . . . . . . . . . . . . . . . . . . 22
83	82	sincld 13743	. . . . . . . . . . . . . . . . . . . . 21
84	80, 83	mulcld 9628	. . . . . . . . . . . . . . . . . . . 20
85	69, 84	ifcld 3988	. . . . . . . . . . . . . . . . . . 19
86	85	rgen 2827	. . . . . . . . . . . . . . . . . 18
87		eqid 2467	. . . . . . . . . . . . . . . . . . 19
88	87	fmpt 6053	. . . . . . . . . . . . . . . . . 18
89	86, 88	mpbi 208	. . . . . . . . . . . . . . . . 17
90	89	a1i 11	. . . . . . . . . . . . . . . 16
91		eqidd 2468	. . . . . . . . . . . . . . . . . . . 20
92		breq2 4457	. . . . . . . . . . . . . . . . . . . . . 22
93		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . 22
94		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . 24
95	94	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . 23
96		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . 24
97	96	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . 23
98	95, 97	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . 22
99	92, 93, 98	ifeq123d 31337	. . . . . . . . . . . . . . . . . . . . 21
100	99	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$
101	32	elexi 3128	. . . . . . . . . . . . . . . . . . . . . 22
102		ovex 6320	. . . . . . . . . . . . . . . . . . . . . 22
103	101, 102	ifex 4014	. . . . . . . . . . . . . . . . . . . . 21
104	103	a1i 11	. . . . . . . . . . . . . . . . . . . 20
105	91, 100, 10, 104	fvmptd 5962	. . . . . . . . . . . . . . . . . . 19
106	105	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$
107		simpr 461	. . . . . . . . . . . . . . . . . . . 20 $/\$
108		simpl 457	. . . . . . . . . . . . . . . . . . . . 21 $/\$
109		2nn 10705	. . . . . . . . . . . . . . . . . . . . . 22
110	109	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
111		nndivdvds 13870	. . . . . . . . . . . . . . . . . . . . 21 $/\$
112	108, 110, 111	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$
113	107, 112	mpbird 232	. . . . . . . . . . . . . . . . . . 19 $/\$
114	113	iftrued 3953	. . . . . . . . . . . . . . . . . 18 $/\$
115	106, 114	eqtrd 2508	. . . . . . . . . . . . . . . . 17 $/\$
116	115	3adant1 1014	. . . . . . . . . . . . . . . 16 $/\$ $/\$
117		breq2 4457	. . . . . . . . . . . . . . . . . . . . . . 23
118		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . 24
119	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
120		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . 24
121	120	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . 23
122	117, 119, 121	ifeq123d 31337	. . . . . . . . . . . . . . . . . . . . . 22
123		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . 23
124	123	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . 22
125	122, 124	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . 21
126	125	cbvmptv 4544	. . . . . . . . . . . . . . . . . . . 20
127		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . 23
128	125	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
129		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
130	69, 80	ifcld 3988	. . . . . . . . . . . . . . . . . . . . . . . 24
131	130, 83	mulcld 9628	. . . . . . . . . . . . . . . . . . . . . . 23
132	127, 128, 129, 131	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . . 22
133		iftrue 3951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	133	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	134	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
136	83	mul02d 9789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137	136	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
138	135, 137	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
139		iftrue 3951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
140	139	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
141	140	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
142	138, 141	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
143		iffalse 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
144	143	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
145	144	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
146		iffalse 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
147	146	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
148	147	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
149	145, 148	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
150	142, 149	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . . . . . . 25
151	150	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
152	128, 151	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
153	127, 152, 129, 85	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . . 22
154	132, 153	eqtr3d 2510	. . . . . . . . . . . . . . . . . . . . 21
155	154	mpteq2ia 4535	. . . . . . . . . . . . . . . . . . . 20
156	126, 155	eqtr2i 2497	. . . . . . . . . . . . . . . . . . 19
157		seqeq3 12092	. . . . . . . . . . . . . . . . . . 19
158	156, 157	ax-mp 5	. . . . . . . . . . . . . . . . . 18
159		fouriersw.f	. . . . . . . . . . . . . . . . . . . . 21
160	36	renegcli 9892	. . . . . . . . . . . . . . . . . . . . . . 23
161		ifcl 3987	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
162	36, 160, 161	mp2an 672	. . . . . . . . . . . . . . . . . . . . . 22
163	162	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
164	159, 163	fmpti 6055	. . . . . . . . . . . . . . . . . . . 20
165		fouriersw.t	. . . . . . . . . . . . . . . . . . . 20
166		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
167	166	breq1d 4463	. . . . . . . . . . . . . . . . . . . . . . . . . 26
168		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . 26
169		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . 26
170	167, 168, 169	ifeq123d 31337	. . . . . . . . . . . . . . . . . . . . . . . . 25
171	170	cbvmptv 4544	. . . . . . . . . . . . . . . . . . . . . . . 24
172	159, 171	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . 23
173	172	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
174		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
175	34, 60	remulcli 9622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
176	165, 175	eqeltri 2551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
177	176	recni 9620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178	177	mulid2i 9611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179	178	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180	179	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
181	180	oveq1i 6305	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
183	174, 182	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . 26
184	183	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
185		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
186	34, 60	mulgt0i 9728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
187	50, 76, 186	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
188	165	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
189	187, 188	breqtri 4476	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
190		elrp 11234	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
191	176, 189, 190	mpbir2an 918	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
192	191	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
193		1zzd 10907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
194		modcyc 12011	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
195	185, 192, 193, 194	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
196	184, 195	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
197	196	breq1d 4463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
198		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
199		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
200	197, 198, 199	ifeq123d 31337	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
201		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
202	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
203	201, 202	readdcld 9635	. . . . . . . . . . . . . . . . . . . . . 22
204	173, 200, 203, 163	fvmptd 5962	. . . . . . . . . . . . . . . . . . . . 21
205	159	fvmpt2 5964	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
206	201, 163, 205	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22
207	206	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . 21
208		eqidd 2468	. . . . . . . . . . . . . . . . . . . . 21
209	204, 207, 208	3eqtrd 2512	. . . . . . . . . . . . . . . . . . . 20
210		eqid 2467	. . . . . . . . . . . . . . . . . . . 20
211		snfi 7608	. . . . . . . . . . . . . . . . . . . . 21
212		eldifi 3631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
213	212	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$
214		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$
215		0xr 9652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
216	215	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
217	60	rexri 9658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
218	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
219		elioore 11571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
220	219	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
221		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
222	60	renegcli 9892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
223	222	rexri 9658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
224	223	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
225	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
226		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
227		iooltub 31435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
228	224, 225, 226, 227	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
229	228	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
230	216, 218, 220, 221, 229	eliood 31418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
231		negpilt0 31362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
232	222, 32, 231	ltleii 9719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
233		iooss1 11576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
234	223, 232, 233	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
235		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
236	234, 235	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
237		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
238	101, 237	dmmpti 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
239	238	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
240		reelprrecn 9596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
241	240	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
242		iooretop 21141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
243		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ℂ_fld
244	243	tgioo2 21176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t
245	242, 244	eleqtri 2553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
246	245	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
247		1cnd 9624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
248	241, 246, 247	dvmptconst 31566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
249	248	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
250	249	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
251	159	reseq1i 5275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
252		ioossre 11598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
253		resmpt 5329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
254	252, 253	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
255	236, 219	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
256	191	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
257	32	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
258	215	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
259	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
260		ioogtlb 31415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$
261	258, 259, 235, 260	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
262	257, 255, 261	ltled 9744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
263	60	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
264	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
265	236, 228	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
266	60, 76	elrpii 11235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
267		2timesgt 31375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
268	266, 267	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
269	268, 188	breqtri 4476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
271	255, 263, 264, 265, 270	lttrd 9754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
272		modid 12000	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
273	255, 256, 262, 271, 272	syl22anc 1229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
274	273, 265	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
275	274	iftrued 3953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
276	275	mpteq2ia 4535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
277	251, 254, 276	3eqtri 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
278	277	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
279	278	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
280	201	ssriv 3513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
281		fss 5745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
282	164, 15, 281	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
283		dvresioo 31574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
284	280, 282, 283	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
285	250, 279, 284	3eqtri 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
286	285	dmeqi 5210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
287	239, 286	eqtr2i 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
288		ssdmres 5301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
289	287, 288	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
290	289, 235	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
291	236, 290	elind 3693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
292		dmres 5300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
293	292	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
294	293	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
295	291, 294	eleqtrd 2557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
296	230, 295	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
297	296	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
298	223	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
299	215	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
300	219	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
301		ioogtlb 31415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
302	224, 225, 226, 301	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
303	302	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
304	32	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
305		neqne 31339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
306	305	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
307		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
308	300, 304, 306, 307	lttri5d 31399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
309	298, 299, 300, 303, 308	eliood 31418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
310	32, 60, 76	ltleii 9719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
311		iooss2 11577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
312	217, 310, 311	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
313		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
314	312, 313	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
315		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
316	101, 315	dmmpti 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
317	316	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
318		iooretop 21141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
319	318, 244	eleqtri 2553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
320	319	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
321	247	negcld 9929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
322	241, 320, 321	dvmptconst 31566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
323	322	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
324	323	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
325	159	reseq1i 5275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
326		ioossre 11598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
327		resmpt 5329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
328	326, 327	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
329	60	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
330	314, 219	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
331	330, 203	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
332		2times 10666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
333	61, 332	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
334	165, 333	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
335	334	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
336	15, 222	sselii 3506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
337	336, 61, 61	addassi 9616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
338	337	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
339	336, 61	addcomi 9782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
340	61	negidi 9900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
341	339, 340	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
342	341	oveq1i 6305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
343	61	addid2i 9779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
344	342, 343	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
345	335, 338, 344	3eqtrri 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
346	345	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
347	222	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
348	176	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
349	314, 302	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
350	347, 330, 348, 349	ltadd1dd 10175	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
351	346, 350	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
352	329, 331, 351	ltled 9744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
353		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
354	32	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
355	222, 176	readdcli 9621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
356	355	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
357	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
358	357, 346	breqtrd 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
359	354, 356, 331, 358, 350	lttrd 9754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
360	354, 331, 359	ltled 9744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
361	15, 330	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
362	177	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
363	361, 362	addcomd 9793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
364	223	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
365	215	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
366		iooltub 31435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$
367	364, 365, 313, 366	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
368		ltaddneg 31384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$
369	330, 348, 368	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
370	367, 369	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
371	363, 370	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
372	360, 371	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
373	191	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
374		modid2 12003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$
375	331, 373, 374	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
376	372, 375	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
377	376	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
378	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
379	191	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
380		1zzd 10907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
381	201, 379, 380, 194	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
382	378, 381	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
383	330, 382	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
384	353, 377, 383	3eqtrd 2512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
385	352, 384	breqtrd 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
386	384, 331	eqeltrrd 2556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
387	329, 386	lenltd 9742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
388	385, 387	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
389	388	iffalsed 3956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
390	389	mpteq2ia 4535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
391	325, 328, 390	3eqtri 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
392	391	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
393	392	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
394		dvresioo 31574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
395	280, 282, 394	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
396	324, 393, 395	3eqtri 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
397	396	dmeqi 5210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
398	317, 397	eqtr2i 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
399		ssdmres 5301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
400	398, 399	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
401	400, 313	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
402	314, 401	elind 3693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
403	293	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
404	402, 403	eleqtrd 2557	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
405	309, 404	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
406	297, 405	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
407	213, 214, 406	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
408		eldifn 3632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
409	408	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
410	407, 409	condan 792	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
411		elsn 4047	. . . . . . . . . . . . . . . . . . . . . . . 24
412	410, 411	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
413	412	rgen 2827	. . . . . . . . . . . . . . . . . . . . . 22 $\$
414		dfss3 3499	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
415	413, 414	mpbir 209	. . . . . . . . . . . . . . . . . . . . 21 $\$
416		ssfi 7752	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$
417	211, 415, 416	mp2an 672	. . . . . . . . . . . . . . . . . . . 20 $\$
418		inss1 3723	. . . . . . . . . . . . . . . . . . . . . . . . 25
419	292, 418	eqsstri 3539	. . . . . . . . . . . . . . . . . . . . . . . 24
420		ioosscn 31414	. . . . . . . . . . . . . . . . . . . . . . . 24
421	419, 420	sstri 3518	. . . . . . . . . . . . . . . . . . . . . . 23
422	421	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
423		dvf 22179	. . . . . . . . . . . . . . . . . . . . . . . . . 26
424		fresin 5760	. . . . . . . . . . . . . . . . . . . . . . . . . 26
425	423, 424	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25
426		ffdm 5751	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
427	425, 426	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
428	427	simpli 458	. . . . . . . . . . . . . . . . . . . . . . 23
429	428	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
430	223	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
431	215	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
432	219	ssriv 3513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
433	419	sseli 3505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
434	432, 433	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
435	434	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
436	433, 302	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
437	436	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
438		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
439	430, 431, 435, 437, 438	eliood 31418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
440		elun1 3676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
441	439, 440	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
442		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
443	32	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
444	442, 434	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
445		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
446	443, 444	lenltd 9742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
447	445, 446	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
448		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
449	15	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
450	282	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
451	280	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
452		inss2 3724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
453	292, 452	eqsstri 3539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
454		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
455	453, 454	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
456	244, 243	dvcnp2 22191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ ℂ_fld
457	449, 450, 451, 455, 456	syl31anc 1231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ℂ_fld
458	280	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
459		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
460	282	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
461	32	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
462		mnfxr 11335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
463	462	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
464	461	mnfltd 31391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
465	459, 463, 461, 464	lptioo2 31496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
466	465	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
467		incom 3696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
468		ioossre 11598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
469		df-ss 3495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
470	468, 469	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
471	467, 470	eqtr2i 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
472	471	fveq2i 5875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
473	466, 472	eleqtri 2553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
474	473	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
475		pnfxr 11333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
476	475	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
477	461	ltpnfd 31380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
478	459, 461, 476, 477	lptioo1 31497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
479	478	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
480		incom 3696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
481		ioossre 11598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
482		df-ss 3495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
483	481, 482	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
484	480, 483	eqtr2i 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
485	484	fveq2i 5875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
486	479, 485	eleqtri 2553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
487	486	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
488		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
489		mnfle 11354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
490	223, 489	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
491		iooss1 11576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
492	462, 490, 491	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
493	492	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
494	468, 15	sstri 3518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
495	494	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
496	493, 495	sstrd 3519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
497		0cnd 9601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
498	488, 496, 321, 497	constlimc 31489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 lim
499	498	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 lim
500		resabs1 5308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
501	492, 500	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
502	326	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
503	460, 502	feqresmpt 5928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
504	503	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
505	392, 504	eqtr2i 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
506	501, 504, 505	3eqtrri 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
507	506	oveq1i 6305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 lim lim
508		fssres 5757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
509	282, 468, 508	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
510	509	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
511		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld ↾_t ℂ_fld ↾_t
512		0le0 10637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
513		elioc2 11599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$ $/\$ $/\$
514	223, 32, 513	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$
515	32, 231, 512, 514	mpbir3an 1178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
516	243	cnfldtop 21159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ℂ_fld
517		ovex 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
518		resttop 19529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ℂ_fld $/\$ ℂ_fld ↾_t
519	516, 517, 518	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ℂ_fld ↾_t
520	223	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
521		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ↾_t ↾_t
522	490	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
523	463, 520, 461, 459, 521, 522, 461	iocopn 31447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ↾_t
524	523	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ↾_t
525	244	oveq1i 6305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ↾_t ℂ_fld ↾_t ↾_t
526		iocssre 11616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$
527	462, 32, 526	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
528	240	elexi 3128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
529		restabs 19534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
530	516, 527, 528, 529	mp3an 1324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
531	525, 530	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ↾_t ℂ_fld ↾_t
532	524, 531	eleqtri 2553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ℂ_fld ↾_t
533		isopn3i 19451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
534	519, 532, 533	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ℂ_fld ↾_t
535	534	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ℂ_fld ↾_t
536	464	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
537		snunioo2 31431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$ $/\$
538	462, 215, 536, 537	mp3an 1324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
539	538	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
540	539	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ℂ_fld ↾_t ℂ_fld ↾_t
541	540	fveq2i 5875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ℂ_fld ↾_t ℂ_fld ↾_t
542		snunioo2 31431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$
543	223, 215, 231, 542	mp3an 1324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
544	543	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
545	541, 544	fveq12i 5877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ℂ_fld ↾_t ℂ_fld ↾_t
546	535, 545	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ℂ_fld ↾_t
547	515, 546	eleqtri 2553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ℂ_fld ↾_t
548	547	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld ↾_t
549	510, 493, 495, 243, 511, 548	limcres 22158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 lim lim
550	549	trud 1388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41