Metamath Proof Explorer

Theorem dvmulcncf

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

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

Proof

Step Hyp Ref Expression
1 dvmulcncf.s 
 |-  ( ph -> S e. { RR , CC } )
2 dvmulcncf.f 
 |-  ( ph -> F : X --> CC )
3 dvmulcncf.g 
 |-  ( ph -> G : X --> CC )
4 dvmulcncf.fdv 
 |-  ( ph -> ( S _D F ) e. ( X -cn-> CC ) )
5 dvmulcncf.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 dvmulf 
 |-  ( ph -> ( S _D ( F oF x. G ) ) = ( ( ( S _D F ) oF x. G ) oF + ( ( S _D G ) oF x. F ) ) )
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 dvbsss 
 |-  dom ( S _D F ) C_ S
23 8 22 eqsstrrdi 
 |-  ( ph -> X C_ S )
24 dvcn 
 |-  ( ( ( S C_ CC /\ G : X --> CC /\ X C_ S ) /\ dom ( S _D G ) = X ) -> G e. ( X -cn-> CC ) )
25 21 3 23 11 24 syl31anc 
 |-  ( ph -> G e. ( X -cn-> CC ) )
26 4 25 mulcncff 
 |-  ( ph -> ( ( S _D F ) oF x. G ) e. ( X -cn-> CC ) )
27 dvcn 
 |-  ( ( ( S C_ CC /\ F : X --> CC /\ X C_ S ) /\ dom ( S _D F ) = X ) -> F e. ( X -cn-> CC ) )
28 21 2 23 8 27 syl31anc 
 |-  ( ph -> F e. ( X -cn-> CC ) )
29 5 28 mulcncff 
 |-  ( ph -> ( ( S _D G ) oF x. F ) e. ( X -cn-> CC ) )
30 26 29 addcncff 
 |-  ( ph -> ( ( ( S _D F ) oF x. G ) oF + ( ( S _D G ) oF x. F ) ) e. ( X -cn-> CC ) )
31 12 30 eqeltrd 
 |-  ( ph -> ( S _D ( F oF x. G ) ) e. ( X -cn-> CC ) )