Metamath Proof Explorer

Theorem sgnval2

Description: Value of the signum of a real number, expresssed using absolute value. (Contributed by Thierry Arnoux, 9-Nov-2025)

Ref Expression
Assertion sgnval2 ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( sgn ‘ 𝐴 ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ )
2 0red ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 ∈ ℝ )
3 1 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ∈ ℂ )
5 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ≠ 0 )
6 4 4 5 divneg2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → - ( 𝐴 / 𝐴 ) = ( 𝐴 / - 𝐴 ) )
7 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
8 3 7 dividd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 / 𝐴 ) = 1 )
9 8 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → ( 𝐴 / 𝐴 ) = 1 )
10 9 negeqd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → - ( 𝐴 / 𝐴 ) = - 1 )
11 6 10 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → ( 𝐴 / - 𝐴 ) = - 1 )
12 absnid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 )
13 12 adantlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 )
14 13 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → ( 𝐴 / ( abs ‘ 𝐴 ) ) = ( 𝐴 / - 𝐴 ) )
15 1 rexrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ* )
16 1 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ∈ ℝ )
17 0red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → 0 ∈ ℝ )
18 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 ≤ 0 )
19 7 necomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 ≠ 𝐴 )
20 19 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → 0 ≠ 𝐴 )
21 16 17 18 20 leneltd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → 𝐴 < 0 )
22 sgnn ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( sgn ‘ 𝐴 ) = - 1 )
23 15 21 22 syl2an2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → ( sgn ‘ 𝐴 ) = - 1 )
24 11 14 23 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐴 ≤ 0 ) → ( sgn ‘ 𝐴 ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )
25 8 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 0 ≤ 𝐴 ) → ( 𝐴 / 𝐴 ) = 1 )
26 1 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
27 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 0 ≤ 𝐴 ) → 0 ≤ 𝐴 )
28 26 27 absidd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
29 28 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 0 ≤ 𝐴 ) → ( 𝐴 / ( abs ‘ 𝐴 ) ) = ( 𝐴 / 𝐴 ) )
30 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 0 ≤ 𝐴 ) → 𝐴 ≠ 0 )
31 26 27 30 ne0gt0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 0 ≤ 𝐴 ) → 0 < 𝐴 )
32 sgnp ⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( sgn ‘ 𝐴 ) = 1 )
33 15 31 32 syl2an2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 0 ≤ 𝐴 ) → ( sgn ‘ 𝐴 ) = 1 )
34 25 29 33 3eqtr4rd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 0 ≤ 𝐴 ) → ( sgn ‘ 𝐴 ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )
35 1 2 24 34 lecasei ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( sgn ‘ 𝐴 ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )