cjmulge0

Description: A complex number times its conjugate is nonnegative. (Contributed by NM, 26-Mar-2005) (Revised by Mario Carneiro, 14-Jul-2014)

		Ref	Expression
	Assertion	cjmulge0	$⊢ A \in ℂ \to 0 \leq A \overline{A}$

Step	Hyp	Ref	Expression
1		recl	$⊢ A \in ℂ \to ℜ (A) \in ℝ$
2	1	resqcld	$⊢ A \in ℂ \to {ℜ (A)}^{2} \in ℝ$
3		imcl	$⊢ A \in ℂ \to ℑ (A) \in ℝ$
4	3	resqcld	$⊢ A \in ℂ \to {ℑ (A)}^{2} \in ℝ$
5	1	sqge0d	$⊢ A \in ℂ \to 0 \leq {ℜ (A)}^{2}$
6	3	sqge0d	$⊢ A \in ℂ \to 0 \leq {ℑ (A)}^{2}$
7	2 4 5 6	addge0d	$⊢ A \in ℂ \to 0 \leq {ℜ (A)}^{2} + {ℑ (A)}^{2}$
8		cjmulval	$⊢ A \in ℂ \to A \overline{A} = {ℜ (A)}^{2} + {ℑ (A)}^{2}$
9	7 8	breqtrrd	$⊢ A \in ℂ \to 0 \leq A \overline{A}$

Metamath Proof Explorer