Theorem absidm

Description: The absolute value function is idempotent. (Contributed by NM, 20-Nov-2004)

	Ref	Expression
Assertion	absidm	$$⊢A\in ℂ\to \left|\left|A\right|\right|=\left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
2		absge0	$$⊢A\in ℂ\to 0\le \left|A\right|$$
3		absid	$$⊢\left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)\to \left|\left|A\right|\right|=\left|A\right|$$
4	1 2 3	syl2anc	$$⊢A\in ℂ\to \left|\left|A\right|\right|=\left|A\right|$$