Metamath Proof Explorer

Theorem cjdiv

Description: Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

		Ref	Expression
	Assertion	cjdiv	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \overline{\frac{A}{B}} = \frac{\overline{A}}{\overline{B}}$

Proof

Step	Hyp	Ref	Expression
1		divcl	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} \in ℂ$
2		cjcl	$⊢ \frac{A}{B} \in ℂ \to \overline{\frac{A}{B}} \in ℂ$
3	1 2	syl	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \overline{\frac{A}{B}} \in ℂ$
4		simp2	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to B \in ℂ$
5		cjcl	$⊢ B \in ℂ \to \overline{B} \in ℂ$
6	4 5	syl	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \overline{B} \in ℂ$
7		simp3	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to B \neq 0$
8		cjne0	$⊢ B \in ℂ \to (B \neq 0 \leftrightarrow \overline{B} \neq 0)$
9	4 8	syl	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to (B \neq 0 \leftrightarrow \overline{B} \neq 0)$
10	7 9	mpbid	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \overline{B} \neq 0$
11	3 6 10	divcan4d	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{\overline{\frac{A}{B}} \overline{B}}{\overline{B}} = \overline{\frac{A}{B}}$
12		cjmul	$⊢ (\frac{A}{B} \in ℂ \land B \in ℂ) \to \overline{(\frac{A}{B}) B} = \overline{\frac{A}{B}} \overline{B}$
13	1 4 12	syl2anc	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \overline{(\frac{A}{B}) B} = \overline{\frac{A}{B}} \overline{B}$
14		divcan1	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to (\frac{A}{B}) B = A$
15	14	fveq2d	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \overline{(\frac{A}{B}) B} = \overline{A}$
16	13 15	eqtr3d	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \overline{\frac{A}{B}} \overline{B} = \overline{A}$
17	16	oveq1d	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{\overline{\frac{A}{B}} \overline{B}}{\overline{B}} = \frac{\overline{A}}{\overline{B}}$
18	11 17	eqtr3d	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \overline{\frac{A}{B}} = \frac{\overline{A}}{\overline{B}}$