This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limcicciooub

Description: The limit of a function at the upper 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 limcicciooub.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
limcicciooub.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
limcicciooub.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
limcicciooub.4 ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
Assertion limcicciooub ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) = ( 𝐹 limℂ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 limcicciooub.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 limcicciooub.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 limcicciooub.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 limcicciooub.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 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
15 iocssre ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
16 14 2 15 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ℝ )
17 difssd ⊢ ( 𝜑 → ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ⊆ ℝ )
18 16 17 unssd ⊢ ( 𝜑 → ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ℝ )
19 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
20 18 19 sseqtrdi ⊢ ( 𝜑 → ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ∪ ( topGen ‘ ran (,) ) )
21 elioore ⊢ ( 𝑥 ∈ ( 𝐴 (,) +∞ ) → 𝑥 ∈ ℝ )
22 21 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → 𝑥 ∈ ℝ )
23 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → 𝑥 ∈ ( 𝐴 (,) +∞ ) )
24 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → 𝐴 ∈ ℝ* )
25 pnfxr ⊢ +∞ ∈ ℝ*
26 elioo2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) ) )
27 24 25 26 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → ( 𝑥 ∈ ( 𝐴 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) ) )
28 23 27 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 < +∞ ) )
29 28 simp2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → 𝐴 < 𝑥 )
30 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → 𝑥 ≤ 𝐵 )
31 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
32 elioc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
33 24 31 32 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 < 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
34 22 29 30 33 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → 𝑥 ∈ ( 𝐴 (,] 𝐵 ) )
35 34 orcd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ 𝑥 ≤ 𝐵 ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
36 21 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ ¬ 𝑥 ≤ 𝐵 ) → 𝑥 ∈ ℝ )
37 3mix3 ⊢ ( ¬ 𝑥 ≤ 𝐵 → ( ¬ 𝑥 ∈ ℝ ∨ ¬ 𝐴 ≤ 𝑥 ∨ ¬ 𝑥 ≤ 𝐵 ) )
38 3ianor ⊢ ( ¬ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ↔ ( ¬ 𝑥 ∈ ℝ ∨ ¬ 𝐴 ≤ 𝑥 ∨ ¬ 𝑥 ≤ 𝐵 ) )
39 37 38 sylibr ⊢ ( ¬ 𝑥 ≤ 𝐵 → ¬ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
40 39 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ ¬ 𝑥 ≤ 𝐵 ) → ¬ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) )
41 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ ¬ 𝑥 ≤ 𝐵 ) → 𝐴 ∈ ℝ )
42 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ ¬ 𝑥 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
43 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
44 41 42 43 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ ¬ 𝑥 ≤ 𝐵 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 ≤ 𝐵 ) ) )
45 40 44 mtbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ ¬ 𝑥 ≤ 𝐵 ) → ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
46 36 45 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ ¬ 𝑥 ≤ 𝐵 ) → 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) )
47 46 olcd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) ∧ ¬ 𝑥 ≤ 𝐵 ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
48 35 47 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) → ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
49 elun ⊢ ( 𝑥 ∈ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ↔ ( 𝑥 ∈ ( 𝐴 (,] 𝐵 ) ∨ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
50 48 49 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) +∞ ) ) → 𝑥 ∈ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
51 50 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) +∞ ) 𝑥 ∈ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
52 dfss3 ⊢ ( ( 𝐴 (,) +∞ ) ⊆ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ↔ ∀ 𝑥 ∈ ( 𝐴 (,) +∞ ) 𝑥 ∈ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
53 51 52 sylibr ⊢ ( 𝜑 → ( 𝐴 (,) +∞ ) ⊆ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) )
54 eqid ⊢ ∪ ( topGen ‘ ran (,) ) = ∪ ( topGen ‘ ran (,) )
55 54 ntrss ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ⊆ ∪ ( topGen ‘ ran (,) ) ∧ ( 𝐴 (,) +∞ ) ⊆ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) +∞ ) ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
56 13 20 53 55 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) +∞ ) ) ⊆ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
57 25 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
58 2 ltpnfd ⊢ ( 𝜑 → 𝐵 < +∞ )
59 14 57 2 3 58 eliood ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 (,) +∞ ) )
60 iooretop ⊢ ( 𝐴 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
61 isopn3i ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 (,) +∞ ) ∈ ( topGen ‘ ran (,) ) ) → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) +∞ ) ) = ( 𝐴 (,) +∞ ) )
62 13 60 61 sylancl ⊢ ( 𝜑 → ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) +∞ ) ) = ( 𝐴 (,) +∞ ) )
63 59 62 eleqtrrd ⊢ ( 𝜑 → 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( 𝐴 (,) +∞ ) ) )
64 56 63 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) )
65 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
66 1 2 3 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
67 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
68 14 65 66 67 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
69 64 68 elind ⊢ ( 𝜑 → 𝐵 ∈ ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
70 iocssicc ⊢ ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
71 70 a1i ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
72 eqid ⊢ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) )
73 19 72 restntr ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ( 𝐴 (,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) ) → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) = ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
74 13 7 71 73 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) = ( ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝐴 (,] 𝐵 ) ∪ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) ) ∩ ( 𝐴 [,] 𝐵 ) ) )
75 69 74 eleqtrrd ⊢ ( 𝜑 → 𝐵 ∈ ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) )
76 eqid ⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
77 10 76 rerest ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
78 7 77 syl ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) )
79 78 eqcomd ⊢ ( 𝜑 → ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) )
80 79 fveq2d ⊢ ( 𝜑 → ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) = ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) )
81 80 fveq1d ⊢ ( 𝜑 → ( ( int ‘ ( ( topGen ‘ ran (,) ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) )
82 75 81 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) )
83 68 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) )
84 ssequn2 ⊢ ( { 𝐵 } ⊆ ( 𝐴 [,] 𝐵 ) ↔ ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
85 83 84 sylib ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
86 85 eqcomd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐵 } ) )
87 86 oveq2d ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐵 } ) ) )
88 87 fveq2d ⊢ ( 𝜑 → ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) = ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐵 } ) ) ) )
89 ioounsn ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
90 14 65 3 89 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
91 90 eqcomd ⊢ ( 𝜑 → ( 𝐴 (,] 𝐵 ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) )
92 88 91 fveq12d ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝐴 [,] 𝐵 ) ) ) ‘ ( 𝐴 (,] 𝐵 ) ) = ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐵 } ) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) )
93 82 92 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t ( ( 𝐴 [,] 𝐵 ) ∪ { 𝐵 } ) ) ) ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) )
94 4 6 9 10 11 93 limcres ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 (,) 𝐵 ) ) limℂ 𝐵 ) = ( 𝐹 limℂ 𝐵 ) )