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 ⊢ A ∈ ℝ ∧ A ≤ 0 → A = − A

Proof

Step Hyp Ref Expression
1 le0neg1 ⊢ A ∈ ℝ → A ≤ 0 ↔ 0 ≤ − A
2 recn ⊢ A ∈ ℝ → A ∈ ℂ
3 absneg ⊢ A ∈ ℂ → − A = A
4 2 3 syl ⊢ A ∈ ℝ → − A = A
5 4 adantr ⊢ A ∈ ℝ ∧ 0 ≤ − A → − A = A
6 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
7 absid ⊢ − A ∈ ℝ ∧ 0 ≤ − A → − A = − A
8 6 7 sylan ⊢ A ∈ ℝ ∧ 0 ≤ − A → − A = − A
9 5 8 eqtr3d ⊢ A ∈ ℝ ∧ 0 ≤ − A → A = − A
10 9 ex ⊢ A ∈ ℝ → 0 ≤ − A → A = − A
11 1 10 sylbid ⊢ A ∈ ℝ → A ≤ 0 → A = − A
12 11 imp ⊢ A ∈ ℝ ∧ A ≤ 0 → A = − A