This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem absidm

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

Ref Expression
Assertion absidm ⊢ A ∈ ℂ → A = A

Proof

Step Hyp Ref Expression
1 abscl ⊢ A ∈ ℂ → A ∈ ℝ
2 absge0 ⊢ A ∈ ℂ → 0 ≤ A
3 absid ⊢ A ∈ ℝ ∧ 0 ≤ A → A = A
4 1 2 3 syl2anc ⊢ A ∈ ℂ → A = A