Metamath Proof Explorer

Theorem cjth

Description: The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013)

		Ref	Expression
	Assertion	cjth	$⊢ A \in ℂ \to (A + \overline{A} \in ℝ \land i (A - \overline{A}) \in ℝ)$

Proof

Step	Hyp	Ref	Expression
1		cju	$⊢ A \in ℂ \to \exists! x \in ℂ (A + x \in ℝ \land i (A - x) \in ℝ)$
2		riotasbc	$⊢ \exists! x \in ℂ (A + x \in ℝ \land i (A - x) \in ℝ) \to \underset{˙}{[} (ι x \in ℂ \| (A + x \in ℝ \land i (A - x) \in ℝ)) / x \underset{˙}{]} (A + x \in ℝ \land i (A - x) \in ℝ)$
3	1 2	syl	$⊢ A \in ℂ \to \underset{˙}{[} (ι x \in ℂ \| (A + x \in ℝ \land i (A - x) \in ℝ)) / x \underset{˙}{]} (A + x \in ℝ \land i (A - x) \in ℝ)$
4		cjval	$⊢ A \in ℂ \to \overline{A} = (ι x \in ℂ \| (A + x \in ℝ \land i (A - x) \in ℝ))$
5	4	sbceq1d	$⊢ A \in ℂ \to (\underset{˙}{[} \overline{A} / x \underset{˙}{]} (A + x \in ℝ \land i (A - x) \in ℝ) \leftrightarrow \underset{˙}{[} (ι x \in ℂ \| (A + x \in ℝ \land i (A - x) \in ℝ)) / x \underset{˙}{]} (A + x \in ℝ \land i (A - x) \in ℝ))$
6	3 5	mpbird	$⊢ A \in ℂ \to \underset{˙}{[} \overline{A} / x \underset{˙}{]} (A + x \in ℝ \land i (A - x) \in ℝ)$
7		fvex	$⊢ \overline{A} \in V$
8		oveq2	$⊢ x = \overline{A} \to A + x = A + \overline{A}$
9	8	eleq1d	$⊢ x = \overline{A} \to (A + x \in ℝ \leftrightarrow A + \overline{A} \in ℝ)$
10		oveq2	$⊢ x = \overline{A} \to A - x = A - \overline{A}$
11	10	oveq2d	$⊢ x = \overline{A} \to i (A - x) = i (A - \overline{A})$
12	11	eleq1d	$⊢ x = \overline{A} \to (i (A - x) \in ℝ \leftrightarrow i (A - \overline{A}) \in ℝ)$
13	9 12	anbi12d	$⊢ x = \overline{A} \to ((A + x \in ℝ \land i (A - x) \in ℝ) \leftrightarrow (A + \overline{A} \in ℝ \land i (A - \overline{A}) \in ℝ))$
14	7 13	sbcie	$⊢ \underset{˙}{[} \overline{A} / x \underset{˙}{]} (A + x \in ℝ \land i (A - x) \in ℝ) \leftrightarrow (A + \overline{A} \in ℝ \land i (A - \overline{A}) \in ℝ)$
15	6 14	sylib	$⊢ A \in ℂ \to (A + \overline{A} \in ℝ \land i (A - \overline{A}) \in ℝ)$