Metamath Proof Explorer

Theorem sgnneg

Description: Negation of the signum. (Contributed by Thierry Arnoux, 1-Oct-2018)

Ref Expression
Assertion sgnneg ( 𝐴 ∈ ℝ → ( sgn ‘ - 𝐴 ) = - ( sgn ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 1 negeq0d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 = 0 ↔ - 𝐴 = 0 ) )
3 2 bicomd ⊢ ( 𝐴 ∈ ℝ → ( - 𝐴 = 0 ↔ 𝐴 = 0 ) )
4 eqidd ⊢ ( ( 𝐴 ∈ ℝ ∧ - 𝐴 = 0 ) → 0 = 0 )
5 3 necon3bbid ⊢ ( 𝐴 ∈ ℝ → ( ¬ - 𝐴 = 0 ↔ 𝐴 ≠ 0 ) )
6 5 biimpa ⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ - 𝐴 = 0 ) → 𝐴 ≠ 0 )
7 lt0neg2 ⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ - 𝐴 < 0 ) )
8 7 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 0 < 𝐴 ↔ - 𝐴 < 0 ) )
9 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
10 0red ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
11 9 10 lttri2d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≠ 0 ↔ ( 𝐴 < 0 ∨ 0 < 𝐴 ) ) )
12 11 biimpa ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 < 0 ∨ 0 < 𝐴 ) )
13 ltnsym2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ¬ ( 𝐴 < 0 ∧ 0 < 𝐴 ) )
14 10 13 mpdan ⊢ ( 𝐴 ∈ ℝ → ¬ ( 𝐴 < 0 ∧ 0 < 𝐴 ) )
15 14 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ¬ ( 𝐴 < 0 ∧ 0 < 𝐴 ) )
16 12 15 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 < 0 ∨ 0 < 𝐴 ) ∧ ¬ ( 𝐴 < 0 ∧ 0 < 𝐴 ) ) )
17 pm5.17 ⊢ ( ( ( 𝐴 < 0 ∨ 0 < 𝐴 ) ∧ ¬ ( 𝐴 < 0 ∧ 0 < 𝐴 ) ) ↔ ( 𝐴 < 0 ↔ ¬ 0 < 𝐴 ) )
18 16 17 sylib ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 < 0 ↔ ¬ 0 < 𝐴 ) )
19 18 con2bid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 0 < 𝐴 ↔ ¬ 𝐴 < 0 ) )
20 8 19 bitr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( - 𝐴 < 0 ↔ ¬ 𝐴 < 0 ) )
21 20 ifbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → if ( - 𝐴 < 0 , - 1 , 1 ) = if ( ¬ 𝐴 < 0 , - 1 , 1 ) )
22 ifnot ⊢ if ( ¬ 𝐴 < 0 , - 1 , 1 ) = if ( 𝐴 < 0 , 1 , - 1 )
23 21 22 eqtrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → if ( - 𝐴 < 0 , - 1 , 1 ) = if ( 𝐴 < 0 , 1 , - 1 ) )
24 6 23 syldan ⊢ ( ( 𝐴 ∈ ℝ ∧ ¬ - 𝐴 = 0 ) → if ( - 𝐴 < 0 , - 1 , 1 ) = if ( 𝐴 < 0 , 1 , - 1 ) )
25 3 4 24 ifbieq12d2 ⊢ ( 𝐴 ∈ ℝ → if ( - 𝐴 = 0 , 0 , if ( - 𝐴 < 0 , - 1 , 1 ) ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , 1 , - 1 ) ) )
26 renegcl ⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
27 rexr ⊢ ( - 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ* )
28 sgnval ⊢ ( - 𝐴 ∈ ℝ* → ( sgn ‘ - 𝐴 ) = if ( - 𝐴 = 0 , 0 , if ( - 𝐴 < 0 , - 1 , 1 ) ) )
29 26 27 28 3syl ⊢ ( 𝐴 ∈ ℝ → ( sgn ‘ - 𝐴 ) = if ( - 𝐴 = 0 , 0 , if ( - 𝐴 < 0 , - 1 , 1 ) ) )
30 df-neg ⊢ - ( sgn ‘ 𝐴 ) = ( 0 − ( sgn ‘ 𝐴 ) )
31 30 a1i ⊢ ( 𝐴 ∈ ℝ → - ( sgn ‘ 𝐴 ) = ( 0 − ( sgn ‘ 𝐴 ) ) )
32 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
33 sgnval ⊢ ( 𝐴 ∈ ℝ* → ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )
34 32 33 syl ⊢ ( 𝐴 ∈ ℝ → ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )
35 34 oveq2d ⊢ ( 𝐴 ∈ ℝ → ( 0 − ( sgn ‘ 𝐴 ) ) = ( 0 − if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) ) )
36 ovif2 ⊢ ( 0 − if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) ) = if ( 𝐴 = 0 , ( 0 − 0 ) , ( 0 − if ( 𝐴 < 0 , - 1 , 1 ) ) )
37 biid ⊢ ( 𝐴 = 0 ↔ 𝐴 = 0 )
38 0m0e0 ⊢ ( 0 − 0 ) = 0
39 ovif2 ⊢ ( 0 − if ( 𝐴 < 0 , - 1 , 1 ) ) = if ( 𝐴 < 0 , ( 0 − - 1 ) , ( 0 − 1 ) )
40 biid ⊢ ( 𝐴 < 0 ↔ 𝐴 < 0 )
41 0cn ⊢ 0 ∈ ℂ
42 ax-1cn ⊢ 1 ∈ ℂ
43 41 42 subnegi ⊢ ( 0 − - 1 ) = ( 0 + 1 )
44 0p1e1 ⊢ ( 0 + 1 ) = 1
45 43 44 eqtr2i ⊢ 1 = ( 0 − - 1 )
46 df-neg ⊢ - 1 = ( 0 − 1 )
47 40 45 46 ifbieq12i ⊢ if ( 𝐴 < 0 , 1 , - 1 ) = if ( 𝐴 < 0 , ( 0 − - 1 ) , ( 0 − 1 ) )
48 39 47 eqtr4i ⊢ ( 0 − if ( 𝐴 < 0 , - 1 , 1 ) ) = if ( 𝐴 < 0 , 1 , - 1 )
49 37 38 48 ifbieq12i ⊢ if ( 𝐴 = 0 , ( 0 − 0 ) , ( 0 − if ( 𝐴 < 0 , - 1 , 1 ) ) ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , 1 , - 1 ) )
50 36 49 eqtri ⊢ ( 0 − if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , 1 , - 1 ) )
51 50 a1i ⊢ ( 𝐴 ∈ ℝ → ( 0 − if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , 1 , - 1 ) ) )
52 31 35 51 3eqtrd ⊢ ( 𝐴 ∈ ℝ → - ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , 1 , - 1 ) ) )
53 25 29 52 3eqtr4d ⊢ ( 𝐴 ∈ ℝ → ( sgn ‘ - 𝐴 ) = - ( sgn ‘ 𝐴 ) )