Theorem absimle

Description: The absolute value of a complex number is greater than or equal to the absolute value of its imaginary part. (Contributed by NM, 17-Mar-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		negicn	$$⊢-\mathrm{i}\in ℂ$$
2	1	a1i	$$⊢A\in ℂ\to -\mathrm{i}\in ℂ$$
3		id	$$⊢A\in ℂ\to A\in ℂ$$
4	2 3	mulcld	$$⊢A\in ℂ\to \left(-\mathrm{i}\right)A\in ℂ$$
5		absrele	$$⊢\left(-\mathrm{i}\right)A\in ℂ\to \left|\Re \left(\left(-\mathrm{i}\right)A\right)\right|\le \left|\left(-\mathrm{i}\right)A\right|$$
6	4 5	syl	$$⊢A\in ℂ\to \left|\Re \left(\left(-\mathrm{i}\right)A\right)\right|\le \left|\left(-\mathrm{i}\right)A\right|$$
7		imre	$$⊢A\in ℂ\to \Im \left(A\right)=\Re \left(\left(-\mathrm{i}\right)A\right)$$
8	7	fveq2d	$$⊢A\in ℂ\to \left|\Im \left(A\right)\right|=\left|\Re \left(\left(-\mathrm{i}\right)A\right)\right|$$
9		absmul	$$⊢\left(-\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \left|\left(-\mathrm{i}\right)A\right|=\left|-\mathrm{i}\right|\left|A\right|$$
10	1 9	mpan	$$⊢A\in ℂ\to \left|\left(-\mathrm{i}\right)A\right|=\left|-\mathrm{i}\right|\left|A\right|$$
11		ax-icn	$$⊢\mathrm{i}\in ℂ$$
12		absneg	$$⊢\mathrm{i}\in ℂ\to \left|-\mathrm{i}\right|=\left|\mathrm{i}\right|$$
13	11 12	ax-mp	$$⊢\left|-\mathrm{i}\right|=\left|\mathrm{i}\right|$$
14		absi	$$⊢\left|\mathrm{i}\right|=1$$
15	13 14	eqtri	$$⊢\left|-\mathrm{i}\right|=1$$
16	15	oveq1i	$$⊢\left|-\mathrm{i}\right|\left|A\right|=1\left|A\right|$$
17		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
18	17	recnd	$$⊢A\in ℂ\to \left|A\right|\in ℂ$$
19	18	mulid2d	$$⊢A\in ℂ\to 1\left|A\right|=\left|A\right|$$
20	16 19	syl5eq	$$⊢A\in ℂ\to \left|-\mathrm{i}\right|\left|A\right|=\left|A\right|$$
21	10 20	eqtr2d	$$⊢A\in ℂ\to \left|A\right|=\left|\left(-\mathrm{i}\right)A\right|$$
22	6 8 21	3brtr4d	$$⊢A\in ℂ\to \left|\Im \left(A\right)\right|\le \left|A\right|$$