Metamath Proof Explorer


Theorem imdivd

Description: Imaginary part of a division. Related to remul2 . (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses crred.1
|- ( ph -> A e. RR )
remul2d.2
|- ( ph -> B e. CC )
redivd.2
|- ( ph -> A =/= 0 )
Assertion imdivd
|- ( ph -> ( Im ` ( B / A ) ) = ( ( Im ` B ) / A ) )

Proof

Step Hyp Ref Expression
1 crred.1
 |-  ( ph -> A e. RR )
2 remul2d.2
 |-  ( ph -> B e. CC )
3 redivd.2
 |-  ( ph -> A =/= 0 )
4 imdiv
 |-  ( ( B e. CC /\ A e. RR /\ A =/= 0 ) -> ( Im ` ( B / A ) ) = ( ( Im ` B ) / A ) )
5 2 1 3 4 syl3anc
 |-  ( ph -> ( Im ` ( B / A ) ) = ( ( Im ` B ) / A ) )