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 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvdivcncf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvdivcncf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
dvdivcncf.fdv ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
dvdivcncf.gdv ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
Assertion dvdivcncf ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f / 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 dvdivcncf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvdivcncf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3 dvdivcncf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
4 dvdivcncf.fdv ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
5 dvdivcncf.gdv ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
6 cncff ⊢ ( ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
7 fdm ⊢ ( ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ → dom ( 𝑆 D 𝐹 ) = 𝑋 )
8 4 6 7 3syl ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
9 cncff ⊢ ( ( 𝑆 D 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) → ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ )
10 fdm ⊢ ( ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ → dom ( 𝑆 D 𝐺 ) = 𝑋 )
11 5 9 10 3syl ⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
12 1 2 3 8 11 dvdivf ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f / 𝐺 ) ) = ( ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f − ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) ∘f / ( 𝐺 ∘f · 𝐺 ) ) )
13 ax-resscn ⊢ ℝ ⊆ ℂ
14 sseq1 ⊢ ( 𝑆 = ℝ → ( 𝑆 ⊆ ℂ ↔ ℝ ⊆ ℂ ) )
15 13 14 mpbiri ⊢ ( 𝑆 = ℝ → 𝑆 ⊆ ℂ )
16 eqimss ⊢ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ )
17 15 16 pm3.2i ⊢ ( ( 𝑆 = ℝ → 𝑆 ⊆ ℂ ) ∧ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ ) )
18 elpri ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
19 1 18 syl ⊢ ( 𝜑 → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
20 pm3.44 ⊢ ( ( ( 𝑆 = ℝ → 𝑆 ⊆ ℂ ) ∧ ( 𝑆 = ℂ → 𝑆 ⊆ ℂ ) ) → ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → 𝑆 ⊆ ℂ ) )
21 17 19 20 mpsyl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
22 difssd ⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
23 3 22 fssd ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
24 dvbsss ⊢ dom ( 𝑆 D 𝐹 ) ⊆ 𝑆
25 8 24 eqsstrrdi ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
26 dvcn ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐺 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐺 ) = 𝑋 ) → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )
27 21 23 25 11 26 syl31anc ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 –cn→ ℂ ) )
28 4 27 mulcncff ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
29 dvcn ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ 𝑆 ) ∧ dom ( 𝑆 D 𝐹 ) = 𝑋 ) → 𝐹 ∈ ( 𝑋 –cn→ ℂ ) )
30 21 2 25 8 29 syl31anc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 –cn→ ℂ ) )
31 5 30 mulcncff ⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
32 28 31 subcncff ⊢ ( 𝜑 → ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f − ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
33 eldifi ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ∈ ℂ )
34 33 adantr ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
35 eldifi ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ∈ ℂ )
36 35 adantl ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ℂ )
37 34 36 mulcld ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
38 eldifsni ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ≠ 0 )
39 38 adantr ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ≠ 0 )
40 eldifsni ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ≠ 0 )
41 40 adantl ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ≠ 0 )
42 34 36 39 41 mulne0d ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
43 eldifsn ⊢ ( ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑥 · 𝑦 ) ∈ ℂ ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
44 37 42 43 sylanbrc ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
45 44 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ) → ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
46 1 25 ssexd ⊢ ( 𝜑 → 𝑋 ∈ V )
47 inidm ⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋
48 45 3 3 46 46 47 off ⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐺 ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) )
49 27 27 mulcncff ⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
50 cncffvrn ⊢ ( ( ( ℂ ∖ { 0 } ) ⊆ ℂ ∧ ( 𝐺 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) ) → ( ( 𝐺 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐺 ∘f · 𝐺 ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) ) )
51 22 49 50 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ( ℂ ∖ { 0 } ) ) ↔ ( 𝐺 ∘f · 𝐺 ) : 𝑋 ⟶ ( ℂ ∖ { 0 } ) ) )
52 48 51 mpbird ⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐺 ) ∈ ( 𝑋 –cn→ ( ℂ ∖ { 0 } ) ) )
53 32 52 divcncff ⊢ ( 𝜑 → ( ( ( ( 𝑆 D 𝐹 ) ∘f · 𝐺 ) ∘f − ( ( 𝑆 D 𝐺 ) ∘f · 𝐹 ) ) ∘f / ( 𝐺 ∘f · 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
54 12 53 eqeltrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f / 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )