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 = if A = 0 0 if A < 0 − 1 1
3 1 2 syl ⊢ A ∈ ℝ → sgn ⁡ A = if A = 0 0 if A < 0 − 1 1
4 3 oveq1d ⊢ A ∈ ℝ → sgn ⁡ A ⁢ A = if A = 0 0 if A < 0 − 1 1 ⁢ A
5 ovif ⊢ if A = 0 0 if A < 0 − 1 1 ⁢ A = if A = 0 0 ⋅ A if A < 0 − 1 1 ⁢ A
6 ovif ⊢ if A < 0 − 1 1 ⁢ A = if A < 0 -1 ⁢ A 1 ⁢ A
7 ifeq2 ⊢ if A < 0 − 1 1 ⁢ A = if A < 0 -1 ⁢ A 1 ⁢ A → if A = 0 0 ⋅ A if A < 0 − 1 1 ⁢ A = if A = 0 0 ⋅ A if A < 0 -1 ⁢ A 1 ⁢ A
8 6 7 ax-mp ⊢ if A = 0 0 ⋅ A if A < 0 − 1 1 ⁢ A = if A = 0 0 ⋅ A if A < 0 -1 ⁢ A 1 ⁢ A
9 5 8 eqtri ⊢ if A = 0 0 if A < 0 − 1 1 ⁢ A = if A = 0 0 ⋅ A if A < 0 -1 ⁢ A 1 ⁢ 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 mulid2d ⊢ A ∈ ℝ → 1 ⁢ A = A
18 16 17 ifeq12d ⊢ A ∈ ℝ → if A < 0 -1 ⁢ A 1 ⁢ A = if A < 0 − A A
19 reabsifneg ⊢ A ∈ ℝ → A = if A < 0 − A A
20 18 19 eqtr4d ⊢ A ∈ ℝ → if A < 0 -1 ⁢ A 1 ⁢ A = A
21 20 adantr ⊢ A ∈ ℝ ∧ ¬ A = 0 → if A < 0 -1 ⁢ A 1 ⁢ A = A
22 14 21 ifeqda ⊢ A ∈ ℝ → if A = 0 0 ⋅ A if A < 0 -1 ⁢ A 1 ⁢ A = A
23 9 22 syl5eq ⊢ A ∈ ℝ → if A = 0 0 if A < 0 − 1 1 ⁢ A = A
24 4 23 eqtr2d ⊢ A ∈ ℝ → A = sgn ⁡ A ⁢ A