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