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)

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 ffvelrnda ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 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 ffvelrnd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
31 30 adantr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
32 4 31 subcld ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ )
33 ssid ⊢ ℂ ⊆ ℂ
34 33 a1i ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ℂ ⊆ ℂ )
35 txtopon ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐾 ∈ ( TopOn ‘ ℂ ) ) → ( 𝐾 ×t 𝐾 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) ) )
36 13 13 35 mp2an ⊢ ( 𝐾 ×t 𝐾 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) )
37 36 toponrestid ⊢ ( 𝐾 ×t 𝐾 ) = ( ( 𝐾 ×t 𝐾 ) ↾t ( ℂ × ℂ ) )
38 12 6 sstrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐴 ⊆ ℂ )
39 3 38 29 dvlem ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ∈ ℂ )
40 38 ssdifssd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ℂ )
41 40 sselda ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ ℂ )
42 38 29 sseldd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐵 ∈ ℂ )
43 42 adantr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐵 ∈ ℂ )
44 41 43 subcld ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 − 𝐵 ) ∈ ℂ )
45 27 simplbda ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) )
46 limcresi ⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 ) ⊆ ( ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 )
47 difss ⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
48 resmpt ⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) )
49 47 48 ax-mp ⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) )
50 49 oveq1i ⊢ ( ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 )
51 46 50 sseqtri ⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 ) ⊆ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 )
52 42 subidd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐵 − 𝐵 ) = 0 )
53 2 subcn ⊢ − ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
54 53 a1i ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → − ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) )
55 cncfmptid ⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ 𝐴 ↦ 𝑧 ) ∈ ( 𝐴 –cn→ ℂ ) )
56 38 33 55 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ 𝑧 ) ∈ ( 𝐴 –cn→ ℂ ) )
57 cncfmptc ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
58 42 38 34 57 syl3anc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ 𝐵 ) ∈ ( 𝐴 –cn→ ℂ ) )
59 2 54 56 58 cncfmpt2f ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
60 oveq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 − 𝐵 ) = ( 𝐵 − 𝐵 ) )
61 59 29 60 cnmptlimc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐵 − 𝐵 ) ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 ) )
62 52 61 eqeltrrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 ) )
63 51 62 sseldi ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( 𝑧 − 𝐵 ) ) limℂ 𝐵 ) )
64 2 mulcn ⊢ · ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
65 24 25 26 dvcl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝑦 ∈ ℂ )
66 0cn ⊢ 0 ∈ ℂ
67 opelxpi ⊢ ( ( 𝑦 ∈ ℂ ∧ 0 ∈ ℂ ) → ⟨ 𝑦 , 0 ⟩ ∈ ( ℂ × ℂ ) )
68 65 66 67 sylancl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ⟨ 𝑦 , 0 ⟩ ∈ ( ℂ × ℂ ) )
69 36 toponunii ⊢ ( ℂ × ℂ ) = ∪ ( 𝐾 ×t 𝐾 )
70 69 cncnpi ⊢ ( ( · ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) ∧ ⟨ 𝑦 , 0 ⟩ ∈ ( ℂ × ℂ ) ) → · ∈ ( ( ( 𝐾 ×t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 𝑦 , 0 ⟩ ) )
71 64 68 70 sylancr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → · ∈ ( ( ( 𝐾 ×t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 𝑦 , 0 ⟩ ) )
72 39 44 34 34 2 37 45 63 71 limccnp2 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 · 0 ) ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) )
73 65 mul01d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑦 · 0 ) = 0 )
74 3 adantr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝐹 : 𝐴 ⟶ ℂ )
75 simpr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) )
76 47 75 sseldi ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ∈ 𝐴 )
77 74 76 ffvelrnd ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
78 30 adantr ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
79 77 78 subcld ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ∈ ℂ )
80 eldifsni ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) → 𝑧 ≠ 𝐵 )
81 80 adantl ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → 𝑧 ≠ 𝐵 )
82 41 43 81 subne0d ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( 𝑧 − 𝐵 ) ≠ 0 )
83 79 44 82 divcan1d ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) )
84 83 mpteq2dva ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) )
85 84 oveq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) · ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) )
86 72 73 85 3eltr3d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) )
87 32 fmpttd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) : 𝐴 ⟶ ℂ )
88 87 limcdif ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) = ( ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) )
89 resmpt ⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) )
90 47 89 ax-mp ⊢ ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) )
91 90 oveq1i ⊢ ( ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) ↾ ( 𝐴 ∖ { 𝐵 } ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 )
92 88 91 eqtrdi ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) = ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) )
93 86 92 eleqtrrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 0 ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) )
94 cncfmptc ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ℂ ∧ 𝐴 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
95 30 38 34 94 syl3anc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∈ ( 𝐴 –cn→ ℂ ) )
96 eqidd ⊢ ( 𝑧 = 𝐵 → ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
97 95 29 96 cnmptlimc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) limℂ 𝐵 ) )
98 2 addcn ⊢ + ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 )
99 opelxpi ⊢ ( ( 0 ∈ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℂ ) → ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ ( ℂ × ℂ ) )
100 66 30 99 sylancr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ ( ℂ × ℂ ) )
101 69 cncnpi ⊢ ( ( + ∈ ( ( 𝐾 ×t 𝐾 ) Cn 𝐾 ) ∧ ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ∈ ( ℂ × ℂ ) ) → + ∈ ( ( ( 𝐾 ×t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ) )
102 98 100 101 sylancr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → + ∈ ( ( ( 𝐾 ×t 𝐾 ) CnP 𝐾 ) ‘ ⟨ 0 , ( 𝐹 ‘ 𝐵 ) ⟩ ) )
103 32 31 34 34 2 37 93 97 102 limccnp2 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 0 + ( 𝐹 ‘ 𝐵 ) ) ∈ ( ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) )
104 30 addid2d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 0 + ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ 𝐵 ) )
105 4 31 npcand ⊢ ( ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) = ( 𝐹 ‘ 𝑧 ) )
106 105 mpteq2dva ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
107 3 feqmptd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
108 106 107 eqtr4d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) = 𝐹 )
109 108 oveq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( ( 𝑧 ∈ 𝐴 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) + ( 𝐹 ‘ 𝐵 ) ) ) limℂ 𝐵 ) = ( 𝐹 limℂ 𝐵 ) )
110 103 104 109 3eltr3d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) )
111 2 1 cnplimc ⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) ) )
112 38 29 111 syl2anc ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ ℂ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ( 𝐹 limℂ 𝐵 ) ) ) )
113 3 110 112 mpbir2and ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )
114 113 ex ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( 𝐵 ( 𝑆 D 𝐹 ) 𝑦 → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
115 114 exlimdv ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( ∃ 𝑦 𝐵 ( 𝑆 D 𝐹 ) 𝑦 → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) ) )
116 eldmg ⊢ ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) → ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ↔ ∃ 𝑦 𝐵 ( 𝑆 D 𝐹 ) 𝑦 ) )
117 116 ibi ⊢ ( 𝐵 ∈ dom ( 𝑆 D 𝐹 ) → ∃ 𝑦 𝐵 ( 𝑆 D 𝐹 ) 𝑦 )
118 115 117 impel ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ∧ 𝐵 ∈ dom ( 𝑆 D 𝐹 ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝐵 ) )