Theorem cjmul

Description: Complex conjugate distributes over multiplication. Proposition 10-3.4(c) of Gleason p. 133. (Contributed by NM, 29-Jul-1999) (Proof shortened by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Assertion	cjmul	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \overline{AB}=\bar{A}\bar{B}$$

Proof

Step	Hyp	Ref	Expression
1		remullem	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\Re \left(AB\right)=\Re \left(A\right)\Re \left(B\right)-\Im \left(A\right)\Im \left(B\right)\wedge \Im \left(AB\right)=\Re \left(A\right)\Im \left(B\right)+\Im \left(A\right)\Re \left(B\right)\wedge \overline{AB}=\bar{A}\bar{B}\right)$$
2	1	simp3d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \overline{AB}=\bar{A}\bar{B}$$