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 37672

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 22828	. . . . . . . . . . . . 13 lim
2		limclner.r	. . . . . . . . . . . . 13 lim
3	1, 2	sseldi 3462	. . . . . . . . . . . 12
4	3	ad2antrr 730	. . . . . . . . . . 11 $/\$ $/\$ $/\$
5		limccl 22828	. . . . . . . . . . . . 13 lim
6		limclner.l	. . . . . . . . . . . . 13 lim
7	5, 6	sseldi 3462	. . . . . . . . . . . 12
8	7	ad2antrr 730	. . . . . . . . . . 11 $/\$ $/\$ $/\$
9	4, 8	subcld 9993	. . . . . . . . . 10 $/\$ $/\$ $/\$
10		limclner.lner	. . . . . . . . . . . . 13
11	10	necomd 2691	. . . . . . . . . . . 12
12	11	ad2antrr 730	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13	4, 8, 12	subne0d 10002	. . . . . . . . . 10 $/\$ $/\$ $/\$
14	9, 13	absrpcld 13509	. . . . . . . . 9 $/\$ $/\$ $/\$
15		4re 10693	. . . . . . . . . . 11
16		4pos 10712	. . . . . . . . . . 11
17	15, 16	elrpii 11312	. . . . . . . . . 10
18	17	a1i 11	. . . . . . . . 9 $/\$ $/\$ $/\$
19	14, 18	rpdivcld 11365	. . . . . . . 8 $/\$ $/\$ $/\$
20		nfv 1755	. . . . . . . . . . 11 $/\$
21		nfra1 2803	. . . . . . . . . . 11 $/\$
22	20, 21	nfan 1988	. . . . . . . . . 10 $/\$ $/\$ $/\$
23		nfv 1755	. . . . . . . . . 10
24	22, 23	nfim 1980	. . . . . . . . 9 $/\$ $/\$ $/\$
25		ovex 6333	. . . . . . . . 9
26		eleq1 2495	. . . . . . . . . . 11
27		oveq2 6313	. . . . . . . . . . . . 13
28	27	breq2d 4435	. . . . . . . . . . . 12
29	28	2rexbidv 2943	. . . . . . . . . . 11
30	26, 29	imbi12d 321	. . . . . . . . . 10
31	30	imbi2d 317	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simpll 758	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
34		rspa 2789	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
35	34	adantll 718	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
36		limclner.f	. . . . . . . . . . . . . . . . . . . . . . 23
37		fresin 5769	. . . . . . . . . . . . . . . . . . . . . . 23
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
39		inss2 3683	. . . . . . . . . . . . . . . . . . . . . . . 24
40		ioosscn 37540	. . . . . . . . . . . . . . . . . . . . . . . 24
41	39, 40	sstri 3473	. . . . . . . . . . . . . . . . . . . . . . 23
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
43		limclner.j	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		retop 21780	. . . . . . . . . . . . . . . . . . . . . . . . . 26
45	43, 44	eqeltri 2503	. . . . . . . . . . . . . . . . . . . . . . . . 25
46		ioossre 11703	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47	39, 46	sstri 3473	. . . . . . . . . . . . . . . . . . . . . . . . 25
48		uniretop 21781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
49	43	unieqi 4228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
50	48, 49	eqtr4i 2454	. . . . . . . . . . . . . . . . . . . . . . . . . 26
51	50	lpss 20156	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
52	45, 47, 51	mp2an 676	. . . . . . . . . . . . . . . . . . . . . . . 24
53		limclner.blp1	. . . . . . . . . . . . . . . . . . . . . . . 24
54	52, 53	sseldi 3462	. . . . . . . . . . . . . . . . . . . . . . 23
55	54	recnd 9676	. . . . . . . . . . . . . . . . . . . . . 22
56	38, 42, 55	ellimc3 22832	. . . . . . . . . . . . . . . . . . . . 21 lim $/\$ $/\$
57	6, 56	mpbid 213	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
58	57	simprd 464	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	r19.21bi 2791	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
60	59	3ad2ant1 1026	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
61		simp11l 1116	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		simp12 1036	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp2 1006	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		ifcl 3953	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
65	64	3adant1 1023	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		inss1 3682	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68		limclner.k	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
69	68	cnfldtop 21802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
71		ax-resscn 9603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
72	71	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
73	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
74		unicntop 37344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
75	68	unieqi 4228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
76	74, 75	eqtr4i 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77	68	tgioo2 21819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ↾_t
78	43, 77	eqtri 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ↾_t
79	76, 78	restlp 20197	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
80	70, 72, 73, 79	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	68	eqcomi 2435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
82	81	fveq2i 5884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld
83	82	fveq1i 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℂ_fld
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℂ_fld
85	67, 80, 84	3sstr4d 3507	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld
86	85, 53	sseldd 3465	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld
87	42, 55	islpcn 37659	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld $\$
88	86, 87	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
89	88	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
90		breq2 4427	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	90	rexbidv 2936	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
92	91	rspcva 3180	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $\$
93	65, 89, 92	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
94		eldifi 3587	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
95	47, 94	sseldi 3462	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
96	72	sselda 3464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
97	55	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
98	96, 97	subcld 9993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
99	98	abscld 13497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
100	99	3ad2antl1 1167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
101	100	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
102	65	rpred 11348	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
103	102	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
104		rpre 11315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
105	104	3ad2ant2 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
106	105	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
107		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
108		rpre 11315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109		min1 11490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
110	104, 108, 109	syl2an 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
111	110	3adant1 1023	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
112	111	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
113	101, 103, 106, 107, 112	ltletrd 9802	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
114	108	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
115	114	3adant1 1023	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
116	115	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
117		min2 11491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
118	104, 108, 117	syl2an 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
119	118	3adant1 1023	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
120	119	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
121	101, 103, 116, 107, 120	ltletrd 9802	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
122	113, 121	jca 534	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
123	122	ex 435	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
124	95, 123	sylan2 476	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$ $/\$
125	124	reximdva 2897	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $/\$
126	93, 125	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$
127	61, 62, 63, 126	syl3anc 1264	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
128		nfv 1755	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129		nfre1 2883	. . . . . . . . . . . . . . . . . . . . 21 $/\$
130		inss1 3682	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	130, 94	sseldi 3462	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
132	131	3ad2ant2 1027	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
133		simp113 1136	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
134		eldifsni 4126	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
135	134	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
136		simprl 762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
137	135, 136	jca 534	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $/\$ $/\$
138	137	3adant1 1023	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
139		neeq1 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140		oveq1 6312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
141	140	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142	141	breq1d 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143	139, 142	anbi12d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
144		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
145	144	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
146	145	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
147	146	breq1d 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
148	143, 147	imbi12d 321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
149	148	rspcva 3180	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
150	149	imp 430	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
151	132, 133, 138, 150	syl21anc 1263	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
152	94	3ad2ant2 1027	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
153	61	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
154		simp13 1037	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
155		nfv 1755	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
156		nfra1 2803	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
157	155, 156	nfan 1988	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
158		elinel2 3652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
159		fvres 5895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
160	158, 159	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
161	160	eqcomd 2430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
162	161	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
163	162	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
164	163	3ad2ant2 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
165		rspa 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
166	165	3impia 1202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
167	166	3adant1l 1256	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
168	164, 167	eqbrtrd 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
169	168	3exp 1204	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
170	157, 169	ralrimi 2822	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
171	153, 154, 170	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
172	134	anim1i 570	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
173	172	adantrl 720	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $/\$ $/\$
174	173	3adant1 1023	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
175	141	breq1d 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
176	139, 175	anbi12d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	144	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
178	177	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	178	breq1d 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
180	176, 179	imbi12d 321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	180	rspcva 3180	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
182	181	imp 430	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
183	152, 171, 174, 182	syl21anc 1263	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
184		rspe 2880	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
185	132, 151, 183, 184	syl12anc 1262	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
186	185	3exp 1204	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
187	128, 129, 186	rexlimd 2906	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
188	127, 187	mpd 15	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
189	188	3exp 1204	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
190	189	rexlimdv 2912	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
191	60, 190	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
192	191	3exp 1204	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
193	192	rexlimdv 2912	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
194	193	imp 430	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
195	194	adantllr 723	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
196		fresin 5769	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
197	36, 196	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
198		inss2 3683	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
199		ioosscn 37540	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
200	198, 199	sstri 3473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
202	197, 201, 55	ellimc3 22832	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim $/\$ $/\$
203	2, 202	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	203	simprd 464	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
205	204	r19.21bi 2791	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
206	205	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
207		simp11l 1116	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
208		simp12 1036	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
209		simp2 1006	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
210		inss1 3682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	210	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212		ioossre 11703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
213	198, 212	sstri 3473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
214	213	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
215	76, 78	restlp 20197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
216	70, 72, 214, 215	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
217	82	fveq1i 5882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ_fld
218	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
219	211, 216, 218	3sstr4d 3507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
220		limclner.blp2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
221	219, 220	sseldd 3465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld
222	201, 55	islpcn 37659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld $\$
223	221, 222	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
224	223	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
225		breq2 4427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
226	225	rexbidv 2936	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
227	226	rspcva 3180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$
228	65, 224, 227	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$
229		eldifi 3587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
230	213, 229	sseldi 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
231	72	sselda 3464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
232	55	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
233	231, 232	subcld 9993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
234	233	abscld 13497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
235	234	3ad2antl1 1167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
236	235	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
237	102	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
238	105	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
239		simpr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
240	111	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
241	236, 237, 238, 239, 240	ltletrd 9802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
242	115	ad2antrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
243	238, 242, 117	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
244	236, 237, 242, 239, 243	ltletrd 9802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
245	241, 244	jca 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
246	245	ex 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
247	230, 246	sylan2 476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $/\$
248	247	reximdva 2897	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$ $/\$
249	228, 248	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
250	207, 208, 209, 249	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
251		nfv 1755	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
252		nfre1 2883	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
253		inss1 3682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
254	253, 229	sseldi 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
255	254	3ad2ant2 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
256		simp113 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
257		eldifsni 4126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
258	257	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $/\$
259		simprl 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $/\$
260	258, 259	jca 534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $/\$ $/\$
261	260	3adant1 1023	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
262		neeq1 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
263		oveq1 6312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
264	263	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
265	264	breq1d 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
266	262, 265	anbi12d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
267		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
268	267	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
269	268	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
270	269	breq1d 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
271	266, 270	imbi12d 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
272	271	rspcva 3180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
273	272	imp 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
274	255, 256, 261, 273	syl21anc 1263	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
275	229	3ad2ant2 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$