This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvsubcncf

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

Ref Expression
Hypotheses dvsubcncf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvsubcncf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvsubcncf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
dvsubcncf.fdv ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
dvsubcncf.gdv ⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) ∈ ( 𝑋 –cn→ ℂ ) )
Assertion dvsubcncf ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f − 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 dvsubcncf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvsubcncf.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3 dvsubcncf.g ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
4 dvsubcncf.fdv ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) ∈ ( 𝑋 –cn→ ℂ ) )
5 dvsubcncf.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 dvsubf ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f − 𝐺 ) ) = ( ( 𝑆 D 𝐹 ) ∘f − ( 𝑆 D 𝐺 ) ) )
13 4 5 subcncff ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f − ( 𝑆 D 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
14 12 13 eqeltrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝐹 ∘f − 𝐺 ) ) ∈ ( 𝑋 –cn→ ℂ ) )