Metamath Proof Explorer

Theorem reabssgn

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

Ref Expression
Assertion reabssgn ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) = ( ( sgn ‘ 𝐴 ) · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
2 sgnval ⊢ ( 𝐴 ∈ ℝ* → ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )
3 1 2 syl ⊢ ( 𝐴 ∈ ℝ → ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )
4 3 oveq1d ⊢ ( 𝐴 ∈ ℝ → ( ( sgn ‘ 𝐴 ) · 𝐴 ) = ( if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) · 𝐴 ) )
5 ovif ⊢ ( if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) · 𝐴 ) = if ( 𝐴 = 0 , ( 0 · 𝐴 ) , ( if ( 𝐴 < 0 , - 1 , 1 ) · 𝐴 ) )
6 ovif ⊢ ( if ( 𝐴 < 0 , - 1 , 1 ) · 𝐴 ) = if ( 𝐴 < 0 , ( - 1 · 𝐴 ) , ( 1 · 𝐴 ) )
7 ifeq2 ⊢ ( ( if ( 𝐴 < 0 , - 1 , 1 ) · 𝐴 ) = if ( 𝐴 < 0 , ( - 1 · 𝐴 ) , ( 1 · 𝐴 ) ) → if ( 𝐴 = 0 , ( 0 · 𝐴 ) , ( if ( 𝐴 < 0 , - 1 , 1 ) · 𝐴 ) ) = if ( 𝐴 = 0 , ( 0 · 𝐴 ) , if ( 𝐴 < 0 , ( - 1 · 𝐴 ) , ( 1 · 𝐴 ) ) ) )
8 6 7 ax-mp ⊢ if ( 𝐴 = 0 , ( 0 · 𝐴 ) , ( if ( 𝐴 < 0 , - 1 , 1 ) · 𝐴 ) ) = if ( 𝐴 = 0 , ( 0 · 𝐴 ) , if ( 𝐴 < 0 , ( - 1 · 𝐴 ) , ( 1 · 𝐴 ) ) )
9 5 8 eqtri ⊢ ( if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) · 𝐴 ) = if ( 𝐴 = 0 , ( 0 · 𝐴 ) , if ( 𝐴 < 0 , ( - 1 · 𝐴 ) , ( 1 · 𝐴 ) ) )
10 mul02lem2 ⊢ ( 𝐴 ∈ ℝ → ( 0 · 𝐴 ) = 0 )
11 10 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) → ( 0 · 𝐴 ) = 0 )
12 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) → 𝐴 = 0 )
13 12 abs00bd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) → ( abs ‘ 𝐴 ) = 0 )
14 11 13 eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) → ( 0 · 𝐴 ) = ( abs ‘ 𝐴 ) )
15 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
16 15 mulm1d ⊢ ( 𝐴 ∈ ℝ → ( - 1 · 𝐴 ) = - 𝐴 )
17 15 mulid2d ⊢ ( 𝐴 ∈ ℝ → ( 1 · 𝐴 ) = 𝐴 )
18 16 17 ifeq12d ⊢ ( 𝐴 ∈ ℝ → if ( 𝐴 < 0 , ( - 1 · 𝐴 ) , ( 1 · 𝐴 ) ) = if ( 𝐴 < 0 , - 𝐴 , 𝐴 ) )
19 reabsifneg ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) = if ( 𝐴 < 0 , - 𝐴 , 𝐴 ) )
20 18 19 eqtr4d ⊢ ( 𝐴 ∈ ℝ → if ( 𝐴 < 0 , ( - 1 · 𝐴 ) , ( 1 · 𝐴 ) ) = ( abs ‘ 𝐴 ) )
21 20 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 = 0 ) → if ( 𝐴 < 0 , ( - 1 · 𝐴 ) , ( 1 · 𝐴 ) ) = ( abs ‘ 𝐴 ) )
22 14 21 ifeqda ⊢ ( 𝐴 ∈ ℝ → if ( 𝐴 = 0 , ( 0 · 𝐴 ) , if ( 𝐴 < 0 , ( - 1 · 𝐴 ) , ( 1 · 𝐴 ) ) ) = ( abs ‘ 𝐴 ) )
23 9 22 syl5eq ⊢ ( 𝐴 ∈ ℝ → ( if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) · 𝐴 ) = ( abs ‘ 𝐴 ) )
24 4 23 eqtr2d ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ 𝐴 ) = ( ( sgn ‘ 𝐴 ) · 𝐴 ) )