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

Metamath Proof Explorer

Theorem dvcnre

Description: From complex 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 𝐹 ) ↾ ℝ ) )