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 ) ) ) ) |