Metamath Proof Explorer

Theorem dvrec

Description: Derivative of the reciprocal function. (Contributed by Mario Carneiro, 25-Feb-2015) (Revised by Mario Carneiro, 28-Dec-2016)

Ref Expression
Assertion dvrec ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvfcn ⊢ ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) : dom ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) ⟶ ℂ
2 ssidd ⊢ ( 𝐴 ∈ ℂ → ℂ ⊆ ℂ )
3 eldifsn ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
4 divcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 𝐴 / 𝑥 ) ∈ ℂ )
5 4 3expb ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( 𝐴 / 𝑥 ) ∈ ℂ )
6 3 5 sylan2b ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 / 𝑥 ) ∈ ℂ )
7 6 fmpttd ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )
8 difssd ⊢ ( 𝐴 ∈ ℂ → ( ℂ ∖ { 0 } ) ⊆ ℂ )
9 2 7 8 dvbss ⊢ ( 𝐴 ∈ ℂ → dom ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) ⊆ ( ℂ ∖ { 0 } ) )
10 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ( ℂ ∖ { 0 } ) )
11 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
12 11 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
13 cnn0opn ⊢ ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld )
14 isopn3i ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld ) ) → ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ℂ ∖ { 0 } ) ) = ( ℂ ∖ { 0 } ) )
15 12 13 14 mp2an ⊢ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ℂ ∖ { 0 } ) ) = ( ℂ ∖ { 0 } )
16 10 15 eleqtrrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ℂ ∖ { 0 } ) ) )
17 eldifi ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ∈ ℂ )
18 17 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ℂ )
19 18 sqvald ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑦 ↑ 2 ) = ( 𝑦 · 𝑦 ) )
20 19 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 / ( 𝑦 ↑ 2 ) ) = ( 𝐴 / ( 𝑦 · 𝑦 ) ) )
21 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝐴 ∈ ℂ )
22 eldifsni ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ≠ 0 )
23 22 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ≠ 0 )
24 21 18 18 23 23 divdiv1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝐴 / 𝑦 ) / 𝑦 ) = ( 𝐴 / ( 𝑦 · 𝑦 ) ) )
25 20 24 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 / ( 𝑦 ↑ 2 ) ) = ( ( 𝐴 / 𝑦 ) / 𝑦 ) )
26 25 negeqd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → - ( 𝐴 / ( 𝑦 ↑ 2 ) ) = - ( ( 𝐴 / 𝑦 ) / 𝑦 ) )
27 21 18 23 divcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐴 / 𝑦 ) ∈ ℂ )
28 27 18 23 divnegd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → - ( ( 𝐴 / 𝑦 ) / 𝑦 ) = ( - ( 𝐴 / 𝑦 ) / 𝑦 ) )
29 26 28 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → - ( 𝐴 / ( 𝑦 ↑ 2 ) ) = ( - ( 𝐴 / 𝑦 ) / 𝑦 ) )
30 27 negcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → - ( 𝐴 / 𝑦 ) ∈ ℂ )
31 eqid ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) = ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) )
32 31 cdivcncf ⊢ ( - ( 𝐴 / 𝑦 ) ∈ ℂ → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )
33 30 32 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )
34 oveq2 ⊢ ( 𝑧 = 𝑦 → ( - ( 𝐴 / 𝑦 ) / 𝑧 ) = ( - ( 𝐴 / 𝑦 ) / 𝑦 ) )
35 33 10 34 cnmptlimc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( - ( 𝐴 / 𝑦 ) / 𝑦 ) ∈ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) limℂ 𝑦 ) )
36 29 35 eqeltrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → - ( 𝐴 / ( 𝑦 ↑ 2 ) ) ∈ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) limℂ 𝑦 ) )
37 cncff ⊢ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )
38 33 37 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )
39 38 limcdif ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) limℂ 𝑦 ) = ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) ↾ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) limℂ 𝑦 ) )
40 eldifi ⊢ ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) → 𝑧 ∈ ( ℂ ∖ { 0 } ) )
41 40 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → 𝑧 ∈ ( ℂ ∖ { 0 } ) )
42 41 eldifad ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → 𝑧 ∈ ℂ )
43 17 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → 𝑦 ∈ ℂ )
44 42 43 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( 𝑧 − 𝑦 ) ∈ ℂ )
45 27 adantr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( 𝐴 / 𝑦 ) ∈ ℂ )
46 eldifsni ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → 𝑧 ≠ 0 )
47 41 46 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → 𝑧 ≠ 0 )
48 45 42 47 divcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( 𝐴 / 𝑦 ) / 𝑧 ) ∈ ℂ )
49 mulneg12 ⊢ ( ( ( 𝑧 − 𝑦 ) ∈ ℂ ∧ ( ( 𝐴 / 𝑦 ) / 𝑧 ) ∈ ℂ ) → ( - ( 𝑧 − 𝑦 ) · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) = ( ( 𝑧 − 𝑦 ) · - ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) )
50 44 48 49 syl2anc ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( - ( 𝑧 − 𝑦 ) · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) = ( ( 𝑧 − 𝑦 ) · - ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) )
51 43 42 48 subdird ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( 𝑦 − 𝑧 ) · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) = ( ( 𝑦 · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) − ( 𝑧 · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) ) )
52 42 43 negsubdi2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → - ( 𝑧 − 𝑦 ) = ( 𝑦 − 𝑧 ) )
53 52 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( - ( 𝑧 − 𝑦 ) · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) = ( ( 𝑦 − 𝑧 ) · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) )
54 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐴 / 𝑥 ) = ( 𝐴 / 𝑧 ) )
55 eqid ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) )
56 ovex ⊢ ( 𝐴 / 𝑧 ) ∈ V
57 54 55 56 fvmpt ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) = ( 𝐴 / 𝑧 ) )
58 41 57 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) = ( 𝐴 / 𝑧 ) )
59 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → 𝐴 ∈ ℂ )
60 22 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → 𝑦 ≠ 0 )
61 59 43 60 divcan2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( 𝑦 · ( 𝐴 / 𝑦 ) ) = 𝐴 )
62 61 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( 𝑦 · ( 𝐴 / 𝑦 ) ) / 𝑧 ) = ( 𝐴 / 𝑧 ) )
63 43 45 42 47 divassd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( 𝑦 · ( 𝐴 / 𝑦 ) ) / 𝑧 ) = ( 𝑦 · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) )
64 58 62 63 3eqtr2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) = ( 𝑦 · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) )
65 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 / 𝑥 ) = ( 𝐴 / 𝑦 ) )
66 ovex ⊢ ( 𝐴 / 𝑦 ) ∈ V
67 65 55 66 fvmpt ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) = ( 𝐴 / 𝑦 ) )
68 67 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) = ( 𝐴 / 𝑦 ) )
69 45 42 47 divcan2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( 𝑧 · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) = ( 𝐴 / 𝑦 ) )
70 68 69 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) = ( 𝑧 · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) )
71 64 70 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) = ( ( 𝑦 · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) − ( 𝑧 · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) ) )
72 51 53 71 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( - ( 𝑧 − 𝑦 ) · ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) = ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) )
73 45 42 47 divnegd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → - ( ( 𝐴 / 𝑦 ) / 𝑧 ) = ( - ( 𝐴 / 𝑦 ) / 𝑧 ) )
74 73 oveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( 𝑧 − 𝑦 ) · - ( ( 𝐴 / 𝑦 ) / 𝑧 ) ) = ( ( 𝑧 − 𝑦 ) · ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) )
75 50 72 74 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) = ( ( 𝑧 − 𝑦 ) · ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) )
76 75 oveq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) / ( 𝑧 − 𝑦 ) ) = ( ( ( 𝑧 − 𝑦 ) · ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) / ( 𝑧 − 𝑦 ) ) )
77 45 negcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → - ( 𝐴 / 𝑦 ) ∈ ℂ )
78 77 42 47 divcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ∈ ℂ )
79 eldifsni ⊢ ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) → 𝑧 ≠ 𝑦 )
80 79 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → 𝑧 ≠ 𝑦 )
81 42 43 80 subne0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( 𝑧 − 𝑦 ) ≠ 0 )
82 78 44 81 divcan3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( ( 𝑧 − 𝑦 ) · ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) / ( 𝑧 − 𝑦 ) ) = ( - ( 𝐴 / 𝑦 ) / 𝑧 ) )
83 76 82 eqtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) → ( ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) / ( 𝑧 − 𝑦 ) ) = ( - ( 𝐴 / 𝑦 ) / 𝑧 ) )
84 83 mpteq2dva ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) / ( 𝑧 − 𝑦 ) ) ) = ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) )
85 difss ⊢ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ⊆ ( ℂ ∖ { 0 } )
86 resmpt ⊢ ( ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ⊆ ( ℂ ∖ { 0 } ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) ↾ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) = ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) )
87 85 86 ax-mp ⊢ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) ↾ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) = ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) )
88 84 87 eqtr4di ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) / ( 𝑧 − 𝑦 ) ) ) = ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) ↾ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) )
89 88 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) / ( 𝑧 − 𝑦 ) ) ) limℂ 𝑦 ) = ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) ↾ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ) limℂ 𝑦 ) )
90 39 89 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 𝐴 / 𝑦 ) / 𝑧 ) ) limℂ 𝑦 ) = ( ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) / ( 𝑧 − 𝑦 ) ) ) limℂ 𝑦 ) )
91 36 90 eleqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → - ( 𝐴 / ( 𝑦 ↑ 2 ) ) ∈ ( ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) / ( 𝑧 − 𝑦 ) ) ) limℂ 𝑦 ) )
92 11 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
93 92 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
94 eqid ⊢ ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) / ( 𝑧 − 𝑦 ) ) ) = ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) / ( 𝑧 − 𝑦 ) ) )
95 ssidd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ℂ ⊆ ℂ )
96 7 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )
97 difssd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ℂ ∖ { 0 } ) ⊆ ℂ )
98 93 11 94 95 96 97 eldv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑦 ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) - ( 𝐴 / ( 𝑦 ↑ 2 ) ) ↔ ( 𝑦 ∈ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ℂ ∖ { 0 } ) ) ∧ - ( 𝐴 / ( 𝑦 ↑ 2 ) ) ∈ ( ( 𝑧 ∈ ( ( ℂ ∖ { 0 } ) ∖ { 𝑦 } ) ↦ ( ( ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑧 ) − ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ‘ 𝑦 ) ) / ( 𝑧 − 𝑦 ) ) ) limℂ 𝑦 ) ) ) )
99 16 91 98 mpbir2and ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) - ( 𝐴 / ( 𝑦 ↑ 2 ) ) )
100 vex ⊢ 𝑦 ∈ V
101 negex ⊢ - ( 𝐴 / ( 𝑦 ↑ 2 ) ) ∈ V
102 100 101 breldm ⊢ ( 𝑦 ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) - ( 𝐴 / ( 𝑦 ↑ 2 ) ) → 𝑦 ∈ dom ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) )
103 99 102 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ dom ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) )
104 9 103 eqelssd ⊢ ( 𝐴 ∈ ℂ → dom ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) = ( ℂ ∖ { 0 } ) )
105 104 feq2d ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) : dom ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) ⟶ ℂ ↔ ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ ) )
106 1 105 mpbii ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ )
107 106 ffnd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) Fn ( ℂ ∖ { 0 } ) )
108 negex ⊢ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ∈ V
109 108 rgenw ⊢ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ∈ V
110 eqid ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) )
111 110 fnmpt ⊢ ( ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ∈ V → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ) Fn ( ℂ ∖ { 0 } ) )
112 109 111 mp1i ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ) Fn ( ℂ ∖ { 0 } ) )
113 ffun ⊢ ( ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) : dom ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) ⟶ ℂ → Fun ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) )
114 1 113 mp1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → Fun ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) )
115 funbrfv ⊢ ( Fun ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) → ( 𝑦 ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) - ( 𝐴 / ( 𝑦 ↑ 2 ) ) → ( ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) ‘ 𝑦 ) = - ( 𝐴 / ( 𝑦 ↑ 2 ) ) ) )
116 114 99 115 sylc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) ‘ 𝑦 ) = - ( 𝐴 / ( 𝑦 ↑ 2 ) ) )
117 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
118 117 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 / ( 𝑥 ↑ 2 ) ) = ( 𝐴 / ( 𝑦 ↑ 2 ) ) )
119 118 negeqd ⊢ ( 𝑥 = 𝑦 → - ( 𝐴 / ( 𝑥 ↑ 2 ) ) = - ( 𝐴 / ( 𝑦 ↑ 2 ) ) )
120 119 110 101 fvmpt ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ) ‘ 𝑦 ) = - ( 𝐴 / ( 𝑦 ↑ 2 ) ) )
121 120 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ) ‘ 𝑦 ) = - ( 𝐴 / ( 𝑦 ↑ 2 ) ) )
122 116 121 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ) ‘ 𝑦 ) )
123 107 112 122 eqfnfvd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 𝐴 / ( 𝑥 ↑ 2 ) ) ) )