Metamath Proof Explorer

Theorem dvcnp2

Description: A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses dvcnp.j ⊢ 𝐽 = ( 𝐾 ↾t 𝐴 )
dvcnp.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion dvcnp2 ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 dvcnp.j ⊢ 𝐽 = ( 𝐾 ↾t 𝐴 )
2 dvcnp.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
3 simpl2 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐹 : 𝐴 ⟶ ℂ )
4 3 ffvelcdmda ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
5 2 cnfldtop ⊢ 𝐾 ∈ Top
6 simpl1 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑆 ⊆ ℂ )
7 cnex ⊢ ℂ ∈ V
8 ssexg ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
9 6 7 8 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑆 ∈ V )
10 resttop ⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝐾 ↾t 𝑆 ) ∈ Top )
11 5 9 10 sylancr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐾 ↾t 𝑆 ) ∈ Top )
12 simpl3 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐴 ⊆ 𝑆 )
13 2 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
14 resttopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
15 13 6 14 sylancr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
16 toponuni ⊢ ( ( 𝐾 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ ( 𝐾 ↾t 𝑆 ) )
17 15 16 syl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑆 = ∪ ( 𝐾 ↾t 𝑆 ) )
18 12 17 sseqtrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐴 ⊆ ∪ ( 𝐾 ↾t 𝑆 ) )
19 eqid ⊢ ∪ ( 𝐾 ↾t 𝑆 ) = ∪ ( 𝐾 ↾t 𝑆 )
20 19 ntrss2 ⊢ ( ( ( 𝐾 ↾t 𝑆 ) ∈ Top ∧ 𝐴 ⊆ ∪ ( 𝐾 ↾t 𝑆 ) ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ 𝐴 ) ⊆ 𝐴 )
21 11 18 20 syl2anc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ 𝐴 ) ⊆ 𝐴 )
22 eqid ⊢ ( 𝐾 ↾t 𝑆 ) = ( 𝐾 ↾t 𝑆 )
23 eqid ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) )
24 simp1 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝑆 ⊆ ℂ )
25 simp2 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝐹 : 𝐴 ⟶ ℂ )
26 simp3 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → 𝐴 ⊆ 𝑆 )
27 22 2 23 24 25 26 eldv ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ↔ ( 𝐵 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) ) ) )
28 27 simprbda ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ 𝐴 ) )
29 21 28 sseldd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ 𝐴 )
30 3 29 ffvelcdmd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
31 30 adantr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
32 4 31 subcld ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ )
33 ssidd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ℂ ⊆ ℂ )
34 txtopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ) → ( 𝐾 ×t 𝐾 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) ) )
35 13 13 34 mp2an ⊢ ( 𝐾 ×t 𝐾 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) )
36 35 toponrestid ⊢ ( 𝐾 ×t 𝐾 ) = ( ( 𝐾 ×t 𝐾 ) ↾t ( ℂ × ℂ ) )
37 12 6 sstrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐴 ⊆ ℂ )
38 eqid ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑥 − 𝐵 ) ) ) = ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑥 − 𝐵 ) ) )
39 22 2 38 24 25 26 eldv ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ↔ ( 𝐵 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑥 − 𝐵 ) ) ) limℂ 𝐵 ) ) ) )
40 39 simprbda ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ ( ( int ‘ ( 𝐾 ↾t 𝑆 ) ) ‘ 𝐴 ) )
41 21 40 sseldd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ 𝐴 )
42 3 37 41 dvlem ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ∈ ℂ )
43 37 ssdifssd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
44 43 sselda ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ ℂ )
45 37 41 sseldd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ ℂ )
46 45 adantr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐵 ∈ ℂ )
47 44 46 subcld ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 − 𝐵 ) ∈ ℂ )
48 27 simplbda ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) )
49 limcresi ⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 ) ⊆ ( ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 )
50 difss ⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
51 resmpt ⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) )
52 50 51 ax-mp ⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) )
53 52 oveq1i ⊢ ( ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 )
54 49 53 sseqtri ⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 ) ⊆ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 )
55 45 subidd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐵 − 𝐵 ) = 0 )
56 ssid ⊢ ℂ ⊆ ℂ
57 cncfmptid ⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ 𝐴 ↦ 𝑧 ) ∈ ( 𝐴 –cn→ ℂ ) )
58 37 56 57 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ 𝑧 ) ∈ ( 𝐴 –cn→ ℂ ) )
59 cncfmptc ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
60 45 37 33 59 syl3anc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
61 58 60 subcncf ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
62 oveq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 − 𝐵 ) = ( 𝐵 − 𝐵 ) )
63 61 41 62 cnmptlimc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐵 − 𝐵 ) ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 ) )
64 55 63 eqeltrrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 ) )
65 54 64 sselid ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 ) )
66 2 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
67 24 25 26 dvcl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ℂ )
68 0cn ⊢ 0 ∈ ℂ
69 opelxpi ⊢ ( ( 𝑦 ∈ ℂ ∧ 0 ∈ ℂ ) → ⟨ 𝑦 , 0 ⟩ ∈ ( ℂ × ℂ ) )
70 67 68 69 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ⟨ 𝑦 , 0 ⟩ ∈ ( ℂ × ℂ ) )
71 35 toponunii ⊢ ( ℂ × ℂ ) = ∪ ( 𝐾 ×t 𝐾 )
72 71 cncnpi ⊢ ( ( ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) ∧ ⟨ 𝑦 , 0 ⟩ ∈ ( ℂ × ℂ ) ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( 𝐾 ×t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 𝑦 , 0 ⟩ ) )
73 66 70 72 sylancr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( ( 𝐾 ×t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 𝑦 , 0 ⟩ ) )
74 42 47 33 33 2 36 48 65 73 limccnp2 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 0 ) ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) )
75 df-mpt ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) }
76 75 oveq1i ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) = ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) } limℂ 𝐵 )
77 74 76 eleqtrdi ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 0 ) ∈ ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) } limℂ 𝐵 ) )
78 0cnd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ℂ )
79 ovmpot ⊢ ( ( 𝑦 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 0 ) = ( 𝑦 · 0 ) )
80 67 78 79 syl2anc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 0 ) = ( 𝑦 · 0 ) )
81 3 37 29 dvlem ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ∈ ℂ )
82 37 29 sseldd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ ℂ )
83 82 adantr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐵 ∈ ℂ )
84 44 83 subcld ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 − 𝐵 ) ∈ ℂ )
85 ovmpot ⊢ ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ∈ ℂ ∧ ( 𝑧 − 𝐵 ) ∈ ℂ ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) )
86 81 84 85 syl2anc ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) )
87 86 eqeq2d ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ↔ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) )
88 87 pm5.32da ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) ↔ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) ) )
89 88 opabbidv ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) } )
90 df-mpt ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) }
91 89 90 eqtr4di ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) } = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) )
92 91 oveq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ∧ 𝑤 = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑧 − 𝐵 ) ) ) } limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) )
93 77 80 92 3eltr3d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 · 0 ) ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) )
94 67 mul01d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 · 0 ) = 0 )
95 3 adantr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐹 : 𝐴 ⟶ ℂ )
96 simpr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) )
97 50 96 sselid ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ 𝐴 )
98 95 97 ffvelcdmd ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
99 30 adantr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
100 98 99 subcld ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ )
101 eldifsni ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → 𝑧 ≠ 𝐵 )
102 101 adantl ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ≠ 𝐵 )
103 44 83 102 subne0d ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 − 𝐵 ) ≠ 0 )
104 100 84 103 divcan1d ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) )
105 104 mpteq2dva ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) )
106 105 oveq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) )
107 93 94 106 3eltr3d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) )
108 32 fmpttd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) : 𝐴 ⟶ ℂ )
109 108 limcdif ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) = ( ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) )
110 resmpt ⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) )
111 50 110 ax-mp ⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) )
112 111 oveq1i ⊢ ( ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 )
113 109 112 eqtrdi ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) )
114 107 113 eleqtrrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) )
115 cncfmptc ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
116 30 37 33 115 syl3anc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
117 eqidd ⊢ ( 𝑧 = 𝐵 → ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
118 116 29 117 cnmptlimc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) limℂ 𝐵 ) )
119 2 addcn ⊢ + ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
120 opelxpi ⊢ ( ( 0 ∈ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℂ ) → ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ ( ℂ × ℂ ) )
121 68 30 120 sylancr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ ( ℂ × ℂ ) )
122 71 cncnpi ⊢ ( ( + ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) ∧ ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ ( ℂ × ℂ ) ) → + ∈ ( ( ( 𝐾 ×t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ) )
123 119 121 122 sylancr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → + ∈ ( ( ( 𝐾 ×t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ) )
124 32 31 33 33 2 36 114 118 123 limccnp2 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 0 + ( 𝐹 ‘ 𝐵 ) ) ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) )
125 30 addlidd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 0 + ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ 𝐵 ) )
126 4 31 npcand ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ 𝑧 ) )
127 126 mpteq2dva ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
128 3 feqmptd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
129 127 128 eqtr4d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) = 𝐹 )
130 129 oveq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) = ( 𝐹 limℂ 𝐵 ) )
131 124 125 130 3eltr3d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) )
132 2 1 cnplimc ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) ) )
133 37 29 132 syl2anc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) ) )
134 3 131 133 mpbir2and ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )
135 134 ex ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐵 ( 𝑆 D 𝐹 ) 𝑦 → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
136 135 exlimdv ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( ∃ 𝑦 𝐵 ( 𝑆 D 𝐹 ) 𝑦 → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
137 eldmg ⊢ ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) → ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ↔ ∃ 𝑦 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) )
138 137 ibi ⊢ ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) → ∃ 𝑦 𝐵 ( 𝑆 D 𝐹 ) 𝑦 )
139 136 138 impel ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )