Metamath Proof Explorer


Theorem dvcnre

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

Ref Expression
Assertion dvcnre F : dom F D F = F

Proof

Step Hyp Ref Expression
1 reelprrecn
2 1 a1i F : dom F
3 simpl F : dom F F :
4 ssidd F : dom F
5 simpr F : dom F dom F
6 dvres3 F : dom F D F = F
7 2 3 4 5 6 syl22anc F : dom F D F = F