Metamath Proof Explorer


Theorem cjdivd

Description: Complex conjugate distributes over division. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses recld.1 φ A
readdd.2 φ B
cjdivd.2 φ B 0
Assertion cjdivd φ A B = A B

Proof

Step Hyp Ref Expression
1 recld.1 φ A
2 readdd.2 φ B
3 cjdivd.2 φ B 0
4 cjdiv A B B 0 A B = A B
5 1 2 3 4 syl3anc φ A B = A B