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 40448

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 11723	. . . . . . 7
2		1zzd 11408	. . . . . . 7
3		eqidd 2623	. . . . . . . . 9
4		oveq2 6658	. . . . . . . . . . . . . 14
5	4	oveq1d 6665	. . . . . . . . . . . . 13
6	5	oveq1d 6665	. . . . . . . . . . . 12
7	6	fveq2d 6195	. . . . . . . . . . 11
8	7, 5	oveq12d 6668	. . . . . . . . . 10
9	8	adantl 482	. . . . . . . . 9 $/\$
10		id 22	. . . . . . . . 9
11		ovex 6678	. . . . . . . . . 10
12	11	a1i 11	. . . . . . . . 9
13	3, 9, 10, 12	fvmptd 6288	. . . . . . . 8
14	13	adantl 482	. . . . . . 7 $/\$
15		2z 11409	. . . . . . . . . . . . . . 15
16	15	a1i 11	. . . . . . . . . . . . . 14
17		nnz 11399	. . . . . . . . . . . . . 14
18	16, 17	zmulcld 11488	. . . . . . . . . . . . 13
19		1zzd 11408	. . . . . . . . . . . . 13
20	18, 19	zsubcld 11487	. . . . . . . . . . . 12
21	20	zcnd 11483	. . . . . . . . . . 11
22		fouriersw.x	. . . . . . . . . . . . 13
23	22	recni 10052	. . . . . . . . . . . 12
24	23	a1i 11	. . . . . . . . . . 11
25	21, 24	mulcld 10060	. . . . . . . . . 10
26	25	sincld 14860	. . . . . . . . 9
27		0red 10041	. . . . . . . . . 10
28		2re 11090	. . . . . . . . . . . . . 14
29	28	a1i 11	. . . . . . . . . . . . 13
30		1red 10055	. . . . . . . . . . . . 13
31	29, 30	remulcld 10070	. . . . . . . . . . . 12
32	31, 30	resubcld 10458	. . . . . . . . . . 11
33	20	zred 11482	. . . . . . . . . . 11
34		0lt1 10550	. . . . . . . . . . . . 13
35		2t1e2 11176	. . . . . . . . . . . . . . 15
36	35	oveq1i 6660	. . . . . . . . . . . . . 14
37		2m1e1 11135	. . . . . . . . . . . . . 14
38	36, 37	eqtr2i 2645	. . . . . . . . . . . . 13
39	34, 38	breqtri 4678	. . . . . . . . . . . 12
40	39	a1i 11	. . . . . . . . . . 11
41	18	zred 11482	. . . . . . . . . . . 12
42		nnre 11027	. . . . . . . . . . . . 13
43		0le2 11111	. . . . . . . . . . . . . 14
44	43	a1i 11	. . . . . . . . . . . . 13
45		nnge1 11046	. . . . . . . . . . . . 13
46	30, 42, 29, 44, 45	lemul2ad 10964	. . . . . . . . . . . 12
47	31, 41, 30, 46	lesub1dd 10643	. . . . . . . . . . 11
48	27, 32, 33, 40, 47	ltletrd 10197	. . . . . . . . . 10
49	27, 48	gtned 10172	. . . . . . . . 9
50	26, 21, 49	divcld 10801	. . . . . . . 8
51	50	adantl 482	. . . . . . 7 $/\$
52		picn 24211	. . . . . . . . . . 11
53	52	a1i 11	. . . . . . . . . 10
54		4cn 11098	. . . . . . . . . . 11
55	54	a1i 11	. . . . . . . . . 10
56		4ne0 11117	. . . . . . . . . . 11
57	56	a1i 11	. . . . . . . . . 10
58	53, 55, 57	divcld 10801	. . . . . . . . 9
59		eqid 2622	. . . . . . . . . . . . . . . 16
60		0cnd 10033	. . . . . . . . . . . . . . . . 17
61	54	a1i 11	. . . . . . . . . . . . . . . . . . 19
62		nncn 11028	. . . . . . . . . . . . . . . . . . . 20
63		mulcl 10020	. . . . . . . . . . . . . . . . . . . 20 $/\$
64	62, 52, 63	sylancl 694	. . . . . . . . . . . . . . . . . . 19
65	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20
66		nnne0 11053	. . . . . . . . . . . . . . . . . . . 20
67		0re 10040	. . . . . . . . . . . . . . . . . . . . . 22
68		pipos 24212	. . . . . . . . . . . . . . . . . . . . . 22
69	67, 68	gtneii 10149	. . . . . . . . . . . . . . . . . . . . 21
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . 20
71	62, 65, 66, 70	mulne0d 10679	. . . . . . . . . . . . . . . . . . 19
72	61, 64, 71	divcld 10801	. . . . . . . . . . . . . . . . . 18
73	23	a1i 11	. . . . . . . . . . . . . . . . . . . 20
74	62, 73	mulcld 10060	. . . . . . . . . . . . . . . . . . 19
75	74	sincld 14860	. . . . . . . . . . . . . . . . . 18
76	72, 75	mulcld 10060	. . . . . . . . . . . . . . . . 17
77	60, 76	ifcld 4131	. . . . . . . . . . . . . . . 16
78	59, 77	fmpti 6383	. . . . . . . . . . . . . . 15
79	78	a1i 11	. . . . . . . . . . . . . 14
80		eqidd 2623	. . . . . . . . . . . . . . . . . 18
81		breq2 4657	. . . . . . . . . . . . . . . . . . . 20
82		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
83	82	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21
84		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
85	84	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21
86	83, 85	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20
87	81, 86	ifbieq2d 4111	. . . . . . . . . . . . . . . . . . 19
88	87	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
89		c0ex 10034	. . . . . . . . . . . . . . . . . . . 20
90		ovex 6678	. . . . . . . . . . . . . . . . . . . 20
91	89, 90	ifex 4156	. . . . . . . . . . . . . . . . . . 19
92	91	a1i 11	. . . . . . . . . . . . . . . . . 18
93	80, 88, 10, 92	fvmptd 6288	. . . . . . . . . . . . . . . . 17
94	93	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
95		simpr 477	. . . . . . . . . . . . . . . . . 18 $/\$
96		simpl 473	. . . . . . . . . . . . . . . . . . 19 $/\$
97		2nn 11185	. . . . . . . . . . . . . . . . . . 19
98		nndivdvds 14989	. . . . . . . . . . . . . . . . . . 19 $/\$
99	96, 97, 98	sylancl 694	. . . . . . . . . . . . . . . . . 18 $/\$
100	95, 99	mpbird 247	. . . . . . . . . . . . . . . . 17 $/\$
101	100	iftrued 4094	. . . . . . . . . . . . . . . 16 $/\$
102	94, 101	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$
103	102	3adant1 1079	. . . . . . . . . . . . . 14 $/\$ $/\$
104		fouriersw.f	. . . . . . . . . . . . . . . . . 18
105		1re 10039	. . . . . . . . . . . . . . . . . . . 20
106	105	renegcli 10342	. . . . . . . . . . . . . . . . . . . 20
107	105, 106	keepel 4155	. . . . . . . . . . . . . . . . . . 19
108	107	a1i 11	. . . . . . . . . . . . . . . . . 18
109	104, 108	fmpti 6383	. . . . . . . . . . . . . . . . 17
110		fouriersw.t	. . . . . . . . . . . . . . . . 17
111		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24
112	111	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . 23
113	112	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . 22
114	113	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . . 21
115	104, 114	eqtri 2644	. . . . . . . . . . . . . . . . . . . 20
116	115	a1i 11	. . . . . . . . . . . . . . . . . . 19
117		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24
118		pire 24210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119	28, 118	remulcli 10054	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	110, 119	eqeltri 2697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	120	recni 10052	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	121	mulid2i 10043	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
123	122	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . 26
124	123	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . 25
125	124	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . 24
126	117, 125	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23
127	126	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
128		simpl 473	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
129		2pos 11112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
130	28, 118, 129, 68	mulgt0ii 10170	. . . . . . . . . . . . . . . . . . . . . . . . . 26
131	110	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . 26
132	130, 131	breqtri 4678	. . . . . . . . . . . . . . . . . . . . . . . . 25
133	120, 132	elrpii 11835	. . . . . . . . . . . . . . . . . . . . . . . 24
134	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
135		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136		modcyc 12705	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
137	128, 134, 135, 136	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
138	127, 137	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$
139	138	breq1d 4663	. . . . . . . . . . . . . . . . . . . 20 $/\$
140	139	ifbid 4108	. . . . . . . . . . . . . . . . . . 19 $/\$
141		id 22	. . . . . . . . . . . . . . . . . . . 20
142	120	a1i 11	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	readdcld 10069	. . . . . . . . . . . . . . . . . . 19
144	116, 140, 143, 108	fvmptd 6288	. . . . . . . . . . . . . . . . . 18
145	104	fvmpt2 6291	. . . . . . . . . . . . . . . . . . 19 $/\$
146	107, 145	mpan2 707	. . . . . . . . . . . . . . . . . 18
147	144, 146	eqtr4d 2659	. . . . . . . . . . . . . . . . 17
148		eqid 2622	. . . . . . . . . . . . . . . . 17
149		snfi 8038	. . . . . . . . . . . . . . . . . 18
150		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . 22 $\$
151		0xr 10086	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
152	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
153	118	rexri 10097	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
154	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
155		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
156	155	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
157		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
158	118	renegcli 10342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159	158	rexri 10097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
160		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
161	159, 153, 160	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
162	161	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
163	152, 154, 156, 157, 162	eliood 39720	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
164		negpilt0 39492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
165	158, 67, 164	ltleii 10160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
166		iooss1 12210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
167	159, 165, 166	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
168	167	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
169	104	reseq1i 5392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
170		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
171		resmpt 5449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
172	170, 171	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
173		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
174	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
175		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
176		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
177	151, 153, 176	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
178	175, 173, 177	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
179	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
180	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
181	168, 161	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
182		pirp 24213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
183		2timesgt 39500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
184	182, 183	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
185	184, 131	breqtri 4678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
187	173, 179, 180, 181, 186	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
188		modid 12695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
189	173, 174, 178, 187, 188	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
190	189, 181	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191	190	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192	191	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193	169, 172, 192	3eqtrri 2649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
194	193	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
195		reelprrecn 10028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
196	195	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
197		iooretop 22569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
198		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ℂ_fld
199	198	tgioo2 22606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
200	197, 199	eleqtri 2699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ℂ_fld ↾_t
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
202		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
203	196, 201, 202	dvmptconst 40129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
204	203	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
205		ssid 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
206		ax-resscn 9993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
207		fss 6056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
208	109, 206, 207	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
209		dvresioo 40136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
210	205, 208, 209	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	194, 204, 210	3eqtr3i 2652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212	211	dmeqi 5325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
213		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
214	89, 213	dmmpti 6023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
215	212, 214	eqtr3i 2646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
216		ssdmres 5420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
217	215, 216	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
218	217	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
219	168, 218	elind 3798	. . . . . . . . . . . . . . . . . . . . . . . . . 26
220		dmres 5419	. . . . . . . . . . . . . . . . . . . . . . . . . 26
221	219, 220	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . . . . . . . 25
222	163, 221	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
223	222	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
224	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
225	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
226	155	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
227		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
228	159, 153, 227	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . . 26
229	228	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
230		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
231		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
232	231	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
233		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
234	226, 230, 232, 233	lttri5d 39513	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
235	224, 225, 226, 229, 234	eliood 39720	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
236	67, 118, 68	ltleii 10160	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
237		iooss2 12211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
238	153, 236, 237	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
239	238	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . 26
240	104	reseq1i 5392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
241		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
242		resmpt 5449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
243	241, 242	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
244	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
245		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
247	245, 246	modcld 12674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
248	245, 143	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
249	52	2timesi 11147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
250	110, 249	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
251	250	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
252		negpicn 24214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
253	252, 52, 52	addassi 10048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
254	253	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
255	52	negidi 10350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
256	52, 252, 255	addcomli 10228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
257	256	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
258	52	addid2i 10224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
259	257, 258	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
260	251, 254, 259	3eqtrri 2649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
266	261, 265	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
267	244, 248, 266	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
268		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
269	158, 120	readdcli 10053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
271	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
272	271, 260	syl6breq 4694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
273	268, 270, 248, 272, 265	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
274	268, 248, 273	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
275	245	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
276	121	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
277	275, 276	addcomd 10238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
278		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$
279	159, 151, 278	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
280		ltaddneg 10251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
281	245, 120, 280	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
282	279, 281	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
283	277, 282	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
284	274, 283	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
285		modid2 12697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
286	248, 133, 285	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
287	284, 286	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
288	125	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
289	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
290		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
291	141, 289, 290, 136	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
292	288, 291	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
293	245, 292	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
294	287, 293	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
295	267, 294	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
296	244, 247, 295	lensymd 10188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
297	296	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
298	297	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
299	240, 243, 298	3eqtrri 2649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
300	299	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
301		iooretop 22569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
302	301, 199	eleqtri 2699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld ↾_t
303	302	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ℂ_fld ↾_t
304	202	negcld 10379	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
305	196, 303, 304	dvmptconst 40129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
306	305	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
307		dvresioo 40136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
308	205, 208, 307	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
309	300, 306, 308	3eqtr3i 2652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
310	309	dmeqi 5325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
311		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
312	89, 311	dmmpti 6023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
313	310, 312	eqtr3i 2646	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
314		ssdmres 5420	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
315	313, 314	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
316	315	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . 26
317	239, 316	elind 3798	. . . . . . . . . . . . . . . . . . . . . . . . 25
318	317, 220	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . . . . . . 24
319	235, 318	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
320	223, 319	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
321	150, 320	sylan 488	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
322		eldifn 3733	. . . . . . . . . . . . . . . . . . . . . 22 $\$
323	322	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
324	321, 323	condan 835	. . . . . . . . . . . . . . . . . . . 20 $\$
325		velsn 4193	. . . . . . . . . . . . . . . . . . . 20
326	324, 325	sylibr 224	. . . . . . . . . . . . . . . . . . 19 $\$
327	326	ssriv 3607	. . . . . . . . . . . . . . . . . 18 $\$
328		ssfi 8180	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$
329	149, 327, 328	mp2an 708	. . . . . . . . . . . . . . . . 17 $\$
330		inss1 3833	. . . . . . . . . . . . . . . . . . . . . 22
331	220, 330	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . 21
332		ioosscn 39716	. . . . . . . . . . . . . . . . . . . . 21
333	331, 332	sstri 3612	. . . . . . . . . . . . . . . . . . . 20
334	333	a1i 11	. . . . . . . . . . . . . . . . . . 19
335		dvf 23671	. . . . . . . . . . . . . . . . . . . . . 22
336		fresin 6073	. . . . . . . . . . . . . . . . . . . . . 22
337		ffdm 6062	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
338	335, 336, 337	mp2b 10	. . . . . . . . . . . . . . . . . . . . 21 $/\$
339	338	simpli 474	. . . . . . . . . . . . . . . . . . . 20
340	339	a1i 11	. . . . . . . . . . . . . . . . . . 19
341	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
342	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
343		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
344	331	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
345	343, 344	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . 26
346	345	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
347	344, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
348	347	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
349		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
350	341, 342, 346, 348, 349	eliood 39720	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
351		elun1 3780	. . . . . . . . . . . . . . . . . . . . . . . 24
352	350, 351	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
353		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
354		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
355	345	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
356		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
357	354, 355, 356	nltled 10187	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
358		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
359	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
360		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
361	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
362		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
363		mnfxr 10096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
364	363	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
365	362	mnfltd 11958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
366	360, 364, 362, 365	lptioo2 39863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
367		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
368		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
369		df-ss 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
370	368, 369	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
371	367, 370	eqtr2i 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
372	371	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
373	366, 372	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
374		pnfxr 10092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
375	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
376	362	ltpnfd 11955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
377	360, 362, 375, 376	lptioo1 39864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
378		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
379		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
380		df-ss 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
381	379, 380	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
382	378, 381	eqtr2i 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
383	382	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
384	377, 383	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
385		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
386		mnfle 11969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
387	159, 386	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
388		iooss1 12210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
389	363, 387, 388	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
390	389	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
391		ioosscn 39716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
392	390, 391	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
393		0cnd 10033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
394	385, 392, 304, 393	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
395		resabs1 5427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
396	389, 395	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
397	299, 396	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
398	397	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
399		fssres 6070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
400	208, 368, 399	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
401	400	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
402	391	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
403		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
404		0le0 11110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
405		elioc2 12236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
406	159, 67, 405	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
407	67, 164, 404, 406	mpbir3an 1244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
408	198	cnfldtop 22587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld
409		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
410		resttop 20964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
411	408, 409, 410	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
412	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
413		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
414	387	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
415	364, 412, 362, 360, 413, 414, 362	iocopn 39746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
416	415	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
417	199	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
418		iocssre 12253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
419	363, 67, 418	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
420	195	elexi 3213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
421		restabs 20969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
422	408, 419, 420, 421	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
423	417, 422	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
424	416, 423	eleqtri 2699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
425		isopn3i 20886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
426	411, 424, 425	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
427		mnflt0 11959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
428		snunioo2 39731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
429	363, 151, 427, 428	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
430	429	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
431	430	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
432	431	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
433		snunioo2 39731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
434	159, 151, 164, 433	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
435	434	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
436	432, 435	fveq12i 6196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
437	426, 436	eqtr3i 2646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
438	407, 437	eleqtri 2699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
439	438	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
440	401, 390, 402, 198, 403, 439	limcres 23650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
441	440	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
442	398, 441	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
443	394, 442	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
444		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
445		ioosscn 39716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
446	445	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
447	444, 446, 202, 393	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim
448		ltpnf 11954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
449		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
450	153, 374, 449	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
451	118, 448, 450	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
452		iooss2 12211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
453	374, 451, 452	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
454		resabs1 5427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
455	453, 454	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
456	193, 455	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
457	456	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
458		fssres 6070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
459	208, 379, 458	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
460	459	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
461	453	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
462		ioosscn 39716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
463	462	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
464		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t ℂ_fld ↾_t
465		elico2 12237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$
466	67, 153, 465	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
467	67, 404, 68, 466	mpbir3an 1244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
468		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
469		resttop 20964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld $/\$ ℂ_fld ↾_t
470	408, 468, 469	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
471	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
472		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ↾_t ↾_t
473	451	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
474	362, 471, 375, 360, 472, 473	icoopn 39751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t
475	474	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t
476	199	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ↾_t ℂ_fld ↾_t ↾_t
477		rge0ssre 12280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
478		restabs 20969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
479	408, 477, 420, 478	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
480	476, 479	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ↾_t ℂ_fld ↾_t
481	475, 480	eleqtri 2699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t
482		isopn3i 20886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t $/\$ ℂ_fld ↾_t ℂ_fld ↾_t
483	470, 481, 482	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t
484		0ltpnf 11956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
485		snunioo1 39738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
486	151, 374, 484, 485	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
487	486	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
488	487	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ℂ_fld ↾_t ℂ_fld ↾_t
489	488	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ℂ_fld ↾_t ℂ_fld ↾_t
490		snunioo1 39738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
491	151, 153, 68, 490	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
492	491	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
493	489, 492	fveq12i 6196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ℂ_fld ↾_t ℂ_fld ↾_t
494	483, 493	eqtr3i 2646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ℂ_fld ↾_t
495	467, 494	eleqtri 2699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ℂ_fld ↾_t
496	495	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ℂ_fld ↾_t
497	460, 461, 463, 198, 464, 496	limcres 23650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 lim lim
498	497	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 lim lim
499	457, 498	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 lim lim
500	447, 499	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 lim
501		neg1lt0 11127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
502	106, 67, 105	lttri 10163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
503	501, 34, 502	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
504	106, 503	ltneii 10150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
505	504	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
506	198, 359, 360, 361, 362, 373, 384, 443, 500, 505	jumpncnp 40111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
507	506	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
508	206	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
509	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
510	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
511		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
512	220, 511	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
513	512	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
514	199, 198	dvcnp2 23683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ ℂ_fld
515	508, 509, 510, 513, 514	syl31anc 1329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
516	507, 515	mto 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
517	516	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
518	358, 517	eqneltrd 2720	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
519	518	necon2ai 2823	. . . . . . . . . . . . . . . . . . . . . . . . . 26
520	519	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
521	354, 355, 357, 520	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
522	344, 163	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
523		elun2 3781	. . . . . . . . . . . . . . . . . . . . . . . . 25
524	522, 523	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
525	353, 521, 524	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
526	352, 525	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . 22
527		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23
528		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23
529	527, 528	unipr 4449	. . . . . . . . . . . . . . . . . . . . . 22
530	526, 529	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . . . 21
531	530	ssriv 3607	. . . . . . . . . . . . . . . . . . . 20
532	531	a1i 11	. . . . . . . . . . . . . . . . . . 19
533		ineq2 3808	. . . . . . . . . . . . . . . . . . . . . . 23
534		retop 22565	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
535		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
536	535	resex 5443	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
537	536	dmex 7099	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
538	534, 537	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
539	318	ssriv 3607	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
540		ssid 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
541	301, 539, 540	3pm3.2i 1239	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
542		restopnb 20979	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
543	538, 541, 542	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
544	301, 543	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
545		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . . 25
546	539, 540	ssini 3836	. . . . . . . . . . . . . . . . . . . . . . . . 25
547	545, 546	eqssi 3619	. . . . . . . . . . . . . . . . . . . . . . . 24
548	199	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t ℂ_fld ↾_t ↾_t
549	331, 343	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . . . . 26
550		restabs 20969	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld $/\$ $/\$ ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
551	408, 549, 420, 550	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld ↾_t ↾_t ℂ_fld ↾_t
552	548, 551	eqtr2i 2645	. . . . . . . . . . . . . . . . . . . . . . . 24 ℂ_fld ↾_t ↾_t
553	544, 547, 552	3eltr4i 2714	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
554	533, 553	syl6eqel 2709	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ↾_t
555	554	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ℂ_fld ↾_t
556		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . 23
557		elprn1 39865	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
558	556, 557	sylan2 491	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
559		ineq2 3808	. . . . . . . . . . . . . . . . . . . . . . 23
560	221	ssriv 3607	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
561		ssid 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
562	197, 560, 561	3pm3.2i 1239	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
563		restopnb 20979	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ ↾_t
564	538, 562, 563	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . 25 ↾_t
565	197, 564	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . 24 ↾_t
566		inss2 3834	. . . . . . . . . . . . . . . . . . . . . . . . 25
567	560, 561	ssini 3836	. . . . . . . . . . . . . . . . . . . . . . . . 25
568	566, 567	eqssi 3619	. . . . . . . . . . . . . . . . . . . . . . . 24
569	565, 568, 552	3eltr4i 2714	. . . . . . . . . . . . . . . . . . . . . . 23 ℂ_fld ↾_t
570	559, 569	syl6eqel 2709	. . . . . . . . . . . . . . . . . . . . . 22 ℂ_fld ↾_t
571	558, 570	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ℂ_fld ↾_t
572	555, 571	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . 20 ℂ_fld ↾_t
573	572	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$ ℂ_fld ↾_t
574		ssid 3624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
575	574	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
576	392, 393, 575	constcncfg 40084	. . . . . . . . . . . . . . . . . . . . . . . . 25
577	576	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . 24
578	577	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
579		reseq2 5391	. . . . . . . . . . . . . . . . . . . . . . . 24
580		resabs1 5427	. . . . . . . . . . . . . . . . . . . . . . . . . 26
581	238, 580	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25
582	581, 309	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . . . 24
583	579, 582	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23
584	533, 547	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . 24
585	584	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23
586	578, 583, 585	3eltr4d 2716	. . . . . . . . . . . . . . . . . . . . . 22
587	586	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
588	446, 393, 575	constcncfg 40084	. . . . . . . . . . . . . . . . . . . . . . . . 25
589	588	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . 24
590	589	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
591		reseq2 5391	. . . . . . . . . . . . . . . . . . . . . . . 24
592		resabs1 5427	. . . . . . . . . . . . . . . . . . . . . . . . . 26
593	167, 592	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25
594	593, 211	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . . . 24
595	591, 594	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23
596	559, 568	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . 24
597	596	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23
598	590, 595, 597	3eltr4d 2716	. . . . . . . . . . . . . . . . . . . . . 22
599	558, 598	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
600	587, 599	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . 20
601	600	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
602	334, 340, 532, 573, 601	cncfuni 40099	. . . . . . . . . . . . . . . . . 18
603	602	trud 1493	. . . . . . . . . . . . . . . . 17
604		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . 23
605	604	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . 22
606		iooss2 12211	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
607	374, 451, 606	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . 23
608		resabs2 5429	. . . . . . . . . . . . . . . . . . . . . . 23
609	607, 608	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
610	605, 609	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21
611		id 22	. . . . . . . . . . . . . . . . . . . . 21
612	610, 611	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 lim lim
613	252	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
614	311, 392, 393, 613	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . . 24 lim
615	614	trud 1493	. . . . . . . . . . . . . . . . . . . . . . 23 lim
616	309	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . 24 lim lim
617	335	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
618	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
619	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
620	164	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
621	315	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
622	236	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
623	617, 618, 619, 620, 621, 471, 622	limcresioolb 39875	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim lim
624	623	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . 24 lim lim
625	616, 624	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . 23 lim lim
626	615, 625	eleqtri 2699	. . . . . . . . . . . . . . . . . . . . . 22 lim
627	626	ne0ii 3923	. . . . . . . . . . . . . . . . . . . . 21 lim
628	627	a1i 11	. . . . . . . . . . . . . . . . . . . 20 lim
629	612, 628	eqnetrd 2861	. . . . . . . . . . . . . . . . . . 19 lim
630	629	adantl 482	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ lim
631		eldifi 3732	. . . . . . . . . . . . . . . . . . . . 21 $\$
632	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
633	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
634		icossre 12254	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
635	158, 153, 634	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . 24
636	635	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . 23
637	636	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
638	158	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
639		icogelb 12225	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
640	159, 153, 639	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . 24
641	640	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
642		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . 24
643	642	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
644	638, 637, 641, 643	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
645		icoltub 39732	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
646	159, 153, 645	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . 23
647	646	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
648	632, 633, 637, 644, 647	eliood 39720	. . . . . . . . . . . . . . . . . . . . 21 $/\$
649	631, 648	sylan 488	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
650		eldifn 3733	. . . . . . . . . . . . . . . . . . . . 21 $\$
651	650	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
652	649, 651	eldifd 3585	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$
653		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
654	653	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . 21
655	654, 358	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 lim lim
656	213, 446, 393, 393	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . . 24 lim
657	656	trud 1493	. . . . . . . . . . . . . . . . . . . . . . 23 lim
658		resres 5409	. . . . . . . . . . . . . . . . . . . . . . . . 25
659		iooin 12209	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
660	159, 153, 151, 374, 659	mp4an 709	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
661	165	iftruei 4093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
662	451	iftruei 4093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
663	661, 662	oveq12i 6662	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
664	660, 663	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . 26
665	664	reseq2i 5393	. . . . . . . . . . . . . . . . . . . . . . . . 25
666	211	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . 25
667	658, 665, 666	3eqtrri 2649	. . . . . . . . . . . . . . . . . . . . . . . 24
668	667	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . 23 lim lim
669	657, 668	eleqtri 2699	. . . . . . . . . . . . . . . . . . . . . 22 lim
670	669	ne0ii 3923	. . . . . . . . . . . . . . . . . . . . 21 lim
671	670	a1i 11	. . . . . . . . . . . . . . . . . . . 20 lim
672	655, 671	eqnetrd 2861	. . . . . . . . . . . . . . . . . . 19 lim
673	652, 324, 672	3syl 18	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ lim
674	630, 673	pm2.61dan 832	. . . . . . . . . . . . . . . . 17 $\$ lim
675		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . 23
676	675	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . 22
677		id 22	. . . . . . . . . . . . . . . . . . . . . 22
678	676, 677	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . 21 lim lim
679		iooss1 12210	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
680	363, 387, 679	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . 23
681		resabs2 5429	. . . . . . . . . . . . . . . . . . . . . . 23
682	680, 681	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
683	682	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . 21 lim lim
684	678, 683	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20 lim lim
685	213, 446, 393, 53	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . . 24 lim
686	685	trud 1493	. . . . . . . . . . . . . . . . . . . . . . 23 lim
687	211	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . 24 lim lim
688	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
689	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
690	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
691	165	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
692	617, 619, 688, 689, 690, 412, 691	limcresiooub 39874	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim lim
693	692	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . 24 lim lim
694	687, 693	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . 23 lim lim
695	686, 694	eleqtri 2699	. . . . . . . . . . . . . . . . . . . . . 22 lim
696	695	ne0ii 3923	. . . . . . . . . . . . . . . . . . . . 21 lim
697	696	a1i 11	. . . . . . . . . . . . . . . . . . . 20 lim
698	684, 697	eqnetrd 2861	. . . . . . . . . . . . . . . . . . 19 lim
699	698	adantl 482	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ lim
700	159	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
701	153	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
702		negpitopissre 24286	. . . . . . . . . . . . . . . . . . . . . . 23
703		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
704	702, 703	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . 22 $\$
705	704	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
706	159	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
707	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
708		iocgtlb 39724	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
709	706, 707, 703, 708	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 22 $\$
710	709	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
711	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
712		iocleub 39725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
713	706, 707, 703, 712	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
714	713	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
715		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25
716	715	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24
717	716	necon3bi 2820	. . . . . . . . . . . . . . . . . . . . . . 23
718	717	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
719	705, 711, 714, 718	leneltd 10191	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$
720	700, 701, 705, 710, 719	eliood 39720	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
721		eldifn 3733	. . . . . . . . . . . . . . . . . . . . 21 $\$
722	721	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
723	720, 722	eldifd 3585	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$
724		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . 22
725	724	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . 21
726	725, 358	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20 lim lim
727	311, 392, 393, 393	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . . 24 lim
728	727	trud 1493	. . . . . . . . . . . . . . . . . . . . . . 23 lim
729		resres 5409	. . . . . . . . . . . . . . . . . . . . . . . . 25
730		iooin 12209	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
731	159, 153, 363, 151, 730	mp4an 709	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
732		mnflt 11957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
733	158, 732	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
734		xrltnle 10105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
735	363, 159, 734	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
736	733, 735	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
737	736	iffalsei 4096	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
738		xrltnle 10105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
739	151, 153, 738	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
740	68, 739	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
741	740	iffalsei 4096	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
742	737, 741	oveq12i 6662	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
743	731, 742	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . 26
744	743	reseq2i 5393	. . . . . . . . . . . . . . . . . . . . . . . . 25
745	309	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . 25
746	729, 744, 745	3eqtrri 2649	. . . . . . . . . . . . . . . . . . . . . . . 24
747	746	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . 23 lim lim
748	728, 747	eleqtri 2699	. . . . . . . . . . . . . . . . . . . . . 22 lim
749	748	ne0ii 3923	. . . . . . . . . . . . . . . . . . . . 21 lim
750	749	a1i 11	. . . . . . . . . . . . . . . . . . . 20 lim
751	726, 750	eqnetrd 2861	. . . . . . . . . . . . . . . . . . 19 lim
752	723, 324, 751	3syl 18	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ lim
753	699, 752	pm2.61dan 832	. . . . . . . . . . . . . . . . 17 $\$ lim
754		eqid 2622	. . . . . . . . . . . . . . . . . . . 20
755		ioosscn 39716	. . . . . . . . . . . . . . . . . . . . 21
756	755	a1i 11	. . . . . . . . . . . . . . . . . . . 20
757		1cnd 10056	. . . . . . . . . . . . . . . . . . . 20
758	23	a1i 11	. . . . . . . . . . . . . . . . . . . 20
759	754, 756, 757, 758	constlimc 39856	. . . . . . . . . . . . . . . . . . 19 lim
760		ioossioc 39713	. . . . . . . . . . . . . . . . . . . . 21
761	760	sseli 3599	. . . . . . . . . . . . . . . . . . . 20
762	761	iftrued 4094	. . . . . . . . . . . . . . . . . . 19
763	208	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
764		modcl 12672	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
765	22, 133, 764	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . 24
766	22, 765	resubcli 10343	. . . . . . . . . . . . . . . . . . . . . . 23
767	766	rexri 10097	. . . . . . . . . . . . . . . . . . . . . 22
768	767	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
769	22	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
770		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . 23
771		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
772	151, 153, 771	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . 23
773	770, 772	elrpd 11869	. . . . . . . . . . . . . . . . . . . . . 22
774	769, 773	ltsubrpd 11904	. . . . . . . . . . . . . . . . . . . . 21
775		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . 22
776	775	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
777	363	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
778		mnflt 11957	. . . . . . . . . . . . . . . . . . . . . . 23
779		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
780	363, 767, 779	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . 23
781	766, 778, 780	mp2b 10	. . . . . . . . . . . . . . . . . . . . . 22
782	781	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
783	763, 768, 769, 774, 776, 777, 782	limcresiooub 39874	. . . . . . . . . . . . . . . . . . . 20 lim lim
784		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
785	151, 153, 784	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . 22
786	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
787	775	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
788	786, 787	feqresmpt 6250	. . . . . . . . . . . . . . . . . . . . . . 23
789		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
790	789, 107, 145	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . 26
791	790	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
792	789	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
793	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
794	792, 793	modcld 12674	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
795	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
796	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
797	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
798	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
799		ioossico 12262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
800	799	sseli 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
801	797, 798, 800	ltmod 39870	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
802	801	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
803		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
804	794, 795, 796, 802, 803	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
805	804	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
806	791, 805	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
807	806	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . 23
808	788, 807	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . 22
809	785, 808	syl 17	. . . . . . . . . . . . . . . . . . . . 21
810	809	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 lim lim
811	783, 810	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19 lim lim
812	759, 762, 811	3eltr4d 2716	. . . . . . . . . . . . . . . . . 18 lim
813		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
814		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . . . 26
815	814	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
816	815, 206	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . 24
817	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
818	813, 816, 304, 817	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . 23 lim
819	818	trud 1493	. . . . . . . . . . . . . . . . . . . . . 22 lim
820	819	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 lim
821		id 22	. . . . . . . . . . . . . . . . . . . . . . 23
822		lbioc 39739	. . . . . . . . . . . . . . . . . . . . . . . 24
823	822	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
824	821, 823	eqneltrd 2720	. . . . . . . . . . . . . . . . . . . . . 22
825	824	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . 21
826	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
827	814	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
828	826, 827	feqresmpt 6250	. . . . . . . . . . . . . . . . . . . . . . . 24
829	827	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
830	829, 107, 145	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
831	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
832	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
833	829, 832	modcld 12674	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
834	22, 118	resubcli 10343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
835	834	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
836	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
837	835, 836	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
838		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
839	838, 836	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
840	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
841	834	rexri 10097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
842	841	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
843	840	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
844		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
845		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
846	842, 843, 844, 845	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
847	835, 838, 836, 846	ltadd1dd 10638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
848	837, 839, 840, 847	ltsub1dd 10639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
849	848	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
850	250	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
851	52, 52	addcli 10044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
852		subadd23 10293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
853	23, 52, 851, 852	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
854	52, 52	pncan3oi 10297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
855	854	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
856	850, 853, 855	3eqtri 2648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
857	856	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
858		pncan2 10288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
859	23, 52, 858	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
860	857, 859	eqtr2i 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
861	860	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
862	839, 840	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
863		modabs2 12704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
864	862, 133, 863	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
865	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
866		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
867	837, 840	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
868	68, 860	breqtri 4678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
869	868	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
870	866, 867, 862, 869, 848	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
871	866, 862, 870	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
872	840, 836	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
873		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
874	842, 843, 844, 873	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
875	838, 840, 836, 874	ltadd1dd 10638	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
876	839, 872, 840, 875	ltsub1dd 10639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
877		pncan2 10288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
878	23, 121, 877	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
879	876, 878	syl6breq 4694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
880		modid 12695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
881	862, 865, 871, 879, 880	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
882	864, 881	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
883	882	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
884		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
885	884	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
886	862, 865	modcld 12674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
887	886	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
888	887	addid1d 10236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
889	888	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
890	885, 889	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
891	890	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
892		modaddabs 12708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
893	862, 840, 865, 892	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
894	893	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
895	883, 891, 894	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
896	143	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
897	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
898	896, 897	npcand 10396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
899	122	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
900	899	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
901	898, 900	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
902	901	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
903	838, 902	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
904	903	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
905		1zzd 11408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
906	829, 832, 905, 136	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
907	895, 904, 906	3eqtrrd 2661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
908	849, 861, 907	3brtr4d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
909	831, 833, 908	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
910	831, 833, 909	lensymd 10188	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
911	910	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
912	830, 911	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
913	912	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . 24
914	828, 913	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . 23
915	914	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22 lim lim
916	841	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
917	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
918		ltsubrp 11866	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
919	22, 182, 918	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . 25
920	919	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
921		mnflt 11957	. . . . . . . . . . . . . . . . . . . . . . . . . 26
922		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
923	363, 841, 922	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . 26
924	834, 921, 923	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . 25
925	924	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
926	361, 916, 917, 920, 815, 364, 925	limcresiooub 39874	. . . . . . . . . . . . . . . . . . . . . . 23 lim lim
927	926	trud 1493	. . . . . . . . . . . . . . . . . . . . . 22 lim lim
928	915, 927	syl6req 2673	. . . . . . . . . . . . . . . . . . . . 21 lim lim
929	820, 825, 928	3eltr4d 2716	. . . . . . . . . . . . . . . . . . . 20 lim
930	929	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$ lim
931	153	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
932	120	rexri 10097	. . . . . . . . . . . . . . . . . . . . . 22
933	932	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
934	765	rexri 10097	. . . . . . . . . . . . . . . . . . . . . 22
935	934	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
936	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
937	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
938		pm4.56 516	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
939	938	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\/$
940		olc 399	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
941	940	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
942	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
943	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
944	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
945		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
946	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
947		modge0 12678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
948	22, 133, 947	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
949	948	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
950		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
951	945, 946, 949, 950	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
952	951	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
953		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
954	942, 943, 944, 952, 953	eliood 39720	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
955	954	orcd 407	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
956	941, 955	pm2.61dane 2881	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
957	939, 956	nsyl 135	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
958	936, 937, 957	nltled 10187	. . . . . . . . . . . . . . . . . . . . 21 $/\$
959		modlt 12679	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
960	22, 133, 959	mp2an 708	. . . . . . . . . . . . . . . . . . . . . 22
961	960	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 $/\$
962	931, 933, 935, 958, 961	elicod 12224	. . . . . . . . . . . . . . . . . . . 20 $/\$
963		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . 26
964	963, 816, 202, 817	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim
965	964	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . 24 lim
966	965	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 lim
967		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25
968		ubioc1 12227	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
969	151, 153, 68, 968	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . 25
970	967, 969	syl6eqel 2709	. . . . . . . . . . . . . . . . . . . . . . . 24
971	970	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . 23
972	361, 815	feqresmpt 6250	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
973	972	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . . 26
974	838, 107, 145	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
975	974	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
976		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
977	967	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
978	977	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
979	978	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
980	979	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
981	976, 980	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
982	981, 801	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
983		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
984	982, 983	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
985	984	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
986	975, 985	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
987	986	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . 26
988	973, 987	syl5req 2669	. . . . . . . . . . . . . . . . . . . . . . . . 25
989	988	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 lim lim
990	989, 927	syl6req 2673	. . . . . . . . . . . . . . . . . . . . . . 23 lim lim
991	966, 971, 990	3eltr4d 2716	. . . . . . . . . . . . . . . . . . . . . 22 lim
992	991	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ lim
993	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
994	932	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
995	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
996	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
997		icogelb 12225	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
998	153, 932, 997	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . 25
999	998	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
1000		neqne 2802	. . . . . . . . . . . . . . . . . . . . . . . . 25
1001	1000	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
1002	996, 995, 999, 1001	leneltd 10191	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
1003	960	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
1004	993, 994, 995, 1002, 1003	eliood 39720	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
1005		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
1006		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . . . 26
1007	1006	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1008	1007, 206	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . . 24
1009		neg1cn 11124	. . . . . . . . . . . . . . . . . . . . . . . . 25
1010	1009	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
1011	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
1012	1005, 1008, 1010, 1011	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . . 23 lim
1013	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1014	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1015	934	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1016		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
1017	153, 932, 1016	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . 25
1018	1013, 1014, 1015, 1017	gtnelioc 39712	. . . . . . . . . . . . . . . . . . . . . . . 24
1019	1018	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . 23
1020	1006	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1021	361, 1020	feqresmpt 6250	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
1022	1021	trud 1493	. . . . . . . . . . . . . . . . . . . . . . . . . 26
1023		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1024	1023, 107, 145	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1025	1024	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
1026	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
1027	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1028	1023, 1027	modcld 12674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1029	1028	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
1030	22, 118	readdcli 10053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1031	1030	recni 10052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1032	1031	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1033	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1034	765	recni 10052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1035	1034	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1036	1032, 1033, 1035	nnncan2d 10427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1037	1036, 859	syl6req 2673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1038	1030, 765	resubcli 10343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1039	1038	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1040	766	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1041	1038	rexri 10097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1042	1041	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1043	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1044	1043	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1045		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1046		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
1047	1042, 1044, 1045, 1046	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1048	1039, 1023, 1040, 1047	ltsub1dd 10639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1049	1037, 1048	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1050	1023	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1051		sub31 39503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
1052	1050, 1033, 1035, 1051	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1053	1049, 1052	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1054	1053	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
1055	1043, 1023	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1056		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1057		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
1058	1042, 1044, 1045, 1057	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
1059	1023, 1043	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
1060	1058, 1059	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1061	1056, 1055, 1060	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1062	1043, 1039	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1063	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1064	1039, 1023, 1043, 1047	ltsub2dd 10640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1065		sub31 39503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
1066	23, 1031, 1034, 1065	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
1067	859	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
1068	1066, 1067	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
1069		ltsubrp 11866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
1070	765, 182, 1069	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
1071	765, 118	resubcli 10343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
1072	1071, 765, 120	lttri 10163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
1073	1070, 960, 1072	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
1074	1068, 1073	eqbrtri 4674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
1075	1074	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1076	1055, 1062, 1063, 1064, 1075	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1077		modid 12695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$
1078	1055, 1027, 1061, 1076, 1077	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1079	1078	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1080	1079	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1081	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1082	1081, 1055	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1083	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1084	1052, 1082	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1085	68	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1086	1056, 1083, 1084, 1085, 1049	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1087	1086, 1052	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1088	1056, 1082, 1087	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1089	1043, 1040	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1090	1023, 1043, 1040, 1058	ltsub1dd 10639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1091		nncan 10310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
1092	23, 1034, 1091	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
1093	1092, 960	eqbrtri 4674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1094	1093	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1095	1084, 1089, 1063, 1090, 1094	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1096	1052, 1095	eqbrtrrd 4677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1097		modid 12695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$
1098	1082, 1027, 1088, 1096, 1097	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1099	1080, 1098	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1100		modsubmodmod 12729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
1101	1043, 1055, 1027, 1100	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1102	1033, 1050	nncand 10397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1103	1102	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1104	1099, 1101, 1103	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1105	1104	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
1106	1054, 1105	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
1107	1017, 1106	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
1108	1026, 1029, 1107	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
1109	1026, 1029, 1108	lensymd 10188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
1110	1109	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
1111	1025, 1110	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
1112	1111	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . . . . 26
1113	1022, 1112	syl5req 2669	. . . . . . . . . . . . . . . . . . . . . . . . 25
1114	1113	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . 24 lim lim
1115	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1116	1041	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1117	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1118		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
1119		ltaddsublt 10654	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
1120	1117, 1014, 1118, 1119	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26
1121	1017, 1120	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25
1122	363	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1123		mnflt 11957	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
1124		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
1125	363, 1041, 1124	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
1126	1038, 1123, 1125	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26
1127	1126	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1128	1115, 1116, 1117, 1121, 1007, 1122, 1127	limcresiooub 39874	. . . . . . . . . . . . . . . . . . . . . . . 24 lim lim
1129	1114, 1128	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . 23 lim lim
1130	1012, 1019, 1129	3eltr4d 2716	. . . . . . . . . . . . . . . . . . . . . 22 lim
1131	1004, 1130	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ lim
1132	992, 1131	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . 20 lim
1133	962, 1132	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ lim
1134	930, 1133	pm2.61dan 832	. . . . . . . . . . . . . . . . . 18 lim
1135	812, 1134	pm2.61i 176	. . . . . . . . . . . . . . . . 17 lim
1136		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22
1137		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . 24
1138	1137	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
1139	1138, 206	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . 22
1140	1136, 1139, 202, 817	constlimc 39856	. . . . . . . . . . . . . . . . . . . . 21 lim
1141	1140	trud 1493	. . . . . . . . . . . . . . . . . . . 20 lim
1142	1141	a1i 11	. . . . . . . . . . . . . . . . . . 19 lim
1143	104	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
1144		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24
1145	1144	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . 23
1146	1145	ifbid 4108	. . . . . . . . . . . . . . . . . . . . . 22
1147	1146	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1148	22	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
1149	105, 106	keepel 4155	. . . . . . . . . . . . . . . . . . . . . 22
1150	1149	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
1151	1143, 1147, 1148, 1150	fvmptd 6288	. . . . . . . . . . . . . . . . . . . 20
1152		icoltub 39732	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
1153	151, 153, 1152	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . 21
1154	1153	iftrued 4094	. . . . . . . . . . . . . . . . . . . 20
1155	1151, 1154	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19
1156	361, 1138	feqresmpt 6250	. . . . . . . . . . . . . . . . . . . . . . 23
1157	1156	trud 1493	. . . . . . . . . . . . . . . . . . . . . 22
1158		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . 26
1159	1158, 107, 145	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . 25
1160	1159	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
1161	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1162	1158, 1161	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1163	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1164		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1165	1161	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1166	118, 765	resubcli 10343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1167	22, 1166	readdcli 10053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1168	1167	rexri 10097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1169	1168	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1170		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1171		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
1172	1165, 1169, 1170, 1171	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1173	1161, 1158	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1174	1172, 1173	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1175	1164, 1162, 1174	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1176	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1177	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1178	1167	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1179	1178, 1161	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1180		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
1181	1165, 1169, 1170, 1180	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1182	1158, 1178, 1161, 1181	ltsub1dd 10639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1183	1166	recni 10052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1184		pncan2 10288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
1185	23, 1183, 1184	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1186		subge02 10544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
1187	118, 765, 1186	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1188	948, 1187	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1189	1185, 1188	eqbrtri 4674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1190	1189	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1191	1162, 1179, 1176, 1182, 1190	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1192	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1193	1162, 1176, 1177, 1191, 1192	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1194		modid 12695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
1195	1162, 1163, 1175, 1193, 1194	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1196	1195	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1197	1196	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1198	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1199	1198, 1162	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1200	1161, 1161	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1201	1198, 1200	readdcld 10069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1202	23	subidi 10352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1203	1202	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1204	1034	addid1i 10223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1205	1203, 1204	eqtr2i 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1206	948, 1205	breqtri 4678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1207	1206	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1208	1161, 1158, 1161, 1172	ltsub1dd 10639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1209	1200, 1162, 1198, 1208	ltadd2dd 10196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1210	1164, 1201, 1199, 1207, 1209	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1211	1164, 1199, 1210	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1212	1162, 1179, 1198, 1182	ltadd2dd 10196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1213	1185	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1214	1034, 52	pncan3i 10358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1215	1213, 1214	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1216	1212, 1215	syl6breq 4694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1217	1199, 1176, 1177, 1216, 1192	lttrd 10198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1218		modid 12695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
1219	1199, 1163, 1211, 1217, 1218	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1220	1197, 1219	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1221		modaddabs 12708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
1222	1161, 1162, 1163, 1221	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1223	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1224	1158	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1225	1223, 1224	pncan3d 10395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1226	1225	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1227	1220, 1222, 1226	3eqtrrd 2661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1228	1227	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
1229	1216	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
1230	1228, 1229	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
1231	1153, 1230	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
1232	1231	iftrued 4094	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
1233	1160, 1232	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
1234	1233	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . 22
1235	1157, 1234	syl5req 2669	. . . . . . . . . . . . . . . . . . . . 21
1236	1235	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20 lim lim
1237	208	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
1238	1168	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
1239	1166	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
1240	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1241	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1242	1240, 1241	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . . . 24
1243	1153, 1242	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23
1244	1239, 1243	elrpd 11869	. . . . . . . . . . . . . . . . . . . . . 22
1245	1148, 1244	ltaddrpd 11905	. . . . . . . . . . . . . . . . . . . . 21
1246	1137	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
1247	374	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
1248		ltpnf 11954	. . . . . . . . . . . . . . . . . . . . . . 23
1249		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
1250	1168, 374, 1249	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . 23
1251	1167, 1248, 1250	mp2b 10	. . . . . . . . . . . . . . . . . . . . . 22
1252	1251	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
1253	1237, 1148, 1238, 1245, 1246, 1247, 1252	limcresioolb 39875	. . . . . . . . . . . . . . . . . . . 20 lim lim
1254	1236, 1253	eqtr2d 2657	. . . . . . . . . . . . . . . . . . 19 lim lim
1255	1142, 1155, 1254	3eltr4d 2716	. . . . . . . . . . . . . . . . . 18 lim
1256	153	a1i 11	. . . . . . . . . . . . . . . . . . . 20
1257	932	a1i 11	. . . . . . . . . . . . . . . . . . . 20
1258	934	a1i 11	. . . . . . . . . . . . . . . . . . . 20
1259	151	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
1260	153	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
1261	934	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
1262	948	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
1263	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1264	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1265	1263, 1264	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . 24
1266	1265	ibir 257	. . . . . . . . . . . . . . . . . . . . . . 23
1267	1266	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
1268	1259, 1260, 1261, 1262, 1267	elicod 12224	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1269		simpl 473	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1270	1268, 1269	condan 835	. . . . . . . . . . . . . . . . . . . 20
1271	960	a1i 11	. . . . . . . . . . . . . . . . . . . 20
1272	1256, 1257, 1258, 1270, 1271	elicod 12224	. . . . . . . . . . . . . . . . . . 19
1273		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23
1274		ioossre 12235	. . . . . . . . . . . . . . . . . . . . . . . . 25
1275	1274	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
1276	1275, 206	syl6ss 3615	. . . . . . . . . . . . . . . . . . . . . . 23
1277	1273, 1276, 304, 817	constlimc 39856	. . . . . . . . . . . . . . . . . . . . . 22 lim
1278	1277	trud 1493	. . . . . . . . . . . . . . . . . . . . 21 lim
1279	1278	a1i 11	. . . . . . . . . . . . . . . . . . . 20 lim
1280		1ex 10035	. . . . . . . . . . . . . . . . . . . . . . . . 25
1281	106	elexi 3213	. . . . . . . . . . . . . . . . . . . . . . . . 25
1282	1280, 1281	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . 24
1283	1146, 104, 1282	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . . 23
1284	22, 1283	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
1285	1284	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
1286	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
1287	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
1288	1286, 1287, 998	lensymd 10188	. . . . . . . . . . . . . . . . . . . . . 22
1289	1288	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . 21
1290	1285, 1289	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20
1291	361, 1275	feqresmpt 6250	. . . . . . . . . . . . . . . . . . . . . . . 24
1292	1291	trud 1493	. . . . . . . . . . . . . . . . . . . . . . 23
1293		elioore 12205	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
1294	1293, 107, 145	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . 26
1295	1294	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
1296	118	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
1297	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1298	1293, 1297	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1299	133	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1300		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1301	1297	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1302	120, 765	resubcli 10343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
1303	22, 1302	readdcli 10053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
1304	1303	rexri 10097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1305	1304	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1306		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1307		ioogtlb 39717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
1308	1301, 1305, 1306, 1307	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1309	1297, 1293	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1310	1308, 1309	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1311	1300, 1298, 1310	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1312	1303	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1313	1312, 1297	resubcld 10458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1314	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1315		iooltub 39735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
1316	1301, 1305, 1306, 1315	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1317	1293, 1312, 1297, 1316	ltsub1dd 10639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1318	1302	recni 10052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1319		pncan2 10288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
1320	23, 1318, 1319	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1321		subge02 10544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
1322	120, 765, 1321	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1323	948, 1322	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
1324	1320, 1323	eqbrtri 4674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1325	1324	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
1326	1298, 1313, 1314, 1317, 1325	ltletrd 10197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1327	1298, 1299, 1311, 1326, 1194	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1328	1327	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1329	1328	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1330		readdcl 10019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
1331	765, 1298, 1330	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1332	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1333	948	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1334	1332, 1298, 1333, 1310	addgegt0d 10601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1335	1300, 1331, 1334	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1336	1298, 1313, 1332, 1317	ltadd2dd 10196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1337	1320	oveq2i 6661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1338	1034, 121	pncan3i 10358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
1339	1337, 1338	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
1340	1336, 1339	syl6breq 4694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1341	1331, 1299, 1335, 1340, 1218	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1342	1329, 1341	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1343	1297, 1298, 1299, 1221	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1344	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1345	1293	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1346	1344, 1345	pncan3d 10395	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1347	1346	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1348	1342, 1343, 1347	3eqtrd 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1349	1348	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
1350	1331	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
1351	1349, 1350	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
1352	765	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
1353	998	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
1354	1298, 1310	elrpd 11869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1355	1332, 1354	ltaddrpd 11905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1356	1355	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
1357	1296, 1352, 1350, 1353, 1356	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
1358	1296, 1350, 1357	ltled 10185	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
1359	1358, 1349	breqtrd 4679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
1360	1296, 1351, 1359	lensymd 10188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
1361	1360	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
1362	1295, 1361	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
1363	1362	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . . . . . 23
1364	1292, 1363	syl5req 2669	. . . . . . . . . . . . . . . . . . . . . 22
1365	1364	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 lim lim
1366	208	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
1367	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
1368	1304	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
1369	1302	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
1370	960	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
1371	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
1372	1287, 1371	posdifd 10614	. . . . . . . . . . . . . . . . . . . . . . . . 25
1373	1370, 1372	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . 24
1374	1369, 1373	elrpd 11869	. . . . . . . . . . . . . . . . . . . . . . 23
1375	1367, 1374	ltaddrpd 11905	. . . . . . . . . . . . . . . . . . . . . 22
1376	1274	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
1377	374	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
1378		ltpnf 11954	. . . . . . . . . . . . . . . . . . . . . . . 24
1379		xrltle 11982	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
1380	1304, 374, 1379	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . 24
1381	1303, 1378, 1380	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . 23
1382	1381	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
1383	1366, 1367, 1368, 1375, 1376, 1377, 1382	limcresioolb 39875	. . . . . . . . . . . . . . . . . . . . 21 lim lim
1384	1365, 1383	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . 20 lim lim
1385	1279, 1290, 1384	3eltr4d 2716	. . . . . . . . . . . . . . . . . . 19 lim
1386	1272, 1385	syl 17	. . . . . . . . . . . . . . . . . 18 lim
1387	1255, 1386	pm2.61i 176	. . . . . . . . . . . . . . . . 17 lim
1388		id 22	. . . . . . . . . . . . . . . . . . . 20
1389	110, 104, 1388	sqwvfoura 40445	. . . . . . . . . . . . . . . . . . 19
1390	1389	eqcomd 2628	. . . . . . . . . . . . . . . . . 18
1391	1390	mpteq2ia 4740	. . . . . . . . . . . . . . . . 17
1392		id 22	. . . . . . . . . . . . . . . . . . . 20
1393	110, 104, 1392	sqwvfourb 40446	. . . . . . . . . . . . . . . . . . 19
1394	1393	eqcomd 2628	. . . . . . . . . . . . . . . . . 18
1395	1394	mpteq2ia 4740	. . . . . . . . . . . . . . . . 17
1396		nnnn0 11299	. . . . . . . . . . . . . . . . . . . . . . 23
1397		0red 10041	. . . . . . . . . . . . . . . . . . . . . . 23
1398		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
1399	1398	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
1400	1396, 1397, 1399	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22
1401	1400	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21
1402	74	coscld 14861	. . . . . . . . . . . . . . . . . . . . . 22
1403	1402	mul02d 10234	. . . . . . . . . . . . . . . . . . . . 21
1404	1401, 1403	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20
1405		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . 23
1406	89, 1405	ifex 4156	. . . . . . . . . . . . . . . . . . . . . 22
1407		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23
1408	1407	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
1409	1406, 1408	mpan2 707	. . . . . . . . . . . . . . . . . . . . 21
1410	1409	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20
1411	1404, 1410	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19
1412	60, 72	ifcld 4131	. . . . . . . . . . . . . . . . . . . . 21
1413	1412, 75	mulcld 10060	. . . . . . . . . . . . . . . . . . . 20
1414	1413	addid2d 10237	. . . . . . . . . . . . . . . . . . 19
1415		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . 23
1416	1415	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22
1417	75	mul02d 10234	. . . . . . . . . . . . . . . . . . . . . 22
1418	1416, 1417	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1419		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . 23
1420	1419	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22
1421	1420	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1422	1418, 1421	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 $/\$
1423		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . 23
1424	1423	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22
1425	1424	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1426		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . 23
1427	1426	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22
1428	1427	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$
1429	1425, 1428	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 $/\$
1430	1422, 1429	pm2.61dan 832	. . . . . . . . . . . . . . . . . . 19
1431	1411, 1414, 1430	3eqtrrd 2661	. . . . . . . . . . . . . . . . . 18
1432	1431	mpteq2ia 4740	. . . . . . . . . . . . . . . . 17
1433	109, 110, 147, 148, 329, 603, 674, 753, 22, 1135, 1387, 1391, 1395, 1432	fourierclim 40441	. . . . . . . . . . . . . . . 16
1434		0nn0 11307	. . . . . . . . . . . . . . . . . . . . 21
1435		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . 22
1436	1435, 1398, 89	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . 21
1437	1434, 1436	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
1438	1437	oveq1i 6660	. . . . . . . . . . . . . . . . . . 19
1439	28	recni 10052	. . . . . . . . . . . . . . . . . . . 20
1440	67, 129	gtneii 10149	. . . . . . . . . . . . . . . . . . . 20
1441	1439, 1440	div0i 10759	. . . . . . . . . . . . . . . . . . 19
1442	1438, 1441	eqtri 2644	. . . . . . . . . . . . . . . . . 18
1443	1442	oveq2i 6661	. . . . . . . . . . . . . . . . 17
1444	202	trud 1493	. . . . . . . . . . . . . . . . . . . . 21
1445	1444, 1009	keepel 4155	. . . . . . . . . . . . . . . . . . . 20
1446	1149	recni 10052	. . . . . . . . . . . . . . . . . . . . 21
1447	1284, 1446	eqeltri 2697	. . . . . . . . . . . . . . . . . . . 20
1448	1445, 1447	addcli 10044	. . . . . . . . . . . . . . . . . . 19
1449	1448, 1439, 1440	divcli 10767	. . . . . . . . . . . . . . . . . 18
1450	1449	subid1i 10353	. . . . . . . . . . . . . . . . 17
1451	1443, 1450	eqtri 2644	. . . . . . . . . . . . . . . 16
1452	1433, 1451	breqtri 4678	. . . . . . . . . . . . . . 15
1453	1452	a1i 11	. . . . . . . . . . . . . 14
1454	79, 103, 1453	sumnnodd 39862	. . . . . . . . . . . . 13 $/\$
1455	1454	trud 1493	. . . . . . . . . . . 12 $/\$
1456	1455	simpli 474	. . . . . . . . . . 11
1457		breq2 4657	. . . . . . . . . . . . . . . . . 18
1458		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20
1459	1458	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
1460		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20
1461	1460	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
1462	1459, 1461	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
1463	1457, 1462	ifbieq2d 4111	. . . . . . . . . . . . . . . . 17
1464	1463	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
1465		elnnz 11387	. . . . . . . . . . . . . . . . 17 $/\$
1466	20, 48, 1465	sylanbrc 698	. . . . . . . . . . . . . . . 16
1467		ovex 6678	. . . . . . . . . . . . . . . . . 18
1468	89, 1467	ifex 4156	. . . . . . . . . . . . . . . . 17
1469	1468	a1i 11	. . . . . . . . . . . . . . . 16
1470	80, 1464, 1466, 1469	fvmptd 6288	. . . . . . . . . . . . . . 15
1471		dvdsmul1 15003	. . . . . . . . . . . . . . . . . . 19 $/\$
1472	15, 17, 1471	sylancr 695	. . . . . . . . . . . . . . . . . 18
1473	18	zcnd 11483	. . . . . . . . . . . . . . . . . . . 20
1474		1cnd 10056	. . . . . . . . . . . . . . . . . . . 20
1475	1473, 1474	npcand 10396	. . . . . . . . . . . . . . . . . . 19
1476	1475	eqcomd 2628	. . . . . . . . . . . . . . . . . 18
1477	1472, 1476	breqtrd 4679	. . . . . . . . . . . . . . . . 17
1478		oddp1even 15068	. . . . . . . . . . . . . . . . . 18
1479	20, 1478	syl 17	. . . . . . . . . . . . . . . . 17
1480	1477, 1479	mpbird 247	. . . . . . . . . . . . . . . 16
1481	1480	iffalsed 4097	. . . . . . . . . . . . . . 15
1482	52	a1i 11	. . . . . . . . . . . . . . . . . . . 20
1483	21, 1482	mulcomd 10061	. . . . . . . . . . . . . . . . . . 19
1484	1483	oveq2d 6666	. . . . . . . . . . . . . . . . . 18
1485	54	a1i 11	. . . . . . . . . . . . . . . . . . 19
1486	69	a1i 11	. . . . . . . . . . . . . . . . . . 19
1487	1485, 1482, 21, 1486, 49	divdiv1d 10832	. . . . . . . . . . . . . . . . . 18
1488	1484, 1487	eqtr4d 2659	. . . . . . . . . . . . . . . . 17
1489	1488	oveq1d 6665	. . . . . . . . . . . . . . . 16
1490	1485, 1482, 1486	divcld 10801	. . . . . . . . . . . . . . . . 17
1491	1490, 21, 26, 49	div32d 10824	. . . . . . . . . . . . . . . 16
1492	1489, 1491	eqtrd 2656	. . . . . . . . . . . . . . 15
1493	1470, 1481, 1492	3eqtrd 2660	. . . . . . . . . . . . . 14
1494	1493	mpteq2ia 4740	. . . . . . . . . . . . 13
1495		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
1496	1495	oveq1d 6665	. . . . . . . . . . . . . . . . . 18
1497	1496	oveq1d 6665	. . . . . . . . . . . . . . . . 17
1498	1497	fveq2d 6195	. . . . . . . . . . . . . . . 16
1499	1498, 1496	oveq12d 6668	. . . . . . . . . . . . . . 15
1500	1499	oveq2d 6666	. . . . . . . . . . . . . 14
1501	1500	cbvmptv 4750	. . . . . . . . . . . . 13
1502	1494, 1501	eqtri 2644	. . . . . . . . . . . 12
1503		seqeq3 12806	. . . . . . . . . . . 12
1504	1502, 1503	ax-mp 5	. . . . . . . . . . 11
1505		fouriersw.y	. . . . . . . . . . . . 13
1506	110, 104, 22, 1505	fourierswlem 40447	. . . . . . . . . . . 12
1507	1506	eqcomi 2631	. . . . . . . . . . 11
1508	1456, 1504, 1507	3brtr3i 4682	. . . . . . . . . 10
1509	1508	a1i 11	. . . . . . . . 9
1510		eqid 2622	. . . . . . . . . . . 12
1511	61, 65, 70	divcld 10801	. . . . . . . . . . . . 13
1512	1439	a1i 11	. . . . . . . . . . . . . . . . . 18
1513	1512, 62	mulcld 10060	. . . . . . . . . . . . . . . . 17
1514		id 22	. . . . . . . . . . . . . . . . . 18
1515		1cnd 10056	. . . . . . . . . . . . . . . . . 18
1516	1514, 1515	subcld 10392	. . . . . . . . . . . . . . . . 17
1517	1513, 1516	syl 17	. . . . . . . . . . . . . . . 16
1518	1517, 73	mulcld 10060	. . . . . . . . . . . . . . 15
1519	1518	sincld 14860	. . . . . . . . . . . . . 14
1520	28	a1i 11	. . . . . . . . . . . . . . . . 17
1521		nnre 11027	. . . . . . . . . . . . . . . . 17
1522	1520, 1521	remulcld 10070	. . . . . . . . . . . . . . . 16
1523	1522	recnd 10068	. . . . . . . . . . . . . . 15
1524		1cnd 10056	. . . . . . . . . . . . . . 15
1525	1523, 1524	subcld 10392	. . . . . . . . . . . . . 14
1526		1red 10055	. . . . . . . . . . . . . . . 16
1527	35, 1520	syl5eqel 2705	. . . . . . . . . . . . . . . . 17
1528		1lt2 11194	. . . . . . . . . . . . . . . . . . 19
1529	1528	a1i 11	. . . . . . . . . . . . . . . . . 18
1530	1529, 35	syl6breqr 4695	. . . . . . . . . . . . . . . . 17
1531	43	a1i 11	. . . . . . . . . . . . . . . . . 18
1532		nnge1 11046	. . . . . . . . . . . . . . . . . 18
1533	1526, 1521, 1520, 1531, 1532	lemul2ad 10964	. . . . . . . . . . . . . . . . 17
1534	1526, 1527, 1522, 1530, 1533	ltletrd 10197	. . . . . . . . . . . . . . . 16
1535	1526, 1534	gtned 10172	. . . . . . . . . . . . . . 15
1536	1523, 1524, 1535	subne0d 10401	. . . . . . . . . . . . . 14
1537	1519, 1525, 1536	divcld 10801	. . . . . . . . . . . . 13
1538	1511, 1537	mulcld 10060	. . . . . . . . . . . 12
1539	1510, 1538	fmpti 6383	. . . . . . . . . . 11
1540	1539	a1i 11	. . . . . . . . . 10
1541	1540	ffvelrnda 6359	. . . . . . . . 9 $/\$
1542		divcan6 10732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
1543	52, 69, 54, 56, 1542	mp4an 709	. . . . . . . . . . . . . 14
1544	1543	eqcomi 2631	. . . . . . . . . . . . 13
1545	1544	oveq1i 6660	. . . . . . . . . . . 12
1546	50	mulid2d 10058	. . . . . . . . . . . 12
1547	56	a1i 11	. . . . . . . . . . . . . 14
1548	1482, 1485, 1547	divcld 10801	. . . . . . . . . . . . 13
1549	1548, 1490, 50	mulassd 10063	. . . . . . . . . . . 12
1550	1545, 1546, 1549	3eqtr3a 2680	. . . . . . . . . . 11
1551		eqidd 2623	. . . . . . . . . . . . . 14
1552	8	oveq2d 6666	. . . . . . . . . . . . . . 15
1553	1552	adantl 482	. . . . . . . . . . . . . 14 $/\$
1554	1492, 1467	syl6eqelr 2710	. . . . . . . . . . . . . 14
1555	1551, 1553, 10, 1554	fvmptd 6288	. . . . . . . . . . . . 13
1556	1555	oveq2d 6666	. . . . . . . . . . . 12
1557	1556	eqcomd 2628	. . . . . . . . . . 11
1558	13, 1550, 1557	3eqtrd 2660	. . . . . . . . . 10
1559	1558	adantl 482	. . . . . . . . 9 $/\$
1560	1, 2, 58, 1509, 1541, 1559	isermulc2 14388	. . . . . . . 8
1561		climrel 14223	. . . . . . . . 9
1562	1561	releldmi 5362	. . . . . . . 8
1563	1560, 1562	syl 17	. . . . . . 7
1564	1, 2, 14, 51, 1563	isumclim2 14489	. . . . . 6
1565	1564	trud 1493	. . . . 5
1566	1560	trud 1493	. . . . 5
1567		climuni 14283	. . . . 5 $/\$
1568	1565, 1566, 1567	mp2an 708	. . . 4
1569	1568	oveq2i 6661	. . 3
1570	54, 52, 69	divcli 10767	. . . 4
1571	52, 54, 56	divcli 10767	. . . 4
1572	1284, 1149	eqeltri 2697	. . . . . . 7
1573	67, 1572	keepel 4155	. . . . . 6
1574	1505, 1573	eqeltri 2697	. . . . 5
1575	1574	recni 10052	. . . 4
1576	1570, 1571, 1575	mulassi 10049	. . 3
1577	1571, 1570, 1543	mulcomli 10047	. . . . 5
1578	1577	oveq1i 6660	. . . 4
1579	1575	mulid2i 10043	. . . 4
1580	1578, 1579	eqtri 2644	. . 3
1581	1569, 1576, 1580	3eqtr2i 2650	. 2
1582		fouriersw.z	. . . 4
1583		seqeq3 12806	. . . 4
1584	1582, 1583	ax-mp 5	. . 3
1585	1584, 1566	eqbrtri 4674	. 2
1586	1581, 1585	pm3.2i 471	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wtru 1484

wcel 1990

wne 2794

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

csn 4177

cpr 4179

cuni 4436 class class class wbr 4653

cmpt 4729

cdm 5114

crn 5115

cres 5116

wf 5884

cfv 5888 (class class class)co 6650

cfn 7955

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cpnf 10071

cmnf 10072

cxr 10073

clt 10074

cle 10075

cmin 10266

cneg 10267

cdiv 10684

cn 11020

c2 11070

c4 11072

cn0 11292

cz 11377

crp 11832

cioo 12175

cioc 12176

cico 12177

cmo 12668

cseq 12801

cli 14215

csu 14416

csin 14794

ccos 14795

cpi 14797

cdvds 14983 ↾_t crest 16081

ctopn 16082

ctg 16098 ℂ_fldccnfld 19746

ctop 20698

cnt 20821

clp 20938

ccnp 21029

ccncf 22679

citg 23387 lim

climc 23626

cdv 23627

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cc 9257 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-ofr 6898 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-omul 7565 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-acn 8768 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-xnn0 11364 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-sum 14417 df-ef 14798 df-sin 14800 df-cos 14801 df-pi 14803 df-dvds 14984 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-mulg 17541 df-cntz 17750 df-cmn 18195 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-t1 21118 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389 df-itg2 23390 df-ibl 23391 df-itg 23392 df-0p 23437 df-ditg 23611 df-limc 23630 df-dv 23631

This theorem is referenced by: (None)

W3C validator