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
|- ( A e. CC -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) = ( x e. ( CC \ { 0 } ) |-> -u ( A / ( x ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvfcn
 |-  ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) : dom ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) --> CC
2 ssidd
 |-  ( A e. CC -> CC C_ CC )
3 eldifsn
 |-  ( x e. ( CC \ { 0 } ) <-> ( x e. CC /\ x =/= 0 ) )
4 divcl
 |-  ( ( A e. CC /\ x e. CC /\ x =/= 0 ) -> ( A / x ) e. CC )
5 4 3expb
 |-  ( ( A e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( A / x ) e. CC )
6 3 5 sylan2b
 |-  ( ( A e. CC /\ x e. ( CC \ { 0 } ) ) -> ( A / x ) e. CC )
7 6 fmpttd
 |-  ( A e. CC -> ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) : ( CC \ { 0 } ) --> CC )
8 difssd
 |-  ( A e. CC -> ( CC \ { 0 } ) C_ CC )
9 2 7 8 dvbss
 |-  ( A e. CC -> dom ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) C_ ( CC \ { 0 } ) )
10 simpr
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> y e. ( CC \ { 0 } ) )
11 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
12 11 cnfldtop
 |-  ( TopOpen ` CCfld ) e. Top
13 11 cnfldhaus
 |-  ( TopOpen ` CCfld ) e. Haus
14 0cn
 |-  0 e. CC
15 unicntop
 |-  CC = U. ( TopOpen ` CCfld )
16 15 sncld
 |-  ( ( ( TopOpen ` CCfld ) e. Haus /\ 0 e. CC ) -> { 0 } e. ( Clsd ` ( TopOpen ` CCfld ) ) )
17 13 14 16 mp2an
 |-  { 0 } e. ( Clsd ` ( TopOpen ` CCfld ) )
18 15 cldopn
 |-  ( { 0 } e. ( Clsd ` ( TopOpen ` CCfld ) ) -> ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) )
19 17 18 ax-mp
 |-  ( CC \ { 0 } ) e. ( TopOpen ` CCfld )
20 isopn3i
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( CC \ { 0 } ) e. ( TopOpen ` CCfld ) ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` ( CC \ { 0 } ) ) = ( CC \ { 0 } ) )
21 12 19 20 mp2an
 |-  ( ( int ` ( TopOpen ` CCfld ) ) ` ( CC \ { 0 } ) ) = ( CC \ { 0 } )
22 10 21 eleqtrrdi
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> y e. ( ( int ` ( TopOpen ` CCfld ) ) ` ( CC \ { 0 } ) ) )
23 eldifi
 |-  ( y e. ( CC \ { 0 } ) -> y e. CC )
24 23 adantl
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> y e. CC )
25 24 sqvald
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( y ^ 2 ) = ( y x. y ) )
26 25 oveq2d
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( A / ( y ^ 2 ) ) = ( A / ( y x. y ) ) )
27 simpl
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> A e. CC )
28 eldifsni
 |-  ( y e. ( CC \ { 0 } ) -> y =/= 0 )
29 28 adantl
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> y =/= 0 )
30 27 24 24 29 29 divdiv1d
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( A / y ) / y ) = ( A / ( y x. y ) ) )
31 26 30 eqtr4d
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( A / ( y ^ 2 ) ) = ( ( A / y ) / y ) )
32 31 negeqd
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> -u ( A / ( y ^ 2 ) ) = -u ( ( A / y ) / y ) )
33 27 24 29 divcld
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( A / y ) e. CC )
34 33 24 29 divnegd
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> -u ( ( A / y ) / y ) = ( -u ( A / y ) / y ) )
35 32 34 eqtrd
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> -u ( A / ( y ^ 2 ) ) = ( -u ( A / y ) / y ) )
36 33 negcld
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> -u ( A / y ) e. CC )
37 eqid
 |-  ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) = ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) )
38 37 cdivcncf
 |-  ( -u ( A / y ) e. CC -> ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) )
39 36 38 syl
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) )
40 oveq2
 |-  ( z = y -> ( -u ( A / y ) / z ) = ( -u ( A / y ) / y ) )
41 39 10 40 cnmptlimc
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( -u ( A / y ) / y ) e. ( ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) limCC y ) )
42 35 41 eqeltrd
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> -u ( A / ( y ^ 2 ) ) e. ( ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) limCC y ) )
43 cncff
 |-  ( ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) e. ( ( CC \ { 0 } ) -cn-> CC ) -> ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) : ( CC \ { 0 } ) --> CC )
44 39 43 syl
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) : ( CC \ { 0 } ) --> CC )
45 44 limcdif
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) limCC y ) = ( ( ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) |` ( ( CC \ { 0 } ) \ { y } ) ) limCC y ) )
46 eldifi
 |-  ( z e. ( ( CC \ { 0 } ) \ { y } ) -> z e. ( CC \ { 0 } ) )
47 46 adantl
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> z e. ( CC \ { 0 } ) )
48 47 eldifad
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> z e. CC )
49 23 ad2antlr
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> y e. CC )
50 48 49 subcld
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( z - y ) e. CC )
51 33 adantr
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( A / y ) e. CC )
52 eldifsni
 |-  ( z e. ( CC \ { 0 } ) -> z =/= 0 )
53 47 52 syl
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> z =/= 0 )
54 51 48 53 divcld
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( A / y ) / z ) e. CC )
55 mulneg12
 |-  ( ( ( z - y ) e. CC /\ ( ( A / y ) / z ) e. CC ) -> ( -u ( z - y ) x. ( ( A / y ) / z ) ) = ( ( z - y ) x. -u ( ( A / y ) / z ) ) )
56 50 54 55 syl2anc
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( -u ( z - y ) x. ( ( A / y ) / z ) ) = ( ( z - y ) x. -u ( ( A / y ) / z ) ) )
57 49 48 54 subdird
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( y - z ) x. ( ( A / y ) / z ) ) = ( ( y x. ( ( A / y ) / z ) ) - ( z x. ( ( A / y ) / z ) ) ) )
58 48 49 negsubdi2d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> -u ( z - y ) = ( y - z ) )
59 58 oveq1d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( -u ( z - y ) x. ( ( A / y ) / z ) ) = ( ( y - z ) x. ( ( A / y ) / z ) ) )
60 oveq2
 |-  ( x = z -> ( A / x ) = ( A / z ) )
61 eqid
 |-  ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) = ( x e. ( CC \ { 0 } ) |-> ( A / x ) )
62 ovex
 |-  ( A / z ) e. _V
63 60 61 62 fvmpt
 |-  ( z e. ( CC \ { 0 } ) -> ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) = ( A / z ) )
64 47 63 syl
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) = ( A / z ) )
65 simpll
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> A e. CC )
66 28 ad2antlr
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> y =/= 0 )
67 65 49 66 divcan2d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( y x. ( A / y ) ) = A )
68 67 oveq1d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( y x. ( A / y ) ) / z ) = ( A / z ) )
69 49 51 48 53 divassd
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( y x. ( A / y ) ) / z ) = ( y x. ( ( A / y ) / z ) ) )
70 64 68 69 3eqtr2d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) = ( y x. ( ( A / y ) / z ) ) )
71 oveq2
 |-  ( x = y -> ( A / x ) = ( A / y ) )
72 ovex
 |-  ( A / y ) e. _V
73 71 61 72 fvmpt
 |-  ( y e. ( CC \ { 0 } ) -> ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) = ( A / y ) )
74 73 ad2antlr
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) = ( A / y ) )
75 51 48 53 divcan2d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( z x. ( ( A / y ) / z ) ) = ( A / y ) )
76 74 75 eqtr4d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) = ( z x. ( ( A / y ) / z ) ) )
77 70 76 oveq12d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) = ( ( y x. ( ( A / y ) / z ) ) - ( z x. ( ( A / y ) / z ) ) ) )
78 57 59 77 3eqtr4d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( -u ( z - y ) x. ( ( A / y ) / z ) ) = ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) )
79 51 48 53 divnegd
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> -u ( ( A / y ) / z ) = ( -u ( A / y ) / z ) )
80 79 oveq2d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( z - y ) x. -u ( ( A / y ) / z ) ) = ( ( z - y ) x. ( -u ( A / y ) / z ) ) )
81 56 78 80 3eqtr3d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) = ( ( z - y ) x. ( -u ( A / y ) / z ) ) )
82 81 oveq1d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) / ( z - y ) ) = ( ( ( z - y ) x. ( -u ( A / y ) / z ) ) / ( z - y ) ) )
83 51 negcld
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> -u ( A / y ) e. CC )
84 83 48 53 divcld
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( -u ( A / y ) / z ) e. CC )
85 eldifsni
 |-  ( z e. ( ( CC \ { 0 } ) \ { y } ) -> z =/= y )
86 85 adantl
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> z =/= y )
87 48 49 86 subne0d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( z - y ) =/= 0 )
88 84 50 87 divcan3d
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( ( z - y ) x. ( -u ( A / y ) / z ) ) / ( z - y ) ) = ( -u ( A / y ) / z ) )
89 82 88 eqtrd
 |-  ( ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) /\ z e. ( ( CC \ { 0 } ) \ { y } ) ) -> ( ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) / ( z - y ) ) = ( -u ( A / y ) / z ) )
90 89 mpteq2dva
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) / ( z - y ) ) ) = ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( -u ( A / y ) / z ) ) )
91 difss
 |-  ( ( CC \ { 0 } ) \ { y } ) C_ ( CC \ { 0 } )
92 resmpt
 |-  ( ( ( CC \ { 0 } ) \ { y } ) C_ ( CC \ { 0 } ) -> ( ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) |` ( ( CC \ { 0 } ) \ { y } ) ) = ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( -u ( A / y ) / z ) ) )
93 91 92 ax-mp
 |-  ( ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) |` ( ( CC \ { 0 } ) \ { y } ) ) = ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( -u ( A / y ) / z ) )
94 90 93 eqtr4di
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) / ( z - y ) ) ) = ( ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) |` ( ( CC \ { 0 } ) \ { y } ) ) )
95 94 oveq1d
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) / ( z - y ) ) ) limCC y ) = ( ( ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) |` ( ( CC \ { 0 } ) \ { y } ) ) limCC y ) )
96 45 95 eqtr4d
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( z e. ( CC \ { 0 } ) |-> ( -u ( A / y ) / z ) ) limCC y ) = ( ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) / ( z - y ) ) ) limCC y ) )
97 42 96 eleqtrd
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> -u ( A / ( y ^ 2 ) ) e. ( ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) / ( z - y ) ) ) limCC y ) )
98 11 cnfldtopon
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
99 98 toponrestid
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
100 eqid
 |-  ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) / ( z - y ) ) ) = ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) / ( z - y ) ) )
101 ssidd
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> CC C_ CC )
102 7 adantr
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) : ( CC \ { 0 } ) --> CC )
103 difssd
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( CC \ { 0 } ) C_ CC )
104 99 11 100 101 102 103 eldv
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( y ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) -u ( A / ( y ^ 2 ) ) <-> ( y e. ( ( int ` ( TopOpen ` CCfld ) ) ` ( CC \ { 0 } ) ) /\ -u ( A / ( y ^ 2 ) ) e. ( ( z e. ( ( CC \ { 0 } ) \ { y } ) |-> ( ( ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` z ) - ( ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ` y ) ) / ( z - y ) ) ) limCC y ) ) ) )
105 22 97 104 mpbir2and
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> y ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) -u ( A / ( y ^ 2 ) ) )
106 vex
 |-  y e. _V
107 negex
 |-  -u ( A / ( y ^ 2 ) ) e. _V
108 106 107 breldm
 |-  ( y ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) -u ( A / ( y ^ 2 ) ) -> y e. dom ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) )
109 105 108 syl
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> y e. dom ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) )
110 9 109 eqelssd
 |-  ( A e. CC -> dom ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) = ( CC \ { 0 } ) )
111 110 feq2d
 |-  ( A e. CC -> ( ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) : dom ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) --> CC <-> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) : ( CC \ { 0 } ) --> CC ) )
112 1 111 mpbii
 |-  ( A e. CC -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) : ( CC \ { 0 } ) --> CC )
113 112 ffnd
 |-  ( A e. CC -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) Fn ( CC \ { 0 } ) )
114 negex
 |-  -u ( A / ( x ^ 2 ) ) e. _V
115 114 rgenw
 |-  A. x e. ( CC \ { 0 } ) -u ( A / ( x ^ 2 ) ) e. _V
116 eqid
 |-  ( x e. ( CC \ { 0 } ) |-> -u ( A / ( x ^ 2 ) ) ) = ( x e. ( CC \ { 0 } ) |-> -u ( A / ( x ^ 2 ) ) )
117 116 fnmpt
 |-  ( A. x e. ( CC \ { 0 } ) -u ( A / ( x ^ 2 ) ) e. _V -> ( x e. ( CC \ { 0 } ) |-> -u ( A / ( x ^ 2 ) ) ) Fn ( CC \ { 0 } ) )
118 115 117 mp1i
 |-  ( A e. CC -> ( x e. ( CC \ { 0 } ) |-> -u ( A / ( x ^ 2 ) ) ) Fn ( CC \ { 0 } ) )
119 ffun
 |-  ( ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) : dom ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) --> CC -> Fun ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) )
120 1 119 mp1i
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> Fun ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) )
121 funbrfv
 |-  ( Fun ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) -> ( y ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) -u ( A / ( y ^ 2 ) ) -> ( ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) ` y ) = -u ( A / ( y ^ 2 ) ) ) )
122 120 105 121 sylc
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) ` y ) = -u ( A / ( y ^ 2 ) ) )
123 oveq1
 |-  ( x = y -> ( x ^ 2 ) = ( y ^ 2 ) )
124 123 oveq2d
 |-  ( x = y -> ( A / ( x ^ 2 ) ) = ( A / ( y ^ 2 ) ) )
125 124 negeqd
 |-  ( x = y -> -u ( A / ( x ^ 2 ) ) = -u ( A / ( y ^ 2 ) ) )
126 125 116 107 fvmpt
 |-  ( y e. ( CC \ { 0 } ) -> ( ( x e. ( CC \ { 0 } ) |-> -u ( A / ( x ^ 2 ) ) ) ` y ) = -u ( A / ( y ^ 2 ) ) )
127 126 adantl
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( x e. ( CC \ { 0 } ) |-> -u ( A / ( x ^ 2 ) ) ) ` y ) = -u ( A / ( y ^ 2 ) ) )
128 122 127 eqtr4d
 |-  ( ( A e. CC /\ y e. ( CC \ { 0 } ) ) -> ( ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) ` y ) = ( ( x e. ( CC \ { 0 } ) |-> -u ( A / ( x ^ 2 ) ) ) ` y ) )
129 113 118 128 eqfnfvd
 |-  ( A e. CC -> ( CC _D ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) ) = ( x e. ( CC \ { 0 } ) |-> -u ( A / ( x ^ 2 ) ) ) )