Metamath Proof Explorer


Theorem reabsifneg

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

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

Proof

Step Hyp Ref Expression
1 0re 0 ∈ ℝ
2 ltle ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 < 0 → 𝐴 ≤ 0 ) )
3 1 2 mpan2 ( 𝐴 ∈ ℝ → ( 𝐴 < 0 → 𝐴 ≤ 0 ) )
4 3 imdistani ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) )
5 absnid ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 )
6 4 5 syl ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 )
7 6 eqcomd ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → - 𝐴 = ( abs ‘ 𝐴 ) )
8 0red ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
9 id ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
10 8 9 lenltd ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ ¬ 𝐴 < 0 ) )
11 10 bicomd ( 𝐴 ∈ ℝ → ( ¬ 𝐴 < 0 ↔ 0 ≤ 𝐴 ) )
12 11 pm5.32i ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 < 0 ) ↔ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
13 absid ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
14 12 13 sylbi ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 < 0 ) → ( abs ‘ 𝐴 ) = 𝐴 )
15 14 eqcomd ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 < 0 ) → 𝐴 = ( abs ‘ 𝐴 ) )
16 7 15 ifeqda ( 𝐴 ∈ ℝ → if ( 𝐴 < 0 , - 𝐴 , 𝐴 ) = ( abs ‘ 𝐴 ) )
17 16 eqcomd ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) = if ( 𝐴 < 0 , - 𝐴 , 𝐴 ) )