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 31860

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 22405	. . . . . . . . . . . . 13 lim
2		limclner.r	. . . . . . . . . . . . 13 lim
3	1, 2	sseldi 3497	. . . . . . . . . . . 12
4	3	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$
5		limccl 22405	. . . . . . . . . . . . 13 lim
6		limclner.l	. . . . . . . . . . . . 13 lim
7	5, 6	sseldi 3497	. . . . . . . . . . . 12
8	7	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$
9	4, 8	subcld 9950	. . . . . . . . . 10 $/\$ $/\$ $/\$
10		limclner.lner	. . . . . . . . . . . . 13
11	10	necomd 2728	. . . . . . . . . . . 12
12	11	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13	4, 8, 12	subne0d 9959	. . . . . . . . . 10 $/\$ $/\$ $/\$
14	9, 13	absrpcld 13291	. . . . . . . . 9 $/\$ $/\$ $/\$
15		4re 10633	. . . . . . . . . . 11
16		4pos 10652	. . . . . . . . . . 11
17	15, 16	elrpii 11248	. . . . . . . . . 10
18	17	a1i 11	. . . . . . . . 9 $/\$ $/\$ $/\$
19	14, 18	rpdivcld 11298	. . . . . . . 8 $/\$ $/\$ $/\$
20		nfv 1708	. . . . . . . . . . 11 $/\$
21		nfra1 2838	. . . . . . . . . . 11 $/\$
22	20, 21	nfan 1929	. . . . . . . . . 10 $/\$ $/\$ $/\$
23		nfv 1708	. . . . . . . . . 10
24	22, 23	nfim 1921	. . . . . . . . 9 $/\$ $/\$ $/\$
25		ovex 6324	. . . . . . . . 9
26		eleq1 2529	. . . . . . . . . . 11
27		oveq2 6304	. . . . . . . . . . . . 13
28	27	breq2d 4468	. . . . . . . . . . . 12
29	28	2rexbidv 2975	. . . . . . . . . . 11
30	26, 29	imbi12d 320	. . . . . . . . . 10
31	30	imbi2d 316	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simpll 753	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
33		simpr 461	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
34		rspa 2824	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
35	34	adantll 713	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
36		limclner.f	. . . . . . . . . . . . . . . . . . . . . . 23
37		fresin 5760	. . . . . . . . . . . . . . . . . . . . . . 23
38	36, 37	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
39		inss2 3715	. . . . . . . . . . . . . . . . . . . . . . . 24
40		ioosscn 31730	. . . . . . . . . . . . . . . . . . . . . . . 24
41	39, 40	sstri 3508	. . . . . . . . . . . . . . . . . . . . . . 23
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
43		limclner.j	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44		retop 21394	. . . . . . . . . . . . . . . . . . . . . . . . . 26
45	43, 44	eqeltri 2541	. . . . . . . . . . . . . . . . . . . . . . . . 25
46		ioossre 11611	. . . . . . . . . . . . . . . . . . . . . . . . . 26
47	39, 46	sstri 3508	. . . . . . . . . . . . . . . . . . . . . . . . 25
48		uniretop 21395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
49	43	unieqi 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
50	48, 49	eqtr4i 2489	. . . . . . . . . . . . . . . . . . . . . . . . . 26
51	50	lpss 19770	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
52	45, 47, 51	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . 24
53		limclner.blp1	. . . . . . . . . . . . . . . . . . . . . . . 24
54	52, 53	sseldi 3497	. . . . . . . . . . . . . . . . . . . . . . 23
55	54	recnd 9639	. . . . . . . . . . . . . . . . . . . . . 22
56	38, 42, 55	ellimc3 22409	. . . . . . . . . . . . . . . . . . . . 21 lim $/\$ $/\$
57	6, 56	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
58	57	simprd 463	. . . . . . . . . . . . . . . . . . 19 $/\$
59	58	r19.21bi 2826	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
60	59	3ad2ant1 1017	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
61		simp11l 1107	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		simp12 1027	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp2 997	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		ifcl 3986	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
65	64	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
66		inss1 3714	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68		limclner.k	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
69	68	cnfldtop 21417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
71		ax-resscn 9566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
72	71	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
73	47	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
74		unicntop 31634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
75	68	unieqi 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
76	74, 75	eqtr4i 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77	68	tgioo2 21434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ↾_t
78	43, 77	eqtri 2486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ↾_t
79	76, 78	restlp 19811	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
80	70, 72, 73, 79	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
81	68	eqcomi 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
82	81	fveq2i 5875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld
83	82	fveq1i 5873	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℂ_fld
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ℂ_fld
85	67, 80, 84	3sstr4d 3542	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ℂ_fld
86	85, 53	sseldd 3500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld
87	42, 55	islpcn 31848	. . . . . . . . . . . . . . . . . . . . . . . . 25 ℂ_fld $\$
88	86, 87	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
89	88	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
90		breq2 4460	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	90	rexbidv 2968	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
92	91	rspcva 3208	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $\$
93	65, 89, 92	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
94		eldifi 3622	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
95	47, 94	sseldi 3497	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
96	72	sselda 3499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
97	55	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
98	96, 97	subcld 9950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
99	98	abscld 13279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
100	99	3ad2antl1 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
101	100	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
102	65	rpred 11281	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
103	102	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
104		rpre 11251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
105	104	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
106	105	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
107		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
108		rpre 11251	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109		min1 11414	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
110	104, 108, 109	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
111	110	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
112	111	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
113	101, 103, 106, 107, 112	ltletrd 9759	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
114	108	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
115	114	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
116	115	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
117		min2 11415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
118	104, 108, 117	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
119	118	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
120	119	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
121	101, 103, 116, 107, 120	ltletrd 9759	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
122	113, 121	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
123	122	ex 434	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
124	95, 123	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$ $/\$
125	124	reximdva 2932	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $/\$
126	93, 125	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$ $/\$
127	61, 62, 63, 126	syl3anc 1228	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
128		nfv 1708	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129		nfre1 2918	. . . . . . . . . . . . . . . . . . . . 21 $/\$
130		inss1 3714	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	130, 94	sseldi 3497	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
132	131	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
133		simp113 1127	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
134		eldifsni 4158	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$
135	134	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
136		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
137	135, 136	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $/\$ $/\$
138	137	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
139		neeq1 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140		oveq1 6303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
141	140	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142	141	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143	139, 142	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
144		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
145	144	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
146	145	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
147	146	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
148	143, 147	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
149	148	rspcva 3208	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
150	149	imp 429	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
151	132, 133, 138, 150	syl21anc 1227	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
152	94	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
153	61	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
154		simp13 1028	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
155		nfv 1708	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
156		nfra1 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
157	155, 156	nfan 1929	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
158		elinel2 31626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
159		fvres 5886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
160	158, 159	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
161	160	eqcomd 2465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
162	161	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
163	162	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
164	163	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
165		rspa 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
166	165	3impia 1193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$
167	166	3adant1l 1220	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$
168	164, 167	eqbrtrd 4476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
169	168	3exp 1195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
170	157, 169	ralrimi 2857	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
171	153, 154, 170	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
172	134	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$
173	172	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $/\$ $/\$
174	173	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
175	141	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
176	139, 175	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
177	144	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
178	177	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
179	178	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
180	176, 179	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
181	180	rspcva 3208	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
182	181	imp 429	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
183	152, 171, 174, 182	syl21anc 1227	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
184		rspe 2915	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
185	132, 151, 183, 184	syl12anc 1226	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
186	185	3exp 1195	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
187	128, 129, 186	rexlimd 2941	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
188	127, 187	mpd 15	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
189	188	3exp 1195	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
190	189	rexlimdv 2947	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
191	60, 190	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
192	191	3exp 1195	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
193	192	rexlimdv 2947	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
194	193	imp 429	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
195	194	adantllr 718	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
196		fresin 5760	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
197	36, 196	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26
198		inss2 3715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
199		ioosscn 31730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
200	198, 199	sstri 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
201	200	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
202	197, 201, 55	ellimc3 22409	. . . . . . . . . . . . . . . . . . . . . . . . 25 lim $/\$ $/\$
203	2, 202	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
204	203	simprd 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
205	204	r19.21bi 2826	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
206	205	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
207		simp11l 1107	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
208		simp12 1027	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
209		simp2 997	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
210		inss1 3714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	210	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212		ioossre 11611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
213	198, 212	sstri 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
214	213	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
215	76, 78	restlp 19811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
216	70, 72, 214, 215	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
217	82	fveq1i 5873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ℂ_fld
218	217	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ℂ_fld
219	211, 216, 218	3sstr4d 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ℂ_fld
220		limclner.blp2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
221	219, 220	sseldd 3500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld
222	201, 55	islpcn 31848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℂ_fld $\$
223	221, 222	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
224	223	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$
225		breq2 4460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
226	225	rexbidv 2968	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
227	226	rspcva 3208	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$
228	65, 224, 227	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$
229		eldifi 3622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
230	213, 229	sseldi 3497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
231	72	sselda 3499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
232	55	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
233	231, 232	subcld 9950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
234	233	abscld 13279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
235	234	3ad2antl1 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
236	235	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
237	102	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
238	105	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
239		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
240	111	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
241	236, 237, 238, 239, 240	ltletrd 9759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
242	115	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
243	238, 242, 117	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$
244	236, 237, 242, 239, 243	ltletrd 9759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
245	241, 244	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
246	245	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
247	230, 246	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $/\$
248	247	reximdva 2932	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $\$ $/\$
249	228, 248	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
250	207, 208, 209, 249	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
251		nfv 1708	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
252		nfre1 2918	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
253		inss1 3714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
254	253, 229	sseldi 3497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
255	254	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
256		simp113 1127	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
257		eldifsni 4158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$
258	257	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $/\$
259		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $/\$
260	258, 259	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $/\$ $/\$
261	260	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
262		neeq1 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
263		oveq1 6303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
264	263	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
265	264	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
266	262, 265	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
267		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
268	267	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
269	268	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
270	269	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
271	266, 270	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
272	271	rspcva 3208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
273	272	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
274	255, 256, 261, 273	syl21anc 1227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
275	229	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$