Metamath Proof Explorer

Theorem dvmulbrOLD

Description: Obsolete version of dvmulbr as of 10-Apr-2025. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses dvadd.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvadd.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
dvadd.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ℂ )
dvadd.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑆 )
dvaddbr.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
dvadd.bf ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐹 ) 𝐾 )
dvadd.bg ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐺 ) 𝐿 )
dvadd.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion dvmulbrOLD ( 𝜑 → 𝐶 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) + ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvadd.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
2 dvadd.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
3 dvadd.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ℂ )
4 dvadd.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑆 )
5 dvaddbr.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
6 dvadd.bf ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐹 ) 𝐾 )
7 dvadd.bg ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐺 ) 𝐿 )
8 dvadd.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
9 eqid ⊢ ( 𝐽 ↾t 𝑆 ) = ( 𝐽 ↾t 𝑆 )
10 eqid ⊢ ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
11 9 8 10 5 1 2 eldv ⊢ ( 𝜑 → ( 𝐶 ( 𝑆 D 𝐹 ) 𝐾 ↔ ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ 𝐾 ∈ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
12 6 11 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ 𝐾 ∈ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) )
13 12 simpld ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) )
14 eqid ⊢ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
15 9 8 14 5 3 4 eldv ⊢ ( 𝜑 → ( 𝐶 ( 𝑆 D 𝐺 ) 𝐿 ↔ ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ∧ 𝐿 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
16 7 15 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ∧ 𝐿 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) )
17 16 simpld ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) )
18 13 17 elind ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∩ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ) )
19 8 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
20 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
21 19 5 20 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
22 topontop ⊢ ( ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → ( 𝐽 ↾t 𝑆 ) ∈ Top )
23 21 22 syl ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ Top )
24 toponuni ⊢ ( ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) )
25 21 24 syl ⊢ ( 𝜑 → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) )
26 2 25 sseqtrd ⊢ ( 𝜑 → 𝑋 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
27 4 25 sseqtrd ⊢ ( 𝜑 → 𝑌 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
28 eqid ⊢ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ ( 𝐽 ↾t 𝑆 )
29 28 ntrin ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ 𝑋 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ∧ 𝑌 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ) → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∩ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ) )
30 23 26 27 29 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∩ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ) )
31 18 30 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
32 1 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐹 : 𝑋 ⟶ ℂ )
33 inss1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋
34 eldifi ⊢ ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) → 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) )
36 33 35 sselid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ∈ 𝑋 )
37 32 36 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
38 5 1 2 dvbss ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ 𝑋 )
39 reldv ⊢ Rel ( 𝑆 D 𝐹 )
40 releldm ⊢ ( ( Rel ( 𝑆 D 𝐹 ) ∧ 𝐶 ( 𝑆 D 𝐹 ) 𝐾 ) → 𝐶 ∈ dom ( 𝑆 D 𝐹 ) )
41 39 6 40 sylancr ⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑆 D 𝐹 ) )
42 38 41 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
43 1 42 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
45 37 44 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ∈ ℂ )
46 2 5 sstrd ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑋 ⊆ ℂ )
48 47 36 sseldd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ∈ ℂ )
49 46 42 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐶 ∈ ℂ )
51 48 50 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝑧 − 𝐶 ) ∈ ℂ )
52 eldifsni ⊢ ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) → 𝑧 ≠ 𝐶 )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ≠ 𝐶 )
54 48 50 53 subne0d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝑧 − 𝐶 ) ≠ 0 )
55 45 51 54 divcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ )
56 3 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐺 : 𝑌 ⟶ ℂ )
57 inss2 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌
58 57 35 sselid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ∈ 𝑌 )
59 56 58 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
60 55 59 mulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
61 ssdif ⊢ ( ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 → ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑌 ∖ { 𝐶 } ) )
62 57 61 mp1i ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑌 ∖ { 𝐶 } ) )
63 62 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) )
64 4 5 sstrd ⊢ ( 𝜑 → 𝑌 ⊆ ℂ )
65 5 3 4 dvbss ⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) ⊆ 𝑌 )
66 reldv ⊢ Rel ( 𝑆 D 𝐺 )
67 releldm ⊢ ( ( Rel ( 𝑆 D 𝐺 ) ∧ 𝐶 ( 𝑆 D 𝐺 ) 𝐿 ) → 𝐶 ∈ dom ( 𝑆 D 𝐺 ) )
68 66 7 67 sylancr ⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑆 D 𝐺 ) )
69 65 68 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝑌 )
70 3 64 69 dvlem ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ )
71 63 70 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ )
72 71 44 mulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ∈ ℂ )
73 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
74 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝐽 ∈ ( TopOn ‘ ℂ ) ) → ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) ) )
75 19 19 74 mp2an ⊢ ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) )
76 75 toponrestid ⊢ ( 𝐽 ×t 𝐽 ) = ( ( 𝐽 ×t 𝐽 ) ↾t ( ℂ × ℂ ) )
77 12 simprd ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
78 1 46 42 dvlem ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ )
79 78 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) : ( 𝑋 ∖ { 𝐶 } ) ⟶ ℂ )
80 ssdif ⊢ ( ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 → ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑋 ∖ { 𝐶 } ) )
81 33 80 mp1i ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑋 ∖ { 𝐶 } ) )
82 46 ssdifssd ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝐶 } ) ⊆ ℂ )
83 eqid ⊢ ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) )
84 33 2 sstrid ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑆 )
85 84 25 sseqtrd ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
86 difssd ⊢ ( 𝜑 → ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
87 85 86 unssd ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
88 ssun1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) )
89 88 a1i ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) )
90 28 ntrss ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ∧ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) )
91 23 87 89 90 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) )
92 91 31 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) )
93 92 42 elind ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) ∩ 𝑋 ) )
94 33 a1i ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 )
95 eqid ⊢ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) = ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 )
96 28 95 restntr ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ 𝑋 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ∧ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 ) → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) ∩ 𝑋 ) )
97 23 26 94 96 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) ∩ 𝑋 ) )
98 8 cnfldtop ⊢ 𝐽 ∈ Top
99 98 a1i ⊢ ( 𝜑 → 𝐽 ∈ Top )
100 cnex ⊢ ℂ ∈ V
101 ssexg ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
102 5 100 101 sylancl ⊢ ( 𝜑 → 𝑆 ∈ V )
103 restabs ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V ) → ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) = ( 𝐽 ↾t 𝑋 ) )
104 99 2 102 103 syl3anc ⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) = ( 𝐽 ↾t 𝑋 ) )
105 104 fveq2d ⊢ ( 𝜑 → ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) ) = ( int ‘ ( 𝐽 ↾t 𝑋 ) ) )
106 105 fveq1d ⊢ ( 𝜑 → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( int ‘ ( 𝐽 ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
107 97 106 eqtr3d ⊢ ( 𝜑 → ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) ∩ 𝑋 ) = ( ( int ‘ ( 𝐽 ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
108 93 107 eleqtrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
109 undif1 ⊢ ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) = ( 𝑋 ∪ { 𝐶 } )
110 42 snssd ⊢ ( 𝜑 → { 𝐶 } ⊆ 𝑋 )
111 ssequn2 ⊢ ( { 𝐶 } ⊆ 𝑋 ↔ ( 𝑋 ∪ { 𝐶 } ) = 𝑋 )
112 110 111 sylib ⊢ ( 𝜑 → ( 𝑋 ∪ { 𝐶 } ) = 𝑋 )
113 109 112 eqtrid ⊢ ( 𝜑 → ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) = 𝑋 )
114 113 oveq2d ⊢ ( 𝜑 → ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( 𝐽 ↾t 𝑋 ) )
115 114 fveq2d ⊢ ( 𝜑 → ( int ‘ ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) = ( int ‘ ( 𝐽 ↾t 𝑋 ) ) )
116 undif1 ⊢ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) = ( ( 𝑋 ∩ 𝑌 ) ∪ { 𝐶 } )
117 42 69 elind ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑋 ∩ 𝑌 ) )
118 117 snssd ⊢ ( 𝜑 → { 𝐶 } ⊆ ( 𝑋 ∩ 𝑌 ) )
119 ssequn2 ⊢ ( { 𝐶 } ⊆ ( 𝑋 ∩ 𝑌 ) ↔ ( ( 𝑋 ∩ 𝑌 ) ∪ { 𝐶 } ) = ( 𝑋 ∩ 𝑌 ) )
120 118 119 sylib ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∪ { 𝐶 } ) = ( 𝑋 ∩ 𝑌 ) )
121 116 120 eqtrid ⊢ ( 𝜑 → ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) = ( 𝑋 ∩ 𝑌 ) )
122 115 121 fveq12d ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) ‘ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( ( int ‘ ( 𝐽 ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
123 108 122 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) ‘ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) )
124 79 81 82 8 83 123 limcres ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
125 81 resmptd ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
126 125 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
127 124 126 eqtr3d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
128 77 127 eleqtrd ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
129 eqid ⊢ ( 𝐽 ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 )
130 129 8 dvcnp2 ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐺 : 𝑌 ⟶ ℂ ∧ 𝑌 ⊆ 𝑆 ) ∧ 𝐶 ∈ dom ( 𝑆 D 𝐺 ) ) → 𝐺 ∈ ( ( ( 𝐽 ↾t 𝑌 ) CnP 𝐽 ) ‘ 𝐶 ) )
131 5 3 4 68 130 syl31anc ⊢ ( 𝜑 → 𝐺 ∈ ( ( ( 𝐽 ↾t 𝑌 ) CnP 𝐽 ) ‘ 𝐶 ) )
132 8 129 cnplimc ⊢ ( ( 𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌 ) → ( 𝐺 ∈ ( ( ( 𝐽 ↾t 𝑌 ) CnP 𝐽 ) ‘ 𝐶 ) ↔ ( 𝐺 : 𝑌 ⟶ ℂ ∧ ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 limℂ 𝐶 ) ) ) )
133 64 69 132 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( ( 𝐽 ↾t 𝑌 ) CnP 𝐽 ) ‘ 𝐶 ) ↔ ( 𝐺 : 𝑌 ⟶ ℂ ∧ ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 limℂ 𝐶 ) ) ) )
134 131 133 mpbid ⊢ ( 𝜑 → ( 𝐺 : 𝑌 ⟶ ℂ ∧ ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 limℂ 𝐶 ) ) )
135 134 simprd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 limℂ 𝐶 ) )
136 difss ⊢ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑋 ∩ 𝑌 )
137 136 57 sstri ⊢ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ 𝑌
138 137 a1i ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ 𝑌 )
139 eqid ⊢ ( 𝐽 ↾t ( 𝑌 ∪ { 𝐶 } ) ) = ( 𝐽 ↾t ( 𝑌 ∪ { 𝐶 } ) )
140 difssd ⊢ ( 𝜑 → ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
141 85 140 unssd ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
142 ssun1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) )
143 142 a1i ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) )
144 28 ntrss ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ∧ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) )
145 23 141 143 144 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) )
146 145 31 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) )
147 146 69 elind ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
148 57 a1i ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 )
149 eqid ⊢ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) = ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 )
150 28 149 restntr ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ 𝑌 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ∧ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 ) → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
151 23 27 148 150 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
152 restabs ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V ) → ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 ) )
153 99 4 102 152 syl3anc ⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 ) )
154 153 fveq2d ⊢ ( 𝜑 → ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) ) = ( int ‘ ( 𝐽 ↾t 𝑌 ) ) )
155 154 fveq1d ⊢ ( 𝜑 → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
156 151 155 eqtr3d ⊢ ( 𝜑 → ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) ∩ 𝑌 ) = ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
157 147 156 eleqtrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
158 69 snssd ⊢ ( 𝜑 → { 𝐶 } ⊆ 𝑌 )
159 ssequn2 ⊢ ( { 𝐶 } ⊆ 𝑌 ↔ ( 𝑌 ∪ { 𝐶 } ) = 𝑌 )
160 158 159 sylib ⊢ ( 𝜑 → ( 𝑌 ∪ { 𝐶 } ) = 𝑌 )
161 160 oveq2d ⊢ ( 𝜑 → ( 𝐽 ↾t ( 𝑌 ∪ { 𝐶 } ) ) = ( 𝐽 ↾t 𝑌 ) )
162 161 fveq2d ⊢ ( 𝜑 → ( int ‘ ( 𝐽 ↾t ( 𝑌 ∪ { 𝐶 } ) ) ) = ( int ‘ ( 𝐽 ↾t 𝑌 ) ) )
163 162 121 fveq12d ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t ( 𝑌 ∪ { 𝐶 } ) ) ) ‘ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
164 157 163 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t ( 𝑌 ∪ { 𝐶 } ) ) ) ‘ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) )
165 3 138 64 8 139 164 limcres ⊢ ( 𝜑 → ( ( 𝐺 ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( 𝐺 limℂ 𝐶 ) )
166 3 138 feqresmpt ⊢ ( 𝜑 → ( 𝐺 ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( 𝐺 ‘ 𝑧 ) ) )
167 166 oveq1d ⊢ ( 𝜑 → ( ( 𝐺 ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( 𝐺 ‘ 𝑧 ) ) limℂ 𝐶 ) )
168 165 167 eqtr3d ⊢ ( 𝜑 → ( 𝐺 limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( 𝐺 ‘ 𝑧 ) ) limℂ 𝐶 ) )
169 135 168 eleqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( 𝐺 ‘ 𝑧 ) ) limℂ 𝐶 ) )
170 8 mulcn ⊢ · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
171 5 1 2 dvcl ⊢ ( ( 𝜑 ∧ 𝐶 ( 𝑆 D 𝐹 ) 𝐾 ) → 𝐾 ∈ ℂ )
172 6 171 mpdan ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
173 3 69 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
174 172 173 opelxpd ⊢ ( 𝜑 → ⟨ 𝐾 , ( 𝐺 ‘ 𝐶 ) ⟩ ∈ ( ℂ × ℂ ) )
175 75 toponunii ⊢ ( ℂ × ℂ ) = ∪ ( 𝐽 ×t 𝐽 )
176 175 cncnpi ⊢ ( ( · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ∧ ⟨ 𝐾 , ( 𝐺 ‘ 𝐶 ) ⟩ ∈ ( ℂ × ℂ ) ) → · ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ 𝐾 , ( 𝐺 ‘ 𝐶 ) ⟩ ) )
177 170 174 176 sylancr ⊢ ( 𝜑 → · ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ 𝐾 , ( 𝐺 ‘ 𝐶 ) ⟩ ) )
178 55 59 73 73 8 76 128 169 177 limccnp2 ⊢ ( 𝜑 → ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) ) limℂ 𝐶 ) )
179 16 simprd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
180 70 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) : ( 𝑌 ∖ { 𝐶 } ) ⟶ ℂ )
181 64 ssdifssd ⊢ ( 𝜑 → ( 𝑌 ∖ { 𝐶 } ) ⊆ ℂ )
182 eqid ⊢ ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) )
183 undif1 ⊢ ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) = ( 𝑌 ∪ { 𝐶 } )
184 183 160 eqtrid ⊢ ( 𝜑 → ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) = 𝑌 )
185 184 oveq2d ⊢ ( 𝜑 → ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( 𝐽 ↾t 𝑌 ) )
186 185 fveq2d ⊢ ( 𝜑 → ( int ‘ ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) = ( int ‘ ( 𝐽 ↾t 𝑌 ) ) )
187 186 121 fveq12d ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) ‘ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
188 157 187 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) ‘ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) )
189 180 62 181 8 182 188 limcres ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
190 62 resmptd ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
191 190 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
192 189 191 eqtr3d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
193 179 192 eleqtrd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
194 84 5 sstrd ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ ℂ )
195 cncfmptc ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ∈ ℂ ∧ ( 𝑋 ∩ 𝑌 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) ∈ ( ( 𝑋 ∩ 𝑌 ) –cn→ ℂ ) )
196 43 194 73 195 syl3anc ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) ∈ ( ( 𝑋 ∩ 𝑌 ) –cn→ ℂ ) )
197 eqidd ⊢ ( 𝑧 = 𝐶 → ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )
198 196 117 197 cnmptlimc ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) limℂ 𝐶 ) )
199 43 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
200 199 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) : ( 𝑋 ∩ 𝑌 ) ⟶ ℂ )
201 200 limcdif ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) limℂ 𝐶 ) = ( ( ( 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) )
202 resmpt ⊢ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑋 ∩ 𝑌 ) → ( ( 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( 𝐹 ‘ 𝐶 ) ) )
203 136 202 mp1i ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( 𝐹 ‘ 𝐶 ) ) )
204 203 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( 𝐹 ‘ 𝐶 ) ) limℂ 𝐶 ) )
205 201 204 eqtrd ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ↦ ( 𝐹 ‘ 𝐶 ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( 𝐹 ‘ 𝐶 ) ) limℂ 𝐶 ) )
206 198 205 eleqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( 𝐹 ‘ 𝐶 ) ) limℂ 𝐶 ) )
207 5 3 4 dvcl ⊢ ( ( 𝜑 ∧ 𝐶 ( 𝑆 D 𝐺 ) 𝐿 ) → 𝐿 ∈ ℂ )
208 7 207 mpdan ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
209 208 43 opelxpd ⊢ ( 𝜑 → ⟨ 𝐿 , ( 𝐹 ‘ 𝐶 ) ⟩ ∈ ( ℂ × ℂ ) )
210 175 cncnpi ⊢ ( ( · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ∧ ⟨ 𝐿 , ( 𝐹 ‘ 𝐶 ) ⟩ ∈ ( ℂ × ℂ ) ) → · ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ 𝐿 , ( 𝐹 ‘ 𝐶 ) ⟩ ) )
211 170 209 210 sylancr ⊢ ( 𝜑 → · ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ 𝐿 , ( 𝐹 ‘ 𝐶 ) ⟩ ) )
212 71 44 73 73 8 76 193 206 211 limccnp2 ⊢ ( 𝜑 → ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ) limℂ 𝐶 ) )
213 8 addcn ⊢ + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
214 172 173 mulcld ⊢ ( 𝜑 → ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
215 208 43 mulcld ⊢ ( 𝜑 → ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ∈ ℂ )
216 214 215 opelxpd ⊢ ( 𝜑 → ⟨ ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) , ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ⟩ ∈ ( ℂ × ℂ ) )
217 175 cncnpi ⊢ ( ( + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ∧ ⟨ ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) , ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ⟩ ∈ ( ℂ × ℂ ) ) → + ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) , ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ⟩ ) )
218 213 216 217 sylancr ⊢ ( 𝜑 → + ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) , ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ⟩ ) )
219 60 72 73 73 8 76 178 212 218 limccnp2 ⊢ ( 𝜑 → ( ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) + ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ) ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) + ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ) ) limℂ 𝐶 ) )
220 42 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐶 ∈ 𝑋 )
221 32 220 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
222 37 221 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ∈ ℂ )
223 222 59 mulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
224 69 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐶 ∈ 𝑌 )
225 56 224 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
226 59 225 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
227 226 221 mulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ∈ ℂ )
228 47 220 sseldd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐶 ∈ ℂ )
229 48 228 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝑧 − 𝐶 ) ∈ ℂ )
230 223 227 229 54 divdird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) + ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) / ( 𝑧 − 𝐶 ) ) + ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
231 37 59 mulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
232 221 59 mulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
233 221 225 mulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
234 231 232 233 npncand ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝑧 ) ) ) + ( ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) ) ) = ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) ) )
235 37 221 59 subdird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝑧 ) ) ) )
236 226 221 mulcomd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) = ( ( 𝐹 ‘ 𝐶 ) · ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) )
237 221 59 225 subdid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝐶 ) · ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) = ( ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) ) )
238 236 237 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) = ( ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) ) )
239 235 238 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) + ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ) = ( ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝑧 ) ) ) + ( ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) ) ) )
240 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
241 240 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐹 Fn 𝑋 )
242 3 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑌 )
243 242 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐺 Fn 𝑌 )
244 ssexg ⊢ ( ( 𝑋 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑋 ∈ V )
245 46 100 244 sylancl ⊢ ( 𝜑 → 𝑋 ∈ V )
246 245 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑋 ∈ V )
247 ssexg ⊢ ( ( 𝑌 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑌 ∈ V )
248 64 100 247 sylancl ⊢ ( 𝜑 → 𝑌 ∈ V )
249 248 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑌 ∈ V )
250 eqid ⊢ ( 𝑋 ∩ 𝑌 ) = ( 𝑋 ∩ 𝑌 )
251 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
252 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝑧 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
253 241 243 246 249 250 251 252 ofval ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) )
254 35 253 mpdan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) )
255 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝐶 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )
256 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝐶 ∈ 𝑌 ) → ( 𝐺 ‘ 𝐶 ) = ( 𝐺 ‘ 𝐶 ) )
257 241 243 246 249 250 255 256 ofval ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝐶 ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) = ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) )
258 117 257 mpidan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) = ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) )
259 254 258 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) · ( 𝐺 ‘ 𝐶 ) ) ) )
260 234 239 259 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) + ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ) = ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) ) )
261 260 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) + ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
262 222 59 229 54 div23d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) )
263 226 221 229 54 div23d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) )
264 262 263 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) / ( 𝑧 − 𝐶 ) ) + ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) + ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ) )
265 230 261 264 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) + ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ) )
266 265 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) + ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ) ) )
267 266 oveq1d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐺 ‘ 𝑧 ) ) + ( ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) · ( 𝐹 ‘ 𝐶 ) ) ) ) limℂ 𝐶 ) )
268 219 267 eleqtrrd ⊢ ( 𝜑 → ( ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) + ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ) ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
269 eqid ⊢ ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
270 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
271 270 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
272 271 1 3 245 248 250 off ⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) : ( 𝑋 ∩ 𝑌 ) ⟶ ℂ )
273 9 8 269 5 272 84 eldv ⊢ ( 𝜑 → ( 𝐶 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) + ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ) ↔ ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) ∧ ( ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) + ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ) ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
274 31 268 273 mpbir2and ⊢ ( 𝜑 → 𝐶 ( 𝑆 D ( 𝐹 ∘f · 𝐺 ) ) ( ( 𝐾 · ( 𝐺 ‘ 𝐶 ) ) + ( 𝐿 · ( 𝐹 ‘ 𝐶 ) ) ) )