Metamath Proof Explorer

Theorem dvdivcncf

Description: A sufficient condition for the derivative of a quotient to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvdivcncf.s 
|- ( ph -> S e. { RR , CC } )
dvdivcncf.f 
|- ( ph -> F : X --> CC )
dvdivcncf.g 
|- ( ph -> G : X --> ( CC \ { 0 } ) )
dvdivcncf.fdv 
|- ( ph -> ( S _D F ) e. ( X -cn-> CC ) )
dvdivcncf.gdv 
|- ( ph -> ( S _D G ) e. ( X -cn-> CC ) )
Assertion dvdivcncf 
|- ( ph -> ( S _D ( F oF / G ) ) e. ( X -cn-> CC ) )

Proof

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