Description: Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005) (Revised by Mario Carneiro, 29-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | recl.1 | |- A e. CC |
|
readdi.2 | |- B e. CC |
||
Assertion | cjdivi | |- ( B =/= 0 -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recl.1 | |- A e. CC |
|
2 | readdi.2 | |- B e. CC |
|
3 | cjdiv | |- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) ) |
|
4 | 1 2 3 | mp3an12 | |- ( B =/= 0 -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) ) |