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