limciccioolb

Description: The limit of a function at the lower bound of a closed interval only depends on the values in the inner open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	limciccioolb.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	limciccioolb.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	limciccioolb.3	⊢ ( 𝜑 → 𝐴 < 𝐵 )
	limciccioolb.4	⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
Assertion	limciccioolb	⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) lim_ℂ 𝐴 ) = ( 𝐹 lim_ℂ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		limciccioolb.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		limciccioolb.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		limciccioolb.3	⊢ ( 𝜑 → 𝐴 < 𝐵 )
4		limciccioolb.4	⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
5		ioossicc	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
6	5	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
7	1 2	iccssred	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
8		ax-resscn	⊢ ℝ ⊆ ℂ
9	7 8	sstrdi	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
10		eqid	⊢ ( TopOpen ‘ ℂ_fld ) = ( TopOpen ‘ ℂ_fld )
11		eqid	⊢ ( ( TopOpen ‘ ℂ_fld ) ↾_t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) ) = ( ( TopOpen ‘ ℂ_fld ) ↾_t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) )
12		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
13	12	a1i	⊢ ( 𝜑 → ( topGen ‘ ran (,) ) ∈ Top )
14	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
15		icossre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^* ) → ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
16	1 14 15	syl2anc	⊢ ( 𝜑 → ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
17		difssd	⊢ ( 𝜑 → ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ )
18	16 17	unssd	⊢ ( 𝜑 → ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ℝ )
19		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
20	18 19	sseqtrdi	⊢ ( 𝜑 → ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ∪ ( topGen ‘ ran (,) ) )
21		elioore	⊢ ( 𝑥 ∈ ( -∞ (,) 𝐵 ) → 𝑥 ∈ ℝ )
22	21	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
23		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ≤ 𝑥 )
24		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → 𝑥 ∈ ( -∞ (,) 𝐵 ) )
25		mnfxr	⊢ -∞ ∈ ℝ^*
26	25	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → -∞ ∈ ℝ^* )
27	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → 𝐵 ∈ ℝ^* )
28		elioo2	⊢ ( ( -∞ ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝑥 ∈ ( -∞ (,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
29	26 27 28	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → ( 𝑥 ∈ ( -∞ (,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐵 ) ) )
30	24 29	mpbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ -∞ < 𝑥 ∧ 𝑥 < 𝐵 ) )
31	30	simp3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → 𝑥 < 𝐵 )
32	31	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝑥 < 𝐵 )
33	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝐴 ∈ ℝ )
34	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝐵 ∈ ℝ^* )
35		elico2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
36	33 34 35	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
37	22 23 32 36	mpbir3and	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → 𝑥 ∈ ( 𝐴 [,) 𝐵 ) )
38	37	orcd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ 𝐴 ≤ 𝑥 ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
39	21	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
40		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → ¬ 𝐴 ≤ 𝑥 )
41	40	intnanrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → ¬ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
42	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
43	42	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → 𝐴 ∈ ℝ^* )
44	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → 𝐵 ∈ ℝ^* )
45	39	rexrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → 𝑥 ∈ ℝ^* )
46		elicc4	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
47	43 44 45 46	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
48	41 47	mtbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
49	39 48	eldifd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) )
50	49	olcd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝑥 ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
51	38 50	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
52		elun	⊢ ( 𝑥 ∈ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ↔ ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
53	51 52	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( -∞ (,) 𝐵 ) ) → 𝑥 ∈ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
54	53	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( -∞ (,) 𝐵 ) 𝑥 ∈ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
55		dfss3	⊢ ( ( -∞ (,) 𝐵 ) ⊆ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ↔ ∀ 𝑥 ∈ ( -∞ (,) 𝐵 ) 𝑥 ∈ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
56	54 55	sylibr	⊢ ( 𝜑 → ( -∞ (,) 𝐵 ) ⊆ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
57		eqid	⊢ ∪ ( topGen ‘ ran (,) ) = ∪ ( topGen ‘ ran (,) )
58	57	ntrss	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ∪ ( topGen ‘ ran (,) ) ∧ ( -∞ (,) 𝐵 ) ⊆ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( -∞ (,) 𝐵 ) ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
59	13 20 56 58	syl3anc	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( -∞ (,) 𝐵 ) ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
60	25	a1i	⊢ ( 𝜑 → -∞ ∈ ℝ^* )
61	1	mnfltd	⊢ ( 𝜑 → -∞ < 𝐴 )
62	60 14 1 61 3	eliood	⊢ ( 𝜑 → 𝐴 ∈ ( -∞ (,) 𝐵 ) )
63		iooretop	⊢ ( -∞ (,) 𝐵 ) ∈ ( topGen ‘ ran (,) )
64	63	a1i	⊢ ( 𝜑 → ( -∞ (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) )
65		isopn3i	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( -∞ (,) 𝐵 ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( -∞ (,) 𝐵 ) ) = ( -∞ (,) 𝐵 ) )
66	13 64 65	syl2anc	⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( -∞ (,) 𝐵 ) ) = ( -∞ (,) 𝐵 ) )
67	62 66	eleqtrrd	⊢ ( 𝜑 → 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( -∞ (,) 𝐵 ) ) )
68	59 67	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
69	1	leidd	⊢ ( 𝜑 → 𝐴 ≤ 𝐴 )
70	1 2 3	ltled	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
71	1 2 1 69 70	eliccd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
72	68 71	elind	⊢ ( 𝜑 → 𝐴 ∈ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
73		icossicc	⊢ ( 𝐴 [,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
74	73	a1i	⊢ ( 𝜑 → ( 𝐴 [,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
75		eqid	⊢ ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) )
76	19 75	restntr	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ( 𝐴 [,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ) → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) = ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
77	13 7 74 76	syl3anc	⊢ ( 𝜑 → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) = ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 [,) 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
78	72 77	eleqtrrd	⊢ ( 𝜑 → 𝐴 ∈ ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) )
79		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
80	10 79	rerest	⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( ( TopOpen ‘ ℂ_fld ) ↾_t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) )
81	7 80	syl	⊢ ( 𝜑 → ( ( TopOpen ‘ ℂ_fld ) ↾_t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) )
82	81	eqcomd	⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂ_fld ) ↾_t ( 𝐴 [,] 𝐵 ) ) )
83	82	fveq2d	⊢ ( 𝜑 → ( int ‘ ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) ) = ( int ‘ ( ( TopOpen ‘ ℂ_fld ) ↾_t ( 𝐴 [,] 𝐵 ) ) ) )
84	83	fveq1d	⊢ ( 𝜑 → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾_t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂ_fld ) ↾_t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) )
85	78 84	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂ_fld ) ↾_t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) )
86	71	snssd	⊢ ( 𝜑 → { 𝐴 } ⊆ ( 𝐴 [,] 𝐵 ) )
87		ssequn2	⊢ ( { 𝐴 } ⊆ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) = ( 𝐴 [,] 𝐵 ) )
88	86 87	sylib	⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) = ( 𝐴 [,] 𝐵 ) )
89	88	eqcomd	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) )
90	89	oveq2d	⊢ ( 𝜑 → ( ( TopOpen ‘ ℂ_fld ) ↾_t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂ_fld ) ↾_t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) ) )
91	90	fveq2d	⊢ ( 𝜑 → ( int ‘ ( ( TopOpen ‘ ℂ_fld ) ↾_t ( 𝐴 [,] 𝐵 ) ) ) = ( int ‘ ( ( TopOpen ‘ ℂ_fld ) ↾_t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) ) ) )
92		uncom	⊢ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) = ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) )
93		snunioo	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) → ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
94	42 14 3 93	syl3anc	⊢ ( 𝜑 → ( { 𝐴 } ∪ ( 𝐴 (,) 𝐵 ) ) = ( 𝐴 [,) 𝐵 ) )
95	92 94	eqtr2id	⊢ ( 𝜑 → ( 𝐴 [,) 𝐵 ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) )
96	91 95	fveq12d	⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂ_fld ) ↾_t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 [,) 𝐵 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂ_fld ) ↾_t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) ) )
97	85 96	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂ_fld ) ↾_t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐴 } ) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) ) )
98	4 6 9 10 11 97	limcres	⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) lim_ℂ 𝐴 ) = ( 𝐹 lim_ℂ 𝐴 ) )

Metamath Proof Explorer

Theorem limciccioolb

Proof