Step |
Hyp |
Ref |
Expression |
1 |
|
dvdivcncf.s |
|- ( ph -> S e. { RR , CC } ) |
2 |
|
dvdivcncf.f |
|- ( ph -> F : X --> CC ) |
3 |
|
dvdivcncf.g |
|- ( ph -> G : X --> ( CC \ { 0 } ) ) |
4 |
|
dvdivcncf.fdv |
|- ( ph -> ( S _D F ) e. ( X -cn-> CC ) ) |
5 |
|
dvdivcncf.gdv |
|- ( ph -> ( S _D G ) e. ( X -cn-> CC ) ) |
6 |
|
cncff |
|- ( ( S _D F ) e. ( X -cn-> CC ) -> ( S _D F ) : X --> CC ) |
7 |
|
fdm |
|- ( ( S _D F ) : X --> CC -> dom ( S _D F ) = X ) |
8 |
4 6 7
|
3syl |
|- ( ph -> dom ( S _D F ) = X ) |
9 |
|
cncff |
|- ( ( S _D G ) e. ( X -cn-> CC ) -> ( S _D G ) : X --> CC ) |
10 |
|
fdm |
|- ( ( S _D G ) : X --> CC -> dom ( S _D G ) = X ) |
11 |
5 9 10
|
3syl |
|- ( ph -> dom ( S _D G ) = X ) |
12 |
1 2 3 8 11
|
dvdivf |
|- ( ph -> ( S _D ( F oF / G ) ) = ( ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) oF / ( G oF x. G ) ) ) |
13 |
|
ax-resscn |
|- RR C_ CC |
14 |
|
sseq1 |
|- ( S = RR -> ( S C_ CC <-> RR C_ CC ) ) |
15 |
13 14
|
mpbiri |
|- ( S = RR -> S C_ CC ) |
16 |
|
eqimss |
|- ( S = CC -> S C_ CC ) |
17 |
15 16
|
pm3.2i |
|- ( ( S = RR -> S C_ CC ) /\ ( S = CC -> S C_ CC ) ) |
18 |
|
elpri |
|- ( S e. { RR , CC } -> ( S = RR \/ S = CC ) ) |
19 |
1 18
|
syl |
|- ( ph -> ( S = RR \/ S = CC ) ) |
20 |
|
pm3.44 |
|- ( ( ( S = RR -> S C_ CC ) /\ ( S = CC -> S C_ CC ) ) -> ( ( S = RR \/ S = CC ) -> S C_ CC ) ) |
21 |
17 19 20
|
mpsyl |
|- ( ph -> S C_ CC ) |
22 |
|
difssd |
|- ( ph -> ( CC \ { 0 } ) C_ CC ) |
23 |
3 22
|
fssd |
|- ( ph -> G : X --> CC ) |
24 |
|
dvbsss |
|- dom ( S _D F ) C_ S |
25 |
8 24
|
eqsstrrdi |
|- ( ph -> X C_ S ) |
26 |
|
dvcn |
|- ( ( ( S C_ CC /\ G : X --> CC /\ X C_ S ) /\ dom ( S _D G ) = X ) -> G e. ( X -cn-> CC ) ) |
27 |
21 23 25 11 26
|
syl31anc |
|- ( ph -> G e. ( X -cn-> CC ) ) |
28 |
4 27
|
mulcncff |
|- ( ph -> ( ( S _D F ) oF x. G ) e. ( X -cn-> CC ) ) |
29 |
|
dvcn |
|- ( ( ( S C_ CC /\ F : X --> CC /\ X C_ S ) /\ dom ( S _D F ) = X ) -> F e. ( X -cn-> CC ) ) |
30 |
21 2 25 8 29
|
syl31anc |
|- ( ph -> F e. ( X -cn-> CC ) ) |
31 |
5 30
|
mulcncff |
|- ( ph -> ( ( S _D G ) oF x. F ) e. ( X -cn-> CC ) ) |
32 |
28 31
|
subcncff |
|- ( ph -> ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) e. ( X -cn-> CC ) ) |
33 |
|
eldifi |
|- ( x e. ( CC \ { 0 } ) -> x e. CC ) |
34 |
33
|
adantr |
|- ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> x e. CC ) |
35 |
|
eldifi |
|- ( y e. ( CC \ { 0 } ) -> y e. CC ) |
36 |
35
|
adantl |
|- ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> y e. CC ) |
37 |
34 36
|
mulcld |
|- ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x x. y ) e. CC ) |
38 |
|
eldifsni |
|- ( x e. ( CC \ { 0 } ) -> x =/= 0 ) |
39 |
38
|
adantr |
|- ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> x =/= 0 ) |
40 |
|
eldifsni |
|- ( y e. ( CC \ { 0 } ) -> y =/= 0 ) |
41 |
40
|
adantl |
|- ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> y =/= 0 ) |
42 |
34 36 39 41
|
mulne0d |
|- ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x x. y ) =/= 0 ) |
43 |
|
eldifsn |
|- ( ( x x. y ) e. ( CC \ { 0 } ) <-> ( ( x x. y ) e. CC /\ ( x x. y ) =/= 0 ) ) |
44 |
37 42 43
|
sylanbrc |
|- ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x x. y ) e. ( CC \ { 0 } ) ) |
45 |
44
|
adantl |
|- ( ( ph /\ ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) ) -> ( x x. y ) e. ( CC \ { 0 } ) ) |
46 |
1 25
|
ssexd |
|- ( ph -> X e. _V ) |
47 |
|
inidm |
|- ( X i^i X ) = X |
48 |
45 3 3 46 46 47
|
off |
|- ( ph -> ( G oF x. G ) : X --> ( CC \ { 0 } ) ) |
49 |
27 27
|
mulcncff |
|- ( ph -> ( G oF x. G ) e. ( X -cn-> CC ) ) |
50 |
|
cncffvrn |
|- ( ( ( CC \ { 0 } ) C_ CC /\ ( G oF x. G ) e. ( X -cn-> CC ) ) -> ( ( G oF x. G ) e. ( X -cn-> ( CC \ { 0 } ) ) <-> ( G oF x. G ) : X --> ( CC \ { 0 } ) ) ) |
51 |
22 49 50
|
syl2anc |
|- ( ph -> ( ( G oF x. G ) e. ( X -cn-> ( CC \ { 0 } ) ) <-> ( G oF x. G ) : X --> ( CC \ { 0 } ) ) ) |
52 |
48 51
|
mpbird |
|- ( ph -> ( G oF x. G ) e. ( X -cn-> ( CC \ { 0 } ) ) ) |
53 |
32 52
|
divcncff |
|- ( ph -> ( ( ( ( S _D F ) oF x. G ) oF - ( ( S _D G ) oF x. F ) ) oF / ( G oF x. G ) ) e. ( X -cn-> CC ) ) |
54 |
12 53
|
eqeltrd |
|- ( ph -> ( S _D ( F oF / G ) ) e. ( X -cn-> CC ) ) |