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 ⊢A∈ℝ→A=sgn⁡A⁢A

Proof

Step Hyp Ref Expression
1 rexr ⊢A∈ℝ→A∈ℝ*
2 sgnval ⊢A∈ℝ*→sgn⁡A=ifA=00ifA<0−11
3 1 2 syl ⊢A∈ℝ→sgn⁡A=ifA=00ifA<0−11
4 3 oveq1d ⊢A∈ℝ→sgn⁡A⁢A=ifA=00ifA<0−11⁢A
5 ovif ⊢ifA=00ifA<0−11⁢A=ifA=00⋅AifA<0−11⁢A
6 ovif ⊢ifA<0−11⁢A=ifA<0-1⁢A1⁢A
7 ifeq2 ⊢ifA<0−11⁢A=ifA<0-1⁢A1⁢A→ifA=00⋅AifA<0−11⁢A=ifA=00⋅AifA<0-1⁢A1⁢A
8 6 7 ax-mp ⊢ifA=00⋅AifA<0−11⁢A=ifA=00⋅AifA<0-1⁢A1⁢A
9 5 8 eqtri ⊢ifA=00ifA<0−11⁢A=ifA=00⋅AifA<0-1⁢A1⁢A
10 mul02lem2 ⊢A∈ℝ→0⋅A=0
11 10 adantr ⊢A∈ℝ∧A=0→0⋅A=0
12 simpr ⊢A∈ℝ∧A=0→A=0
13 12 abs00bd ⊢A∈ℝ∧A=0→A=0
14 11 13 eqtr4d ⊢A∈ℝ∧A=0→0⋅A=A
15 recn ⊢A∈ℝ→A∈ℂ
16 15 mulm1d ⊢A∈ℝ→-1⁢A=−A
17 15 mullidd ⊢A∈ℝ→1⁢A=A
18 16 17 ifeq12d ⊢A∈ℝ→ifA<0-1⁢A1⁢A=ifA<0−AA
19 reabsifneg ⊢A∈ℝ→A=ifA<0−AA
20 18 19 eqtr4d ⊢A∈ℝ→ifA<0-1⁢A1⁢A=A
21 20 adantr ⊢A∈ℝ∧¬A=0→ifA<0-1⁢A1⁢A=A
22 14 21 ifeqda ⊢A∈ℝ→ifA=00⋅AifA<0-1⁢A1⁢A=A
23 9 22 eqtrid ⊢A∈ℝ→ifA=00ifA<0−11⁢A=A
24 4 23 eqtr2d ⊢A∈ℝ→A=sgn⁡A⁢A