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 φ S
dvmulcncf.f φ F : X
dvmulcncf.g φ G : X
dvmulcncf.fdv φ F S : X cn
dvmulcncf.gdv φ G S : X cn
Assertion dvmulcncf φ F × f G S : X cn

Proof

Step Hyp Ref Expression
1 dvmulcncf.s φ S
2 dvmulcncf.f φ F : X
3 dvmulcncf.g φ G : X
4 dvmulcncf.fdv φ F S : X cn
5 dvmulcncf.gdv φ G S : X cn
6 cncff F S : X cn F S : X
7 fdm F S : X dom F S = X
8 4 6 7 3syl φ dom F S = X
9 cncff G S : X cn G S : X
10 fdm G S : X dom G S = X
11 5 9 10 3syl φ dom G S = X
12 1 2 3 8 11 dvmulf φ S D F × f G = F S × f G + f G S × f F
13 ax-resscn
14 sseq1 S = S
15 13 14 mpbiri S = S
16 eqimss S = S
17 15 16 pm3.2i S = S S = S
18 elpri S S = S =
19 1 18 syl φ S = S =
20 pm3.44 S = S S = S S = S = S
21 17 19 20 mpsyl φ S
22 dvbsss dom F S S
23 8 22 eqsstrrdi φ X S
24 dvcn S G : X X S dom G S = X G : X cn
25 21 3 23 11 24 syl31anc φ G : X cn
26 4 25 mulcncff φ F S × f G : X cn
27 dvcn S F : X X S dom F S = X F : X cn
28 21 2 23 8 27 syl31anc φ F : X cn
29 5 28 mulcncff φ G S × f F : X cn
30 26 29 addcncff φ F S × f G + f G S × f F : X cn
31 12 30 eqeltrd φ F × f G S : X cn