Theorem dvcnre

Description: From compex differentiation to real differentiation. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	dvcnre	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ ℝ ⊆ dom ( ℂ D 𝐹 ) ) → ( ℝ D ( 𝐹 ↾ ℝ ) ) = ( ( ℂ D 𝐹 ) ↾ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
2	1	a1i	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ ℝ ⊆ dom ( ℂ D 𝐹 ) ) → ℝ ∈ { ℝ , ℂ } )
3		simpl	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ ℝ ⊆ dom ( ℂ D 𝐹 ) ) → 𝐹 : ℂ ⟶ ℂ )
4		ssidd	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ ℝ ⊆ dom ( ℂ D 𝐹 ) ) → ℂ ⊆ ℂ )
5		simpr	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ ℝ ⊆ dom ( ℂ D 𝐹 ) ) → ℝ ⊆ dom ( ℂ D 𝐹 ) )
6		dvres3	⊢ ( ( ( ℝ ∈ { ℝ , ℂ } ∧ 𝐹 : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ ℝ ⊆ dom ( ℂ D 𝐹 ) ) ) → ( ℝ D ( 𝐹 ↾ ℝ ) ) = ( ( ℂ D 𝐹 ) ↾ ℝ ) )
7	2 3 4 5 6	syl22anc	⊢ ( ( 𝐹 : ℂ ⟶ ℂ ∧ ℝ ⊆ dom ( ℂ D 𝐹 ) ) → ( ℝ D ( 𝐹 ↾ ℝ ) ) = ( ( ℂ D 𝐹 ) ↾ ℝ ) )