Metamath Proof Explorer


Theorem reabsifnpos

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

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

Proof

Step Hyp Ref Expression
1 absnid ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 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 mpan ( 𝐴 ∈ ℝ → ( ¬ 𝐴 ≤ 0 → 0 ≤ 𝐴 ) )
8 7 imdistani ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ≤ 0 ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
9 absid ( ( 𝐴 ∈ ℝ ∧ 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 , - 𝐴 , 𝐴 ) )