Metamath Proof Explorer

Theorem dvcnre

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

Ref Expression
Assertion dvcnre 
|- ( ( F : CC --> CC /\ RR C_ dom ( CC _D F ) ) -> ( RR _D ( F |` RR ) ) = ( ( CC _D F ) |` RR ) )

Proof

Step Hyp Ref Expression
1 reelprrecn 
 |-  RR e. { RR , CC }
2 1 a1i 
 |-  ( ( F : CC --> CC /\ RR C_ dom ( CC _D F ) ) -> RR e. { RR , CC } )
3 simpl 
 |-  ( ( F : CC --> CC /\ RR C_ dom ( CC _D F ) ) -> F : CC --> CC )
4 ssidd 
 |-  ( ( F : CC --> CC /\ RR C_ dom ( CC _D F ) ) -> CC C_ CC )
5 simpr 
 |-  ( ( F : CC --> CC /\ RR C_ dom ( CC _D F ) ) -> RR C_ dom ( CC _D F ) )
6 dvres3 
 |-  ( ( ( RR e. { RR , CC } /\ F : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D F ) ) ) -> ( RR _D ( F |` RR ) ) = ( ( CC _D F ) |` RR ) )
7 2 3 4 5 6 syl22anc 
 |-  ( ( F : CC --> CC /\ RR C_ dom ( CC _D F ) ) -> ( RR _D ( F |` RR ) ) = ( ( CC _D F ) |` RR ) )