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

Metamath Proof Explorer

Theorem absnid

Description: For a negative number, its absolute value is its negation. (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 ‘ 𝐴 ) = - 𝐴 )