Metamath Proof Explorer

Theorem sgnneg

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

Ref Expression
Assertion sgnneg 
|- ( A e. RR -> ( sgn ` -u A ) = -u ( sgn ` A ) )

Proof

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