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→ ℂ ) )