Metamath Proof Explorer

Theorem dvcnvlem

Description: Lemma for dvcnvre . (Contributed by Mario Carneiro, 25-Feb-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses dvcnv.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
dvcnv.k ⊢ 𝐾 = ( 𝐽 ↾t 𝑆 )
dvcnv.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvcnv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
dvcnv.f ⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
dvcnv.i ⊢ ( 𝜑 → ◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) )
dvcnv.d ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
dvcnv.z ⊢ ( 𝜑 → ¬ 0 ∈ ran ( 𝑆 D 𝐹 ) )
dvcnv.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
Assertion dvcnvlem ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ( 𝑆 D ◡ 𝐹 ) ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 dvcnv.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 dvcnv.k ⊢ 𝐾 = ( 𝐽 ↾t 𝑆 )
3 dvcnv.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
4 dvcnv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
5 dvcnv.f ⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1-onto→ 𝑌 )
6 dvcnv.i ⊢ ( 𝜑 → ◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) )
7 dvcnv.d ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
8 dvcnv.z ⊢ ( 𝜑 → ¬ 0 ∈ ran ( 𝑆 D 𝐹 ) )
9 dvcnv.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
10 f1of ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
11 5 10 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
12 11 9 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ 𝑌 )
13 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
14 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
15 3 14 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
16 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
17 13 15 16 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
18 2 17 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑆 ) )
19 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑆 ) → 𝐾 ∈ Top )
20 18 19 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
21 isopn3i ⊢ ( ( 𝐾 ∈ Top ∧ 𝑌 ∈ 𝐾 ) → ( ( int ‘ 𝐾 ) ‘ 𝑌 ) = 𝑌 )
22 20 4 21 syl2anc ⊢ ( 𝜑 → ( ( int ‘ 𝐾 ) ‘ 𝑌 ) = 𝑌 )
23 12 22 eleqtrrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ 𝐾 ) ‘ 𝑌 ) )
24 f1ocnv ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 )
25 f1of ⊢ ( ◡ 𝐹 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
26 5 24 25 3syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝑌 ⟶ 𝑋 )
27 eldifi ⊢ ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) → 𝑧 ∈ 𝑌 )
28 ffvelrn ⊢ ( ( ◡ 𝐹 : 𝑌 ⟶ 𝑋 ∧ 𝑧 ∈ 𝑌 ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑋 )
29 26 27 28 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑋 )
30 29 anim1i ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) ∧ ( ◡ 𝐹 ‘ 𝑧 ) ≠ 𝐶 ) → ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑧 ) ≠ 𝐶 ) )
31 eldifsn ⊢ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( 𝑋 ∖ { 𝐶 } ) ↔ ( ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑋 ∧ ( ◡ 𝐹 ‘ 𝑧 ) ≠ 𝐶 ) )
32 30 31 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) ∧ ( ◡ 𝐹 ‘ 𝑧 ) ≠ 𝐶 ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( 𝑋 ∖ { 𝐶 } ) )
33 32 anasss ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ∧ ( ◡ 𝐹 ‘ 𝑧 ) ≠ 𝐶 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ( 𝑋 ∖ { 𝐶 } ) )
34 eldifi ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) → 𝑦 ∈ 𝑋 )
35 dvbsss ⊢ dom ( 𝑆 D 𝐹 ) ⊆ 𝑆
36 7 35 eqsstrrdi ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
37 36 15 sstrd ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
38 37 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ ℂ )
39 34 38 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝑦 ∈ ℂ )
40 36 9 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
41 15 40 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝐶 ∈ ℂ )
43 39 42 subcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( 𝑦 − 𝐶 ) ∈ ℂ )
44 toponss ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑆 ) ∧ 𝑌 ∈ 𝐾 ) → 𝑌 ⊆ 𝑆 )
45 18 4 44 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ 𝑆 )
46 45 15 sstrd ⊢ ( 𝜑 → 𝑌 ⊆ ℂ )
47 11 46 fssd ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
48 ffvelrn ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
49 47 34 48 syl2an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
50 46 12 sseldd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
52 49 51 subcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ∈ ℂ )
53 eldifsni ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) → 𝑦 ≠ 𝐶 )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝑦 ≠ 𝐶 )
55 49 51 subeq0ad ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) = 0 ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐶 ) ) )
56 f1of1 ⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 → 𝐹 : 𝑋 –1-1→ 𝑌 )
57 5 56 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 –1-1→ 𝑌 )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 )
59 34 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝑦 ∈ 𝑋 )
60 9 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → 𝐶 ∈ 𝑋 )
61 f1fveq ⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ ( 𝑦 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝑦 = 𝐶 ) )
62 58 59 60 61 syl12anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝑦 = 𝐶 ) )
63 55 62 bitrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) = 0 ↔ 𝑦 = 𝐶 ) )
64 63 necon3bid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ≠ 0 ↔ 𝑦 ≠ 𝐶 ) )
65 54 64 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ≠ 0 )
66 43 52 65 divcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( 𝑦 − 𝐶 ) / ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) ∈ ℂ )
67 limcresi ⊢ ( ◡ 𝐹 limℂ ( 𝐹 ‘ 𝐶 ) ) ⊆ ( ( ◡ 𝐹 ↾ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) limℂ ( 𝐹 ‘ 𝐶 ) )
68 26 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 f1ocnvfv1 ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐶 ∈ 𝑋 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) = 𝐶 )
77 5 9 76 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) = 𝐶 )
78 6 12 cnlimci ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) ∈ ( ◡ 𝐹 limℂ ( 𝐹 ‘ 𝐶 ) ) )
79 77 78 eqeltrrd ⊢ ( 𝜑 → 𝐶 ∈ ( ◡ 𝐹 limℂ ( 𝐹 ‘ 𝐶 ) ) )
80 75 79 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ↦ ( ◡ 𝐹 ‘ 𝑧 ) ) limℂ ( 𝐹 ‘ 𝐶 ) ) )
81 47 37 9 dvlem ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ∈ ℂ )
82 39 42 54 subne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( 𝑦 − 𝐶 ) ≠ 0 )
83 52 43 65 82 divne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ≠ 0 )
84 eldifsn ⊢ ( ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ∈ ℂ ∧ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ≠ 0 ) )
85 81 83 84 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ∈ ( ℂ ∖ { 0 } ) )
86 85 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) : ( 𝑋 ∖ { 𝐶 } ) ⟶ ( ℂ ∖ { 0 } ) )
87 difss ⊢ ( ℂ ∖ { 0 } ) ⊆ ℂ
88 87 a1i ⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
89 eqid ⊢ ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) = ( 𝐽 ↾t ( ℂ ∖ { 0 } ) )
90 9 7 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑆 D 𝐹 ) )
91 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
92 ffun ⊢ ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ → Fun ( 𝑆 D 𝐹 ) )
93 funfvbrb ⊢ ( Fun ( 𝑆 D 𝐹 ) → ( 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
94 3 91 92 93 4syl ⊢ ( 𝜑 → ( 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ↔ 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
95 90 94 mpbid ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) )
96 eqid ⊢ ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) = ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) )
97 2 1 96 15 47 36 eldv ⊢ ( 𝜑 → ( 𝐶 ( 𝑆 D 𝐹 ) ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ↔ ( 𝐶 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
98 95 97 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) limℂ 𝐶 ) ) )
99 98 simprd ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) limℂ 𝐶 ) )
100 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
101 13 87 100 mp2an ⊢ ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) )
102 101 a1i ⊢ ( 𝜑 → ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
103 13 a1i ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ℂ ) )
104 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
105 102 103 104 cnmptc ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ 1 ) ∈ ( ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) Cn 𝐽 ) )
106 102 cnmptid ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ 𝑥 ) ∈ ( ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) Cn ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) ) )
107 1 89 divcn ⊢ / ∈ ( ( 𝐽 ×t ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) ) Cn 𝐽 )
108 107 a1i ⊢ ( 𝜑 → / ∈ ( ( 𝐽 ×t ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) ) Cn 𝐽 ) )
109 102 105 106 108 cnmpt12f ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∈ ( ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) Cn 𝐽 ) )
110 3 91 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
111 7 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ↔ ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ ) )
112 110 111 mpbid ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
113 112 9 ffvelrnd ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ℂ )
114 110 ffnd ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) Fn dom ( 𝑆 D 𝐹 ) )
115 fnfvelrn ⊢ ( ( ( 𝑆 D 𝐹 ) Fn dom ( 𝑆 D 𝐹 ) ∧ 𝐶 ∈ dom ( 𝑆 D 𝐹 ) ) → ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ran ( 𝑆 D 𝐹 ) )
116 114 90 115 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ran ( 𝑆 D 𝐹 ) )
117 nelne2 ⊢ ( ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ran ( 𝑆 D 𝐹 ) ∧ ¬ 0 ∈ ran ( 𝑆 D 𝐹 ) ) → ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ≠ 0 )
118 116 8 117 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ≠ 0 )
119 eldifsn ⊢ ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ℂ ∧ ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ≠ 0 ) )
120 113 118 119 sylanbrc ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ( ℂ ∖ { 0 } ) )
121 101 toponunii ⊢ ( ℂ ∖ { 0 } ) = ∪ ( 𝐽 ↾t ( ℂ ∖ { 0 } ) )
122 121 cncnpi ⊢ ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∈ ( ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) Cn 𝐽 ) ∧ ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∈ ( ( ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) CnP 𝐽 ) ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
123 109 120 122 syl2anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∈ ( ( ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) CnP 𝐽 ) ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
124 86 88 1 89 99 123 limccnp ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ∈ ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∘ ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) ) limℂ 𝐶 ) )
125 oveq2 ⊢ ( 𝑥 = ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) → ( 1 / 𝑥 ) = ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
126 eqid ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) )
127 ovex ⊢ ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ∈ V
128 125 126 127 fvmpt ⊢ ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) = ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
129 120 128 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ‘ ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) = ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
130 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) = ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) )
131 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) )
132 oveq2 ⊢ ( 𝑥 = ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) → ( 1 / 𝑥 ) = ( 1 / ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) )
133 85 130 131 132 fmptco ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∘ ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) ) = ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( 1 / ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) ) )
134 52 43 65 82 recdivd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( 1 / ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) = ( ( 𝑦 − 𝐶 ) / ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) )
135 134 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( 1 / ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) ) = ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( 𝑦 − 𝐶 ) / ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) )
136 133 135 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∘ ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) ) = ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( 𝑦 − 𝐶 ) / ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) )
137 136 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑥 ) ) ∘ ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑦 − 𝐶 ) ) ) ) limℂ 𝐶 ) = ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( 𝑦 − 𝐶 ) / ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) limℂ 𝐶 ) )
138 124 129 137 3eltr3d ⊢ ( 𝜑 → ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ∈ ( ( 𝑦 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( 𝑦 − 𝐶 ) / ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) ) limℂ 𝐶 ) )
139 oveq1 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑧 ) → ( 𝑦 − 𝐶 ) = ( ( ◡ 𝐹 ‘ 𝑧 ) − 𝐶 ) )
140 fveq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑧 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) )
141 140 oveq1d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑧 ) → ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) − ( 𝐹 ‘ 𝐶 ) ) )
142 139 141 oveq12d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑧 ) → ( ( 𝑦 − 𝐶 ) / ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( ( ( ◡ 𝐹 ‘ 𝑧 ) − 𝐶 ) / ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) )
143 eldifsni ⊢ ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) → 𝑧 ≠ ( 𝐹 ‘ 𝐶 ) )
144 143 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → 𝑧 ≠ ( 𝐹 ‘ 𝐶 ) )
145 144 necomd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → ( 𝐹 ‘ 𝐶 ) ≠ 𝑧 )
146 f1ocnvfvb ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌 ) → ( ( 𝐹 ‘ 𝐶 ) = 𝑧 ↔ ( ◡ 𝐹 ‘ 𝑧 ) = 𝐶 ) )
147 5 9 27 146 syl2an3an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → ( ( 𝐹 ‘ 𝐶 ) = 𝑧 ↔ ( ◡ 𝐹 ‘ 𝑧 ) = 𝐶 ) )
148 147 necon3abid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → ( ( 𝐹 ‘ 𝐶 ) ≠ 𝑧 ↔ ¬ ( ◡ 𝐹 ‘ 𝑧 ) = 𝐶 ) )
149 145 148 mpbid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → ¬ ( ◡ 𝐹 ‘ 𝑧 ) = 𝐶 )
150 149 pm2.21d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) = 𝐶 → ( ( ( ◡ 𝐹 ‘ 𝑧 ) − 𝐶 ) / ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ) )
151 150 impr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ∧ ( ◡ 𝐹 ‘ 𝑧 ) = 𝐶 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) − 𝐶 ) / ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
152 33 66 80 138 142 151 limcco ⊢ ( 𝜑 → ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ↦ ( ( ( ◡ 𝐹 ‘ 𝑧 ) − 𝐶 ) / ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) ) limℂ ( 𝐹 ‘ 𝐶 ) ) )
153 77 eqcomd ⊢ ( 𝜑 → 𝐶 = ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) )
154 153 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → 𝐶 = ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) )
155 154 oveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → ( ( ◡ 𝐹 ‘ 𝑧 ) − 𝐶 ) = ( ( ◡ 𝐹 ‘ 𝑧 ) − ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) ) )
156 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ∧ 𝑧 ∈ 𝑌 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
157 5 27 156 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
158 157 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) − ( 𝐹 ‘ 𝐶 ) ) = ( 𝑧 − ( 𝐹 ‘ 𝐶 ) ) )
159 155 158 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ) → ( ( ( ◡ 𝐹 ‘ 𝑧 ) − 𝐶 ) / ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) = ( ( ( ◡ 𝐹 ‘ 𝑧 ) − ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) ) / ( 𝑧 − ( 𝐹 ‘ 𝐶 ) ) ) )
160 159 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ↦ ( ( ( ◡ 𝐹 ‘ 𝑧 ) − 𝐶 ) / ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ↦ ( ( ( ◡ 𝐹 ‘ 𝑧 ) − ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) ) / ( 𝑧 − ( 𝐹 ‘ 𝐶 ) ) ) ) )
161 160 oveq1d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ↦ ( ( ( ◡ 𝐹 ‘ 𝑧 ) − 𝐶 ) / ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) − ( 𝐹 ‘ 𝐶 ) ) ) ) limℂ ( 𝐹 ‘ 𝐶 ) ) = ( ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ↦ ( ( ( ◡ 𝐹 ‘ 𝑧 ) − ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) ) / ( 𝑧 − ( 𝐹 ‘ 𝐶 ) ) ) ) limℂ ( 𝐹 ‘ 𝐶 ) ) )
162 152 161 eleqtrd ⊢ ( 𝜑 → ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ↦ ( ( ( ◡ 𝐹 ‘ 𝑧 ) − ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) ) / ( 𝑧 − ( 𝐹 ‘ 𝐶 ) ) ) ) limℂ ( 𝐹 ‘ 𝐶 ) ) )
163 eqid ⊢ ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ↦ ( ( ( ◡ 𝐹 ‘ 𝑧 ) − ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) ) / ( 𝑧 − ( 𝐹 ‘ 𝐶 ) ) ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ↦ ( ( ( ◡ 𝐹 ‘ 𝑧 ) − ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) ) / ( 𝑧 − ( 𝐹 ‘ 𝐶 ) ) ) )
164 26 37 fssd ⊢ ( 𝜑 → ◡ 𝐹 : 𝑌 ⟶ ℂ )
165 2 1 163 15 164 45 eldv ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) ( 𝑆 D ◡ 𝐹 ) ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ↔ ( ( 𝐹 ‘ 𝐶 ) ∈ ( ( int ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { ( 𝐹 ‘ 𝐶 ) } ) ↦ ( ( ( ◡ 𝐹 ‘ 𝑧 ) − ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝐶 ) ) ) / ( 𝑧 − ( 𝐹 ‘ 𝐶 ) ) ) ) limℂ ( 𝐹 ‘ 𝐶 ) ) ) ) )
166 23 162 165 mpbir2and ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ( 𝑆 D ◡ 𝐹 ) ( 1 / ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )