Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvmulcncf Structured version   Unicode version

Theorem dvmulcncf 37103
 Description: A sufficient condition for the derivative of a product to be continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
dvmulcncf.s
dvmulcncf.f
dvmulcncf.g
dvmulcncf.fdv
dvmulcncf.gdv
Assertion
Ref Expression
dvmulcncf

Proof of Theorem dvmulcncf
StepHypRef Expression
1 dvmulcncf.s . . 3
2 dvmulcncf.f . . 3
3 dvmulcncf.g . . 3
4 dvmulcncf.fdv . . . 4
5 cncff 21691 . . . 4
6 fdm 5720 . . . 4
74, 5, 63syl 18 . . 3
8 dvmulcncf.gdv . . . 4
9 cncff 21691 . . . 4
10 fdm 5720 . . . 4
118, 9, 103syl 18 . . 3
121, 2, 3, 7, 11dvmulf 22640 . 2
13 ax-resscn 9581 . . . . . . . 8
14 sseq1 3465 . . . . . . . 8
1513, 14mpbiri 235 . . . . . . 7
16 eqimss 3496 . . . . . . 7
1715, 16pm3.2i 455 . . . . . 6
18 elpri 3994 . . . . . . 7
191, 18syl 17 . . . . . 6
20 pm3.44 511 . . . . . 6
2117, 19, 20mpsyl 64 . . . . 5
22 dvbsss 22600 . . . . . 6
237, 22syl6eqssr 3495 . . . . 5
24 dvcn 22618 . . . . 5
2521, 3, 23, 11, 24syl31anc 1235 . . . 4
264, 25mulcncff 37051 . . 3
27 dvcn 22618 . . . . 5
2821, 2, 23, 7, 27syl31anc 1235 . . . 4
298, 28mulcncff 37051 . . 3