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 37025

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		limccl 22571	. . . . . . . . . . . . 13 lim
2		limclner.r	. . . . . . . . . . . . 13 lim
3	1, 2	sseldi 3440	. . . . . . . . . . . 12
4	3	ad2antrr 724	. . . . . . . . . . 11 $/\$ $/\$ $/\$
5		limccl 22571	. . . . . . . . . . . . 13 lim
6		limclner.l	. . . . . . . . . . . . 13 lim
7	5, 6	sseldi 3440	. . . . . . . . . . . 12
8	7	ad2antrr 724	. . . . . . . . . . 11 $/\$ $/\$ $/\$
9	4, 8	subcld 9967	. . . . . . . . . 10 $/\$ $/\$ $/\$
10		limclner.lner	. . . . . . . . . . . . 13
11	10	necomd 2674	. . . . . . . . . . . 12
12	11	ad2antrr 724	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13	4, 8, 12	subne0d 9976	. . . . . . . . . 10 $/\$ $/\$ $/\$
14	9, 13	absrpcld 13428	. . . . . . . . 9 $/\$ $/\$ $/\$
15		4re 10653	. . . . . . . . . . 11
16		4pos 10672	. . . . . . . . . . 11
17	15, 16	elrpii 11268	. . . . . . . . . 10
18	17	a1i 11	. . . . . . . . 9 $/\$ $/\$ $/\$
19	14, 18	rpdivcld 11321	. . . . . . . 8 $/\$ $/\$ $/\$
20		nfv 1728	. . . . . . . . . . 11 $/\$
21		nfra1 2785	. . . . . . . . . . 11 $/\$
22	20, 21	nfan 1956	. . . . . . . . . 10 $/\$ $/\$ $/\$
23		nfv 1728	. . . . . . . . . 10
24	22, 23	nfim 1948	. . . . . . . . 9 $/\$ $/\$ $/\$
25		ovex 6306	. . . . . . . . 9
26		eleq1 2474	. . . . . . . . . . 11
27		oveq2 6286	. . . . . . . . . . . . 13
28	27	breq2d 4407	. . . . . . . . . . . 12
29	28	2rexbidv 2925	. . . . . . . . . . 11
30	26, 29	imbi12d 318	. . . . . . . . . 10
31	30	imbi2d 314	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simpll 752	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 459	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
34		rspa 2771	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
35	34	adantll 712	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
36		limclner.f	. . . . . . . . . . . . . . . . . . . . . . 23
37		fresin 5737	. . . . . . . . . . . . . . . . . . . . . . 23
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
39		inss2 3660	. . . . . . . . . . . . . . . . . . . . . . . 24
40		ioosscn 36896	. . . . . . . . . . . . . . . . . . . . . . . 24
41	39, 40	sstri 3451	. . . . . . . . . . . . . . . . . . . . . . 23
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
43		limclner.j	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		retop 21560	. . . . . . . . . . . . . . . . . . . . . . . . . 26
45	43, 44	eqeltri 2486	. . . . . . . . . . . . . . . . . . . . . . . . 25
46		ioossre 11640	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47	39, 46	sstri 3451	. . . . . . . . . . . . . . . . . . . . . . . . 25
48		uniretop 21561	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
49	43	unieqi 4200	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
50	48, 49	eqtr4i 2434	. . . . . . . . . . . . . . . . . . . . . . . . . 26
51	50	lpss 19936	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
52	45, 47, 51	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . 24
53		limclner.blp1	. . . . . . . . . . . . . . . . . . . . . . . 24
54	52, 53	sseldi 3440	. . . . . . . . . . . . . . . . . . . . . . 23
55	54	recnd 9652	. . . . . . . . . . . . . . . . . . . . . 22
56	38, 42, 55	ellimc3 22575	. . . . . . . . . . . . . . . . . . . . 21 lim $/\$ $/\$
57	6, 56	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
58	57	simprd 461	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	r19.21bi 2773	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
60	59	3ad2ant1 1018	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
61		simp11l 1108	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		simp12 1028	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp2 998	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		ifcl 3927	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
65	64	3adant1 1015	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		inss1 3659	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68		limclner.k	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
69	68	cnfldtop 21583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
71		ax-resscn 9579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
72	71	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
73	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
74		unicntop 36807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
75	68	unieqi 4200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
76	74, 75	eqtr4i 2434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77	68	tgioo2 21600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ↾_t
78	43, 77	eqtri 2431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ↾_t
79	76, 78	restlp 19977	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
80	70, 72, 73, 79	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	68	eqcomi 2415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
82	81	fveq2i 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld
83	82	fveq1i 5850	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℂ_fld
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℂ_fld
85	67, 80, 84	3sstr4d 3485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld
86	85, 53	sseldd 3443	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld
87	42, 55	islpcn 37013	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld $\$
88	86, 87	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
89	88	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
90		breq2 4399	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	90	rexbidv 2918	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
92	91	rspcva 3158	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $\$
93	65, 89, 92	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
94		eldifi 3565	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
95	47, 94	sseldi 3440	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
96	72	sselda 3442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
97	55	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
98	96, 97	subcld 9967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
99	98	abscld 13416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
100	99	3ad2antl1 1159	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
101	100	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
102	65	rpred 11304	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
103	102	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
104		rpre 11271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
105	104	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
106	105	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
107		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
108		rpre 11271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109		min1 11442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
110	104, 108, 109	syl2an 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
111	110	3adant1 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
112	111	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
113	101, 103, 106, 107, 112	ltletrd 9776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
114	108	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
115	114	3adant1 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
116	115	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
117		min2 11443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
118	104, 108, 117	syl2an 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
119	118	3adant1 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
120	119	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
121	101, 103, 116, 107, 120	ltletrd 9776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
122	113, 121	jca 530	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
123	122	ex 432	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
124	95, 123	sylan2 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$ $/\$
125	124	reximdva 2879	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $/\$
126	93, 125	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$
127	61, 62, 63, 126	syl3anc 1230	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
128		nfv 1728	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129		nfre1 2865	. . . . . . . . . . . . . . . . . . . . 21 $/\$
130		inss1 3659	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	130, 94	sseldi 3440	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
132	131	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
133		simp113 1128	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
134		eldifsni 4098	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
135	134	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
136		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
137	135, 136	jca 530	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $/\$ $/\$
138	137	3adant1 1015	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
139		neeq1 2684	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140		oveq1 6285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
141	140	fveq2d 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142	141	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143	139, 142	anbi12d 709	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
144		fveq2 5849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
145	144	oveq1d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
146	145	fveq2d 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
147	146	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
148	143, 147	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
149	148	rspcva 3158	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
150	149	imp 427	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
151	132, 133, 138, 150	syl21anc 1229	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
152	94	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
153	61	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
154		simp13 1029	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
155		nfv 1728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
156		nfra1 2785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
157	155, 156	nfan 1956	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
158		elinel2 3629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
159		fvres 5863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
160	158, 159	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
161	160	eqcomd 2410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
162	161	oveq1d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
163	162	fveq2d 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
164	163	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
165		rspa 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
166	165	3impia 1194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
167	166	3adant1l 1222	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
168	164, 167	eqbrtrd 4415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
169	168	3exp 1196	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
170	157, 169	ralrimi 2804	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
171	153, 154, 170	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
172	134	anim1i 566	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
173	172	adantrl 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $/\$ $/\$
174	173	3adant1 1015	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
175	141	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
176	139, 175	anbi12d 709	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	144	oveq1d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
178	177	fveq2d 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	178	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
180	176, 179	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	180	rspcva 3158	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
182	181	imp 427	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
183	152, 171, 174, 182	syl21anc 1229	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
184		rspe 2862	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
185	132, 151, 183, 184	syl12anc 1228	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
186	185	3exp 1196	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
187	128, 129, 186	rexlimd 2888	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
188	127, 187	mpd 15	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
189	188	3exp 1196	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
190	189	rexlimdv 2894	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
191	60, 190	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
192	191	3exp 1196	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
193	192	rexlimdv 2894	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
194	193	imp 427	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
195	194	adantllr 717	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
196		fresin 5737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
197	36, 196	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
198		inss2 3660	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
199		ioosscn 36896	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
200	198, 199	sstri 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
202	197, 201, 55	ellimc3 22575	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim $/\$ $/\$
203	2, 202	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	203	simprd 461	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
205	204	r19.21bi 2773	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
206	205	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
207		simp11l 1108	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
208		simp12 1028	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
209		simp2 998	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
210		inss1 3659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	210	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212		ioossre 11640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
213	198, 212	sstri 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
214	213	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
215	76, 78	restlp 19977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
216	70, 72, 214, 215	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
217	82	fveq1i 5850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ_fld
218	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
219	211, 216, 218	3sstr4d 3485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
220		limclner.blp2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
221	219, 220	sseldd 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld
222	201, 55	islpcn 37013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld $\$
223	221, 222	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
224	223	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
225		breq2 4399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
226	225	rexbidv 2918	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
227	226	rspcva 3158	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$
228	65, 224, 227	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$
229		eldifi 3565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
230	213, 229	sseldi 3440	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
231	72	sselda 3442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
232	55	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
233	231, 232	subcld 9967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
234	233	abscld 13416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
235	234	3ad2antl1 1159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
236	235	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
237	102	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
238	105	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
239		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
240	111	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
241	236, 237, 238, 239, 240	ltletrd 9776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
242	115	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
243	238, 242, 117	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
244	236, 237, 242, 239, 243	ltletrd 9776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
245	241, 244	jca 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
246	245	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
247	230, 246	sylan2 472	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $/\$
248	247	reximdva 2879	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$ $/\$
249	228, 248	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
250	207, 208, 209, 249	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
251		nfv 1728	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
252		nfre1 2865	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
253		inss1 3659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
254	253, 229	sseldi 3440	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
255	254	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
256		simp113 1128	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
257		eldifsni 4098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
258	257	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $/\$
259		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $/\$
260	258, 259	jca 530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $/\$ $/\$
261	260	3adant1 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
262		neeq1 2684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
263		oveq1 6285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
264	263	fveq2d 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
265	264	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
266	262, 265	anbi12d 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
267		fveq2 5849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
268	267	oveq1d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
269	268	fveq2d 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
270	269	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
271	266, 270	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
272	271	rspcva 3158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
273	272	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
274	255, 256, 261, 273	syl21anc 1229	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
275	229	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$