Theorem absrele

Description: The absolute value of a complex number is greater than or equal to the absolute value of its real part. (Contributed by NM, 1-Apr-2005)

	Ref	Expression
Assertion	absrele	$$⊢A\in ℂ\to \left|\Re \left(A\right)\right|\le \left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		imcl	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$
2	1	sqge0d	$$⊢A\in ℂ\to 0\le {\Im \left(A\right)}^2$$
3		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
4	3	resqcld	$$⊢A\in ℂ\to {\Re \left(A\right)}^2\in ℝ$$
5	1	resqcld	$$⊢A\in ℂ\to {\Im \left(A\right)}^2\in ℝ$$
6	4 5	addge01d	$$⊢A\in ℂ\to \left(0\le {\Im \left(A\right)}^2\leftrightarrow {\Re \left(A\right)}^2\le {\Re \left(A\right)}^2+{\Im \left(A\right)}^2\right)$$
7	2 6	mpbid	$$⊢A\in ℂ\to {\Re \left(A\right)}^2\le {\Re \left(A\right)}^2+{\Im \left(A\right)}^2$$
8	3	sqge0d	$$⊢A\in ℂ\to 0\le {\Re \left(A\right)}^2$$
9	4 5	readdcld	$$⊢A\in ℂ\to {\Re \left(A\right)}^2+{\Im \left(A\right)}^2\in ℝ$$
10	4 5 8 2	addge0d	$$⊢A\in ℂ\to 0\le {\Re \left(A\right)}^2+{\Im \left(A\right)}^2$$
11		sqrtle	$$⊢\left(\left({\Re \left(A\right)}^2\in ℝ\wedge 0\le {\Re \left(A\right)}^2\right)\wedge \left({\Re \left(A\right)}^2+{\Im \left(A\right)}^2\in ℝ\wedge 0\le {\Re \left(A\right)}^2+{\Im \left(A\right)}^2\right)\right)\to \left({\Re \left(A\right)}^2\le {\Re \left(A\right)}^2+{\Im \left(A\right)}^2\leftrightarrow \sqrt{{\Re \left(A\right)}^2}\le \sqrt{{\Re \left(A\right)}^2+{\Im \left(A\right)}^2}\right)$$
12	4 8 9 10 11	syl22anc	$$⊢A\in ℂ\to \left({\Re \left(A\right)}^2\le {\Re \left(A\right)}^2+{\Im \left(A\right)}^2\leftrightarrow \sqrt{{\Re \left(A\right)}^2}\le \sqrt{{\Re \left(A\right)}^2+{\Im \left(A\right)}^2}\right)$$
13	7 12	mpbid	$$⊢A\in ℂ\to \sqrt{{\Re \left(A\right)}^2}\le \sqrt{{\Re \left(A\right)}^2+{\Im \left(A\right)}^2}$$
14		absre	$$⊢\Re \left(A\right)\in ℝ\to \left|\Re \left(A\right)\right|=\sqrt{{\Re \left(A\right)}^2}$$
15	3 14	syl	$$⊢A\in ℂ\to \left|\Re \left(A\right)\right|=\sqrt{{\Re \left(A\right)}^2}$$
16		absval2	$$⊢A\in ℂ\to \left|A\right|=\sqrt{{\Re \left(A\right)}^2+{\Im \left(A\right)}^2}$$
17	13 15 16	3brtr4d	$$⊢A\in ℂ\to \left|\Re \left(A\right)\right|\le \left|A\right|$$