Theorem absnid

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

	Ref	Expression
Assertion	absnid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 )

Proof

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