limclner - Mathbox for Glauco Siliprandi

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

Theorem limclner 37774

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 22842	. . . . . . . . . . . . 13 lim
2		limclner.r	. . . . . . . . . . . . 13 lim
3	1, 2	sseldi 3398	. . . . . . . . . . . 12
4	3	ad2antrr 737	. . . . . . . . . . 11 $/\$ $/\$ $/\$
5		limccl 22842	. . . . . . . . . . . . 13 lim
6		limclner.l	. . . . . . . . . . . . 13 lim
7	5, 6	sseldi 3398	. . . . . . . . . . . 12
8	7	ad2antrr 737	. . . . . . . . . . 11 $/\$ $/\$ $/\$
9	4, 8	subcld 9973	. . . . . . . . . 10 $/\$ $/\$ $/\$
10		limclner.lner	. . . . . . . . . . . . 13
11	10	necomd 2679	. . . . . . . . . . . 12
12	11	ad2antrr 737	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13	4, 8, 12	subne0d 9982	. . . . . . . . . 10 $/\$ $/\$ $/\$
14	9, 13	absrpcld 13521	. . . . . . . . 9 $/\$ $/\$ $/\$
15		4re 10675	. . . . . . . . . . 11
16		4pos 10694	. . . . . . . . . . 11
17	15, 16	elrpii 11295	. . . . . . . . . 10
18	17	a1i 11	. . . . . . . . 9 $/\$ $/\$ $/\$
19	14, 18	rpdivcld 11348	. . . . . . . 8 $/\$ $/\$ $/\$
20		nfv 1765	. . . . . . . . . . 11 $/\$
21		nfra1 2766	. . . . . . . . . . 11 $/\$
22	20, 21	nfan 2016	. . . . . . . . . 10 $/\$ $/\$ $/\$
23		nfv 1765	. . . . . . . . . 10
24	22, 23	nfim 2008	. . . . . . . . 9 $/\$ $/\$ $/\$
25		ovex 6304	. . . . . . . . 9
26		eleq1 2518	. . . . . . . . . . 11
27		oveq2 6284	. . . . . . . . . . . . 13
28	27	breq2d 4386	. . . . . . . . . . . 12
29	28	2rexbidv 2878	. . . . . . . . . . 11
30	26, 29	imbi12d 326	. . . . . . . . . 10
31	30	imbi2d 322	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simpll 765	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
34		rspa 2755	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
35	34	adantll 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
36		limclner.f	. . . . . . . . . . . . . . . . . . . . . . 23
37		fresin 5735	. . . . . . . . . . . . . . . . . . . . . . 23
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
39		inss2 3621	. . . . . . . . . . . . . . . . . . . . . . . 24
40		ioosscn 37632	. . . . . . . . . . . . . . . . . . . . . . . 24
41	39, 40	sstri 3409	. . . . . . . . . . . . . . . . . . . . . . 23
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
43		limclner.j	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		retop 21793	. . . . . . . . . . . . . . . . . . . . . . . . . 26
45	43, 44	eqeltri 2526	. . . . . . . . . . . . . . . . . . . . . . . . 25
46		ioossre 11686	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47	39, 46	sstri 3409	. . . . . . . . . . . . . . . . . . . . . . . . 25
48		uniretop 21794	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
49	43	unieqi 4177	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
50	48, 49	eqtr4i 2477	. . . . . . . . . . . . . . . . . . . . . . . . . 26
51	50	lpss 20169	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
52	45, 47, 51	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . 24
53		limclner.blp1	. . . . . . . . . . . . . . . . . . . . . . . 24
54	52, 53	sseldi 3398	. . . . . . . . . . . . . . . . . . . . . . 23
55	54	recnd 9656	. . . . . . . . . . . . . . . . . . . . . 22
56	38, 42, 55	ellimc3 22846	. . . . . . . . . . . . . . . . . . . . 21 lim $/\$ $/\$
57	6, 56	mpbid 215	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
58	57	simprd 469	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	r19.21bi 2757	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
60	59	3ad2ant1 1030	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
61		simp11l 1120	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		simp12 1040	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp2 1010	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		ifcl 3891	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
65	64	3adant1 1027	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		inss1 3620	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68		limclner.k	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
69	68	cnfldtop 21815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
71		ax-resscn 9583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
72	71	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
73	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
74		unicntop 37367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
75	68	unieqi 4177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
76	74, 75	eqtr4i 2477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77	68	tgioo2 21832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ↾_t
78	43, 77	eqtri 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ↾_t
79	76, 78	restlp 20210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
80	70, 72, 73, 79	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	68	eqcomi 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
82	81	fveq2i 5851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld
83	82	fveq1i 5849	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℂ_fld
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℂ_fld
85	67, 80, 84	3sstr4d 3443	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld
86	85, 53	sseldd 3401	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld
87	42, 55	islpcn 37761	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld $\$
88	86, 87	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
89	88	3ad2ant1 1030	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
90		breq2 4378	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	90	rexbidv 2873	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
92	91	rspcva 3116	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $\$
93	65, 89, 92	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
94		eldifi 3523	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
95	47, 94	sseldi 3398	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
96	72	sselda 3400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
97	55	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
98	96, 97	subcld 9973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
99	98	abscld 13509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
100	99	3ad2antl1 1171	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
101	100	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
102	65	rpred 11331	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
103	102	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
104		rpre 11298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
105	104	3ad2ant2 1031	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
106	105	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
107		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
108		rpre 11298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109		min1 11473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
110	104, 108, 109	syl2an 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
111	110	3adant1 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
112	111	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
113	101, 103, 106, 107, 112	ltletrd 9782	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
114	108	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
115	114	3adant1 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
116	115	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
117		min2 11474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
118	104, 108, 117	syl2an 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
119	118	3adant1 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
120	119	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
121	101, 103, 116, 107, 120	ltletrd 9782	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
122	113, 121	jca 539	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
123	122	ex 440	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
124	95, 123	sylan2 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$ $/\$
125	124	reximdva 2839	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $/\$
126	93, 125	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$
127	61, 62, 63, 126	syl3anc 1271	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
128		nfv 1765	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129		nfre1 2827	. . . . . . . . . . . . . . . . . . . . 21 $/\$
130		inss1 3620	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	130, 94	sseldi 3398	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
132	131	3ad2ant2 1031	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
133		simp113 1140	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
134		eldifsni 4067	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
135	134	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
136		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
137	135, 136	jca 539	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $/\$ $/\$
138	137	3adant1 1027	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
139		neeq1 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140		oveq1 6283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
141	140	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142	141	breq1d 4384	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143	139, 142	anbi12d 722	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
144		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
145	144	oveq1d 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
146	145	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
147	146	breq1d 4384	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
148	143, 147	imbi12d 326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
149	148	rspcva 3116	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
150	149	imp 435	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
151	132, 133, 138, 150	syl21anc 1270	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
152	94	3ad2ant2 1031	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
153	61	3ad2ant1 1030	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
154		simp13 1041	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
155		nfv 1765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
156		nfra1 2766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
157	155, 156	nfan 2016	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
158		elinel2 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
159		fvres 5862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
160	158, 159	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
161	160	eqcomd 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
162	161	oveq1d 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
163	162	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
164	163	3ad2ant2 1031	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
165		rspa 2755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
166	165	3impia 1207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
167	166	3adant1l 1263	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
168	164, 167	eqbrtrd 4395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
169	168	3exp 1209	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
170	157, 169	ralrimi 2781	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
171	153, 154, 170	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
172	134	anim1i 576	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
173	172	adantrl 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $/\$ $/\$
174	173	3adant1 1027	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
175	141	breq1d 4384	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
176	139, 175	anbi12d 722	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	144	oveq1d 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
178	177	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	178	breq1d 4384	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
180	176, 179	imbi12d 326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	180	rspcva 3116	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
182	181	imp 435	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
183	152, 171, 174, 182	syl21anc 1270	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
184		rspe 2825	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
185	132, 151, 183, 184	syl12anc 1269	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
186	185	3exp 1209	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
187	128, 129, 186	rexlimd 2847	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
188	127, 187	mpd 15	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
189	188	3exp 1209	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
190	189	rexlimdv 2851	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
191	60, 190	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
192	191	3exp 1209	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
193	192	rexlimdv 2851	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
194	193	imp 435	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
195	194	adantllr 730	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
196		fresin 5735	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
197	36, 196	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
198		inss2 3621	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
199		ioosscn 37632	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
200	198, 199	sstri 3409	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
202	197, 201, 55	ellimc3 22846	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim $/\$ $/\$
203	2, 202	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	203	simprd 469	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
205	204	r19.21bi 2757	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
206	205	3ad2ant1 1030	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
207		simp11l 1120	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
208		simp12 1040	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
209		simp2 1010	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
210		inss1 3620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	210	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212		ioossre 11686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
213	198, 212	sstri 3409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
214	213	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
215	76, 78	restlp 20210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
216	70, 72, 214, 215	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
217	82	fveq1i 5849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ_fld
218	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
219	211, 216, 218	3sstr4d 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
220		limclner.blp2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
221	219, 220	sseldd 3401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld
222	201, 55	islpcn 37761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld $\$
223	221, 222	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
224	223	3ad2ant1 1030	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
225		breq2 4378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
226	225	rexbidv 2873	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
227	226	rspcva 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$
228	65, 224, 227	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$
229		eldifi 3523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
230	213, 229	sseldi 3398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
231	72	sselda 3400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
232	55	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
233	231, 232	subcld 9973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
234	233	abscld 13509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
235	234	3ad2antl1 1171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
236	235	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
237	102	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
238	105	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
239		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
240	111	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
241	236, 237, 238, 239, 240	ltletrd 9782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
242	115	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
243	238, 242, 117	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
244	236, 237, 242, 239, 243	ltletrd 9782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
245	241, 244	jca 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
246	245	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
247	230, 246	sylan2 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $/\$
248	247	reximdva 2839	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$ $/\$
249	228, 248	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
250	207, 208, 209, 249	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
251		nfv 1765	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
252		nfre1 2827	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
253		inss1 3620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
254	253, 229	sseldi 3398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
255	254	3ad2ant2 1031	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
256		simp113 1140	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
257		eldifsni 4067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
258	257	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $/\$
259		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $/\$
260	258, 259	jca 539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $/\$ $/\$
261	260	3adant1 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
262		neeq1 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
263		oveq1 6283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
264	263	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
265	264	breq1d 4384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
266	262, 265	anbi12d 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
267		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
268	267	oveq1d 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
269	268	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
270	269	breq1d 4384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
271	266, 270	imbi12d 326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
272	271	rspcva 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
273	272	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
274	255, 256, 261, 273	syl21anc 1270	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
275	229	3ad2ant2 1031	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$