# Metamath Proof Explorer

## Theorem absnid

Description: A negative number is the negative of its own absolute value. (Contributed by NM, 27-Feb-2005)

Ref Expression
Assertion absnid ${⊢}\left({A}\in ℝ\wedge {A}\le 0\right)\to \left|{A}\right|=-{A}$

### Proof

Step Hyp Ref Expression
1 le0neg1 ${⊢}{A}\in ℝ\to \left({A}\le 0↔0\le -{A}\right)$
2 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
3 absneg ${⊢}{A}\in ℂ\to \left|-{A}\right|=\left|{A}\right|$
4 2 3 syl ${⊢}{A}\in ℝ\to \left|-{A}\right|=\left|{A}\right|$
5 4 adantr ${⊢}\left({A}\in ℝ\wedge 0\le -{A}\right)\to \left|-{A}\right|=\left|{A}\right|$
6 renegcl ${⊢}{A}\in ℝ\to -{A}\in ℝ$
7 absid ${⊢}\left(-{A}\in ℝ\wedge 0\le -{A}\right)\to \left|-{A}\right|=-{A}$
8 6 7 sylan ${⊢}\left({A}\in ℝ\wedge 0\le -{A}\right)\to \left|-{A}\right|=-{A}$
9 5 8 eqtr3d ${⊢}\left({A}\in ℝ\wedge 0\le -{A}\right)\to \left|{A}\right|=-{A}$
10 9 ex ${⊢}{A}\in ℝ\to \left(0\le -{A}\to \left|{A}\right|=-{A}\right)$
11 1 10 sylbid ${⊢}{A}\in ℝ\to \left({A}\le 0\to \left|{A}\right|=-{A}\right)$
12 11 imp ${⊢}\left({A}\in ℝ\wedge {A}\le 0\right)\to \left|{A}\right|=-{A}$