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