Metamath Proof Explorer

Theorem dvcobrOLD

Description: Obsolete version of dvcobr 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 dvco.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvco.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
dvco.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑋 )
dvco.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑇 )
dvcobr.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
dvcobr.t ⊢ ( 𝜑 → 𝑇 ⊆ ℂ )
dvco.bf ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ( 𝑆 D 𝐹 ) 𝐾 )
dvco.bg ⊢ ( 𝜑 → 𝐶 ( 𝑇 D 𝐺 ) 𝐿 )
dvco.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion dvcobrOLD ( 𝜑 → 𝐶 ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ( 𝐾 · 𝐿 ) )

Proof

Step Hyp Ref Expression
1 dvco.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
2 dvco.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
3 dvco.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ 𝑋 )
4 dvco.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑇 )
5 dvcobr.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
6 dvcobr.t ⊢ ( 𝜑 → 𝑇 ⊆ ℂ )
7 dvco.bf ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ( 𝑆 D 𝐹 ) 𝐾 )
8 dvco.bg ⊢ ( 𝜑 → 𝐶 ( 𝑇 D 𝐺 ) 𝐿 )
9 dvco.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
10 eqid ⊢ ( 𝐽 ↾t 𝑇 ) = ( 𝐽 ↾t 𝑇 )
11 eqid ⊢ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
12 2 5 sstrd ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
13 3 12 fssd ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ℂ )
14 10 9 11 6 13 4 eldv ⊢ ( 𝜑 → ( 𝐶 ( 𝑇 D 𝐺 ) 𝐿 ↔ ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑇 ) ) ‘ 𝑌 ) ∧ 𝐿 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
15 8 14 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑇 ) ) ‘ 𝑌 ) ∧ 𝐿 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) )
16 15 simpld ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑇 ) ) ‘ 𝑌 ) )
17 5 1 2 dvcl ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝐶 ) ( 𝑆 D 𝐹 ) 𝐾 ) → 𝐾 ∈ ℂ )
18 7 17 mpdan ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → 𝐾 ∈ ℂ )
20 1 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝐹 : 𝑋 ⟶ ℂ )
21 eldifi ⊢ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) → 𝑧 ∈ 𝑌 )
22 ffvelcdm ⊢ ( ( 𝐺 : 𝑌 ⟶ 𝑋 ∧ 𝑧 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑋 )
23 3 21 22 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑋 )
24 20 23 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ℂ )
26 3 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝐺 : 𝑌 ⟶ 𝑋 )
27 6 13 4 dvbss ⊢ ( 𝜑 → dom ( 𝑇 D 𝐺 ) ⊆ 𝑌 )
28 reldv ⊢ Rel ( 𝑇 D 𝐺 )
29 releldm ⊢ ( ( Rel ( 𝑇 D 𝐺 ) ∧ 𝐶 ( 𝑇 D 𝐺 ) 𝐿 ) → 𝐶 ∈ dom ( 𝑇 D 𝐺 ) )
30 28 8 29 sylancr ⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑇 D 𝐺 ) )
31 27 30 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝑌 )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝐶 ∈ 𝑌 )
33 26 32 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝐶 ) ∈ 𝑋 )
34 20 33 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
36 25 35 subcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) ∈ ℂ )
37 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → 𝐺 : 𝑌 ⟶ ℂ )
38 21 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → 𝑧 ∈ 𝑌 )
39 37 38 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
40 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → 𝐶 ∈ 𝑌 )
41 37 40 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
42 39 41 subcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
43 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) )
44 39 41 subeq0ad ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) = 0 ↔ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) )
45 44 necon3abid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ≠ 0 ↔ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) )
46 43 45 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ≠ 0 )
47 36 42 46 divcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ∈ ℂ )
48 19 47 ifclda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ∈ ℂ )
49 4 6 sstrd ⊢ ( 𝜑 → 𝑌 ⊆ ℂ )
50 13 49 31 dvlem ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ )
51 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
52 9 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
53 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝐽 ∈ ( TopOn ‘ ℂ ) ) → ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) ) )
54 52 52 53 mp2an ⊢ ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) )
55 54 toponrestid ⊢ ( 𝐽 ×t 𝐽 ) = ( ( 𝐽 ×t 𝐽 ) ↾t ( ℂ × ℂ ) )
56 23 anim1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 𝐺 ‘ 𝐶 ) ) → ( ( 𝐺 ‘ 𝑧 ) ∈ 𝑋 ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 𝐺 ‘ 𝐶 ) ) )
57 eldifsn ⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↔ ( ( 𝐺 ‘ 𝑧 ) ∈ 𝑋 ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 𝐺 ‘ 𝐶 ) ) )
58 56 57 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 𝐺 ‘ 𝐶 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) )
59 58 anasss ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 𝐺 ‘ 𝐶 ) ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) )
60 eldifsni ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) → 𝑦 ≠ ( 𝐺 ‘ 𝐶 ) )
61 ifnefalse ⊢ ( 𝑦 ≠ ( 𝐺 ‘ 𝐶 ) → if ( 𝑦 = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) = ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) )
62 60 61 syl ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) → if ( 𝑦 = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) = ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) )
63 62 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ) → if ( 𝑦 = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) = ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) )
64 3 31 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ 𝑋 )
65 1 12 64 dvlem ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ∈ ℂ )
66 63 65 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ) → if ( 𝑦 = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) ∈ ℂ )
67 limcresi ⊢ ( 𝐺 limℂ 𝐶 ) ⊆ ( ( 𝐺 ↾ ( 𝑌 ∖ { 𝐶 } ) ) limℂ 𝐶 )
68 3 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ 𝑌 ↦ ( 𝐺 ‘ 𝑧 ) ) )
69 68 reseq1d ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝑌 ∖ { 𝐶 } ) ) = ( ( 𝑧 ∈ 𝑌 ↦ ( 𝐺 ‘ 𝑧 ) ) ↾ ( 𝑌 ∖ { 𝐶 } ) ) )
70 difss ⊢ ( 𝑌 ∖ { 𝐶 } ) ⊆ 𝑌
71 resmpt ⊢ ( ( 𝑌 ∖ { 𝐶 } ) ⊆ 𝑌 → ( ( 𝑧 ∈ 𝑌 ↦ ( 𝐺 ‘ 𝑧 ) ) ↾ ( 𝑌 ∖ { 𝐶 } ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( 𝐺 ‘ 𝑧 ) ) )
72 70 71 ax-mp ⊢ ( ( 𝑧 ∈ 𝑌 ↦ ( 𝐺 ‘ 𝑧 ) ) ↾ ( 𝑌 ∖ { 𝐶 } ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( 𝐺 ‘ 𝑧 ) )
73 69 72 eqtrdi ⊢ ( 𝜑 → ( 𝐺 ↾ ( 𝑌 ∖ { 𝐶 } ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( 𝐺 ‘ 𝑧 ) ) )
74 73 oveq1d ⊢ ( 𝜑 → ( ( 𝐺 ↾ ( 𝑌 ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( 𝐺 ‘ 𝑧 ) ) limℂ 𝐶 ) )
75 67 74 sseqtrid ⊢ ( 𝜑 → ( 𝐺 limℂ 𝐶 ) ⊆ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( 𝐺 ‘ 𝑧 ) ) limℂ 𝐶 ) )
76 eqid ⊢ ( 𝐽 ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 )
77 76 9 dvcnp2 ⊢ ( ( ( 𝑇 ⊆ ℂ ∧ 𝐺 : 𝑌 ⟶ ℂ ∧ 𝑌 ⊆ 𝑇 ) ∧ 𝐶 ∈ dom ( 𝑇 D 𝐺 ) ) → 𝐺 ∈ ( ( ( 𝐽 ↾t 𝑌 ) CnP 𝐽 ) ‘ 𝐶 ) )
78 6 13 4 30 77 syl31anc ⊢ ( 𝜑 → 𝐺 ∈ ( ( ( 𝐽 ↾t 𝑌 ) CnP 𝐽 ) ‘ 𝐶 ) )
79 9 76 cnplimc ⊢ ( ( 𝑌 ⊆ ℂ ∧ 𝐶 ∈ 𝑌 ) → ( 𝐺 ∈ ( ( ( 𝐽 ↾t 𝑌 ) CnP 𝐽 ) ‘ 𝐶 ) ↔ ( 𝐺 : 𝑌 ⟶ ℂ ∧ ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 limℂ 𝐶 ) ) ) )
80 49 31 79 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( ( 𝐽 ↾t 𝑌 ) CnP 𝐽 ) ‘ 𝐶 ) ↔ ( 𝐺 : 𝑌 ⟶ ℂ ∧ ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 limℂ 𝐶 ) ) ) )
81 78 80 mpbid ⊢ ( 𝜑 → ( 𝐺 : 𝑌 ⟶ ℂ ∧ ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 limℂ 𝐶 ) ) )
82 81 simprd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ ( 𝐺 limℂ 𝐶 ) )
83 75 82 sseldd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( 𝐺 ‘ 𝑧 ) ) limℂ 𝐶 ) )
84 eqid ⊢ ( 𝐽 ↾t 𝑆 ) = ( 𝐽 ↾t 𝑆 )
85 eqid ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) = ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) )
86 84 9 85 5 1 2 eldv ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐶 ) ( 𝑆 D 𝐹 ) 𝐾 ↔ ( ( 𝐺 ‘ 𝐶 ) ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ 𝐾 ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) limℂ ( 𝐺 ‘ 𝐶 ) ) ) ) )
87 7 86 mpbid ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐶 ) ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ 𝐾 ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) limℂ ( 𝐺 ‘ 𝐶 ) ) ) )
88 87 simprd ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) limℂ ( 𝐺 ‘ 𝐶 ) ) )
89 62 mpteq2ia ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↦ if ( 𝑦 = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) ) = ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) )
90 89 oveq1i ⊢ ( ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↦ if ( 𝑦 = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) ) limℂ ( 𝐺 ‘ 𝐶 ) ) = ( ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) limℂ ( 𝐺 ‘ 𝐶 ) )
91 88 90 eleqtrrdi ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { ( 𝐺 ‘ 𝐶 ) } ) ↦ if ( 𝑦 = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) ) limℂ ( 𝐺 ‘ 𝐶 ) ) )
92 eqeq1 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( 𝑦 = ( 𝐺 ‘ 𝐶 ) ↔ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) )
93 fveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) )
94 93 oveq1d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) )
95 oveq1 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) = ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) )
96 94 95 oveq12d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) )
97 92 96 ifbieq2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → if ( 𝑦 = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑦 − ( 𝐺 ‘ 𝐶 ) ) ) ) = if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) )
98 iftrue ⊢ ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) → if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) = 𝐾 )
99 98 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) ) → if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) = 𝐾 )
100 59 66 83 91 97 99 limcco ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) ) limℂ 𝐶 ) )
101 15 simprd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
102 9 mulcn ⊢ · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
103 6 13 4 dvcl ⊢ ( ( 𝜑 ∧ 𝐶 ( 𝑇 D 𝐺 ) 𝐿 ) → 𝐿 ∈ ℂ )
104 8 103 mpdan ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
105 18 104 opelxpd ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( ℂ × ℂ ) )
106 54 toponunii ⊢ ( ℂ × ℂ ) = ∪ ( 𝐽 ×t 𝐽 )
107 106 cncnpi ⊢ ( ( · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ∧ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( ℂ × ℂ ) ) → · ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ 𝐾 , 𝐿 ⟩ ) )
108 102 105 107 sylancr ⊢ ( 𝜑 → · ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ 𝐾 , 𝐿 ⟩ ) )
109 48 50 51 51 9 55 100 101 108 limccnp2 ⊢ ( 𝜑 → ( 𝐾 · 𝐿 ) ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) limℂ 𝐶 ) )
110 oveq1 ⊢ ( 𝐾 = if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) → ( 𝐾 · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
111 110 eqeq1d ⊢ ( 𝐾 = if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) → ( ( 𝐾 · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) ↔ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) ) )
112 oveq1 ⊢ ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) = if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) → ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
113 112 eqeq1d ⊢ ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) = if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) → ( ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) ↔ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) ) )
114 19 mul01d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐾 · 0 ) = 0 )
115 12 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝑋 ⊆ ℂ )
116 115 23 sseldd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
117 115 33 sseldd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
118 116 117 subeq0ad ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) = 0 ↔ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) )
119 118 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) = 0 )
120 119 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = ( 0 / ( 𝑧 − 𝐶 ) ) )
121 49 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝑌 ⊆ ℂ )
122 21 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝑧 ∈ 𝑌 )
123 121 122 sseldd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝑧 ∈ ℂ )
124 121 32 sseldd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝐶 ∈ ℂ )
125 123 124 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝑧 − 𝐶 ) ∈ ℂ )
126 eldifsni ⊢ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) → 𝑧 ≠ 𝐶 )
127 126 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → 𝑧 ≠ 𝐶 )
128 123 124 127 subne0d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 𝑧 − 𝐶 ) ≠ 0 )
129 125 128 div0d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( 0 / ( 𝑧 − 𝐶 ) ) = 0 )
130 129 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 0 / ( 𝑧 − 𝐶 ) ) = 0 )
131 120 130 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = 0 )
132 131 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐾 · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝐾 · 0 ) )
133 fveq2 ⊢ ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) )
134 24 34 subeq0ad ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) = 0 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) )
135 133 134 imbitrrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) = 0 ) )
136 135 imp ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) = 0 )
137 136 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) = ( 0 / ( 𝑧 − 𝐶 ) ) )
138 137 130 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) = 0 )
139 114 132 138 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝐾 · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) )
140 125 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝑧 − 𝐶 ) ∈ ℂ )
141 128 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( 𝑧 − 𝐶 ) ≠ 0 )
142 36 42 140 46 141 dmdcan2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) ∧ ¬ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) ) → ( ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) )
143 111 113 139 142 ifbothda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) )
144 fvco3 ⊢ ( ( 𝐺 : 𝑌 ⟶ 𝑋 ∧ 𝑧 ∈ 𝑌 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) )
145 3 21 144 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) )
146 fvco3 ⊢ ( ( 𝐺 : 𝑌 ⟶ 𝑋 ∧ 𝐶 ∈ 𝑌 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) )
147 3 31 146 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) )
148 147 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) )
149 145 148 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) = ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) )
150 149 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) )
151 143 150 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
152 151 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
153 152 oveq1d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( if ( ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐶 ) , 𝐾 , ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑧 ) ) − ( 𝐹 ‘ ( 𝐺 ‘ 𝐶 ) ) ) / ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) ) · ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
154 109 153 eleqtrd ⊢ ( 𝜑 → ( 𝐾 · 𝐿 ) ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
155 eqid ⊢ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
156 fco ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝐺 : 𝑌 ⟶ 𝑋 ) → ( 𝐹 ∘ 𝐺 ) : 𝑌 ⟶ ℂ )
157 1 3 156 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝑌 ⟶ ℂ )
158 10 9 155 6 157 4 eldv ⊢ ( 𝜑 → ( 𝐶 ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ( 𝐾 · 𝐿 ) ↔ ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑇 ) ) ‘ 𝑌 ) ∧ ( 𝐾 · 𝐿 ) ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘ 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
159 16 154 158 mpbir2and ⊢ ( 𝜑 → 𝐶 ( 𝑇 D ( 𝐹 ∘ 𝐺 ) ) ( 𝐾 · 𝐿 ) )