Metamath Proof Explorer


Theorem reabsifnneg

Description: Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024)

Ref Expression
Assertion reabsifnneg ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) = if ( 0 ≤ 𝐴 , 𝐴 , - 𝐴 ) )

Proof

Step Hyp Ref Expression
1 absid ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
2 1 eqcomd ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 = ( abs ‘ 𝐴 ) )
3 0re 0 ∈ ℝ
4 ltnle ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 < 0 ↔ ¬ 0 ≤ 𝐴 ) )
5 ltle ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 < 0 → 𝐴 ≤ 0 ) )
6 4 5 sylbird ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( ¬ 0 ≤ 𝐴𝐴 ≤ 0 ) )
7 3 6 mpan2 ( 𝐴 ∈ ℝ → ( ¬ 0 ≤ 𝐴𝐴 ≤ 0 ) )
8 7 imdistani ( ( 𝐴 ∈ ℝ ∧ ¬ 0 ≤ 𝐴 ) → ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) )
9 absnid ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 )
10 8 9 syl ( ( 𝐴 ∈ ℝ ∧ ¬ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = - 𝐴 )
11 10 eqcomd ( ( 𝐴 ∈ ℝ ∧ ¬ 0 ≤ 𝐴 ) → - 𝐴 = ( abs ‘ 𝐴 ) )
12 2 11 ifeqda ( 𝐴 ∈ ℝ → if ( 0 ≤ 𝐴 , 𝐴 , - 𝐴 ) = ( abs ‘ 𝐴 ) )
13 12 eqcomd ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) = if ( 0 ≤ 𝐴 , 𝐴 , - 𝐴 ) )