limclner - Mathbox for Glauco Siliprandi

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

Theorem limclner 31516

Description: For a limit point, both from the left and from the right, of the domain, the limit of the function exits only if the left and the right limits are equal. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
limclner.k	ℂ_fld
limclner.a
limclner.j
limclner.f
limclner.blp1
limclner.blp2
limclner.l	lim
limclner.r	lim
limclner.lner

**Assertion**
Ref	Expression
limclner	lim

Proof of Theorem limclner Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		limclner.r	. . . . . . . . . . . . . 14 lim
2		limccl 22147	. . . . . . . . . . . . . . 15 lim
3	2	sseli 3505	. . . . . . . . . . . . . 14 lim
4	1, 3	syl 16	. . . . . . . . . . . . 13
5	4	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
6		limclner.l	. . . . . . . . . . . . . 14 lim
7		limccl 22147	. . . . . . . . . . . . . . 15 lim
8	7	sseli 3505	. . . . . . . . . . . . . 14 lim
9	6, 8	syl 16	. . . . . . . . . . . . 13
10	9	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
11	5, 10	subcld 9942	. . . . . . . . . . 11 $/\$ $/\$ $/\$
12		limclner.lner	. . . . . . . . . . . . . 14
13	12	necomd 2738	. . . . . . . . . . . . 13
14	13	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
15	5, 10, 14	subne0d 9951	. . . . . . . . . . 11 $/\$ $/\$ $/\$
16	11, 15	absrpcld 13259	. . . . . . . . . 10 $/\$ $/\$ $/\$
17		4re 10624	. . . . . . . . . . . 12
18		4pos 10643	. . . . . . . . . . . 12
19		elrp 11234	. . . . . . . . . . . 12 $/\$
20	17, 18, 19	mpbir2an 918	. . . . . . . . . . 11
21	20	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $/\$
22	16, 21	rpdivcld 11285	. . . . . . . . 9 $/\$ $/\$ $/\$
23		nfv 1683	. . . . . . . . . . . 12 $/\$
24		nfra1 2848	. . . . . . . . . . . 12 $/\$
25	23, 24	nfan 1875	. . . . . . . . . . 11 $/\$ $/\$ $/\$
26		nfv 1683	. . . . . . . . . . 11
27	25, 26	nfim 1867	. . . . . . . . . 10 $/\$ $/\$ $/\$
28		ovex 6320	. . . . . . . . . 10
29		eleq1 2539	. . . . . . . . . . . 12
30		oveq2 6303	. . . . . . . . . . . . . . 15
31	30	breq2d 4465	. . . . . . . . . . . . . 14
32	31	rexbidv 2978	. . . . . . . . . . . . 13
33	32	rexbidv 2978	. . . . . . . . . . . 12
34	29, 33	imbi12d 320	. . . . . . . . . . 11
35	34	imbi2d 316	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		simpll 753	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
37		simpr 461	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
38		rspa 2834	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
39	38	adantll 713	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
40		limclner.f	. . . . . . . . . . . . . . . . . . . . . . . 24
41		fresin 5760	. . . . . . . . . . . . . . . . . . . . . . . 24
42	40, 41	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23
43		inss2 3724	. . . . . . . . . . . . . . . . . . . . . . . . 25
44		ioosscn 31414	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43, 44	sstri 3518	. . . . . . . . . . . . . . . . . . . . . . . 24
46	45	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23
47		ax-resscn 9561	. . . . . . . . . . . . . . . . . . . . . . . . 25
48	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24
49		limclner.j	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
50		retop 21136	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
51	49, 50	eqeltri 2551	. . . . . . . . . . . . . . . . . . . . . . . . . 26
52		ioossre 11598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
53	43, 52	sstri 3518	. . . . . . . . . . . . . . . . . . . . . . . . . 26
54		uniretop 21137	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
55	49	unieqi 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
56	55	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
57	54, 56	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
58	57	lpss 19511	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
59	51, 53, 58	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . 25
60		limclner.blp1	. . . . . . . . . . . . . . . . . . . . . . . . 25
61	59, 60	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . 24
62	48, 61	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . 23
63	42, 46, 62	ellimc3 22151	. . . . . . . . . . . . . . . . . . . . . 22 lim $/\$ $/\$
64	6, 63	mpbid 210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
65	64	simprd 463	. . . . . . . . . . . . . . . . . . . 20 $/\$
66	65	r19.21bi 2836	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
67	66	3ad2ant1 1017	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
68		simp11l 1107	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		simp12 1027	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		simp2 997	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71		ifcl 3987	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
72	71	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
73		inss1 3723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
74	73	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
75		limclner.k	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ_fld
76	75	cnfldtop 21159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
78	53	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
79		unicntop 31336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ_fld
80	75	unieqi 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ℂ_fld
81	80	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ_fld
82	79, 81	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
83	75	tgioo2 21176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ↾_t
84	49, 83	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ↾_t
85	82, 84	restlp 19552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
86	77, 48, 78, 85	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
87	75	eqcomi 2480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ_fld
88	87	fveq2i 5875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
89	88	fveq1i 5873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
90	89	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld
91	86, 90	sseq12d 3538	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℂ_fld
92	74, 91	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℂ_fld
93	92, 60	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld
94	46, 62	islpcn 31504	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld $\$
95	93, 94	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
96	95	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $\$
97		breq2 4457	. . . . . . . . . . . . . . . . . . . . . . . . . 26
98	97	rexbidv 2978	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
99	98	rspcva 3217	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $\$
100	72, 96, 99	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
101		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
102	53	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
103		eldifi 3631	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
104	102, 103	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
105	104	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\$
106	48	sselda 3509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
107	62	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
108	106, 107	subcld 9942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
109	108	abscld 13247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
110	109	3ad2antl1 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
111	110	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
112	72	rpred 11268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
113	112	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
114	113	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
115		rpre 11238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
116	115	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
117	116	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
118		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
119	115	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
120		rpre 11238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121	120	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
122		min1 11401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
123	119, 121, 122	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
124	123	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
125	124	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
126	111, 114, 117, 118, 125	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
127	121	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
128	127	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
129		min2 11402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
130	119, 121, 129	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
131	130	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
132	131	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
133	111, 114, 128, 118, 132	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
134	126, 133	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
135	134	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
136	101, 105, 135	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$ $/\$
137	136	reximdva 2942	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$ $/\$
138	100, 137	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $/\$
139	68, 69, 70, 138	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
140		nfv 1683	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
141		nfre1 2928	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
142		inss1 3723	. . . . . . . . . . . . . . . . . . . . . . . . . 26
143	142, 103	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
144	143	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
145		simp113 1127	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
146		eldifsni 4159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
147	146	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $/\$
148		simprl 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $/\$
149	147, 148	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $/\$ $/\$
150	149	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
151		neeq1 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
152		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
153	152	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
154	153	breq1d 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
155	151, 154	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
156		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
157	156	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
158	157	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
159	158	breq1d 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
160	155, 159	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
161	160	rspcva 3217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
162	161	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
163	144, 145, 150, 162	syl21anc 1227	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
164	103	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
165	68	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
166		simp13 1028	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
167		nfv 1683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
168		nfra1 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
169	167, 168	nfan 1875	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
170	43	sseli 3505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
171		fvres 5886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
172	170, 171	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
173	172	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
174	173	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
175	174	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
176	175	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
177	176	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
178		simp3 998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
179		rspa 2834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
180	179	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
181	178, 180	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
182	181	3adant1l 1220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
183	177, 182	eqbrtrd 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
184	183	3exp 1195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
185	169, 184	ralrimi 2867	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
186	165, 166, 185	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
187	146	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $/\$
188	187	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $/\$ $/\$
189	188	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
190	153	breq1d 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
191	151, 190	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
192	156	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
193	192	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
194	193	breq1d 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
195	191, 194	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
196	195	rspcva 3217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
197	196	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
198	164, 186, 189, 197	syl21anc 1227	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
199	163, 198	jca 532	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
200		rspe 2925	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
201	144, 199, 200	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
202	201	3exp 1195	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
203	140, 141, 202	rexlimd 2951	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
204	139, 203	mpd 15	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
205	204	3exp 1195	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
206	205	rexlimdv 2957	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
207	67, 206	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
208	207	3exp 1195	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
209	208	rexlimdv 2957	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
210	209	imp 429	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
211	210	adantllr 718	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
212		fresin 5760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
213	40, 212	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
214		inss2 3724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
215		ioosscn 31414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
216	214, 215	sstri 3518	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
217	216	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
218	213, 217, 62	ellimc3 22151	. . . . . . . . . . . . . . . . . . . . . . . . . 26 lim $/\$ $/\$
219	1, 218	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
220	219	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
221	220	r19.21bi 2836	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
222	221	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
223		simp11l 1107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
224		simp12 1027	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
225		simp2 997	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
226		inss1 3723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
227	226	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
228		ioossre 11598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
229	214, 228	sstri 3518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
230	229	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
231	82, 84	restlp 19552	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
232	77, 48, 230, 231	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
233	88	fveq1i 5873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ℂ_fld
234	233	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ℂ_fld
235	232, 234	sseq12d 3538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ_fld
236	227, 235	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
237		limclner.blp2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
238	236, 237	sseldd 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
239	217, 62	islpcn 31504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld $\$
240	238, 239	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
241	240	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$
242		breq2 4457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
243	242	rexbidv 2978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
244	243	rspcva 3217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$ $\$
245	72, 241, 244	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
246		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
247		eldifi 3631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
248	229, 247	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$
249	248	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$
250	48	sselda 3509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
251	62	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
252	250, 251	subcld 9942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
253	252	abscld 13247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
254	253	3ad2antl1 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
255	254	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
256	112	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
257	116	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
258		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
259	124	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
260	255, 256, 257, 258, 259	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
261	127	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
262	257, 261, 129	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
263	255, 256, 261, 258, 262	ltletrd 9753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
264	260, 263	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
265	264	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
266	246, 249, 265	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $/\$
267	266	reximdva 2942	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $\$ $/\$
268	245, 267	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
269	223, 224, 225, 268	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
270		nfv 1683	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
271		nfre1 2928	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
272		inss1 3723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
273	272, 247	sseldi 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
274	273	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
275		simp113 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
276		eldifsni 4159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
277	276	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32