Theorem 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\le A\bar{A}$$

Proof

Step	Hyp	Ref	Expression
1		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
2	1	resqcld	$$⊢A\in ℂ\to {\Re \left(A\right)}^2\in ℝ$$
3		imcl	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$
4	3	resqcld	$$⊢A\in ℂ\to {\Im \left(A\right)}^2\in ℝ$$
5	1	sqge0d	$$⊢A\in ℂ\to 0\le {\Re \left(A\right)}^2$$
6	3	sqge0d	$$⊢A\in ℂ\to 0\le {\Im \left(A\right)}^2$$
7	2 4 5 6	addge0d	$$⊢A\in ℂ\to 0\le {\Re \left(A\right)}^2+{\Im \left(A\right)}^2$$
8		cjmulval	$$⊢A\in ℂ\to A\bar{A}={\Re \left(A\right)}^2+{\Im \left(A\right)}^2$$
9	7 8	breqtrrd	$$⊢A\in ℂ\to 0\le A\bar{A}$$