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

Proof

Step Hyp Ref Expression
1 dvdivcncf.s φ S
2 dvdivcncf.f φ F : X
3 dvdivcncf.g φ G : X 0
4 dvdivcncf.fdv φ F S : X cn
5 dvdivcncf.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 dvdivf φ S D F ÷ f G = F S × f G f G S × f F ÷ f G × f G
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 difssd φ 0
23 3 22 fssd φ G : X
24 dvbsss dom F S S
25 8 24 eqsstrrdi φ X S
26 dvcn S G : X X S dom G S = X G : X cn
27 21 23 25 11 26 syl31anc φ G : X cn
28 4 27 mulcncff φ F S × f G : X cn
29 dvcn S F : X X S dom F S = X F : X cn
30 21 2 25 8 29 syl31anc φ F : X cn
31 5 30 mulcncff φ G S × f F : X cn
32 28 31 subcncff φ F S × f G f G S × f F : X cn
33 eldifi x 0 x
34 33 adantr x 0 y 0 x
35 eldifi y 0 y
36 35 adantl x 0 y 0 y
37 34 36 mulcld x 0 y 0 x y
38 eldifsni x 0 x 0
39 38 adantr x 0 y 0 x 0
40 eldifsni y 0 y 0
41 40 adantl x 0 y 0 y 0
42 34 36 39 41 mulne0d x 0 y 0 x y 0
43 eldifsn x y 0 x y x y 0
44 37 42 43 sylanbrc x 0 y 0 x y 0
45 44 adantl φ x 0 y 0 x y 0
46 1 25 ssexd φ X V
47 inidm X X = X
48 45 3 3 46 46 47 off φ G × f G : X 0
49 27 27 mulcncff φ G × f G : X cn
50 cncffvrn 0 G × f G : X cn G × f G : X cn 0 G × f G : X 0
51 22 49 50 syl2anc φ G × f G : X cn 0 G × f G : X 0
52 48 51 mpbird φ G × f G : X cn 0
53 32 52 divcncff φ F S × f G f G S × f F ÷ f G × f G : X cn
54 12 53 eqeltrd φ F ÷ f G S : X cn