Metamath Proof Explorer

Theorem sgnnbi

Description: Negative signum. (Contributed by Thierry Arnoux, 2-Oct-2018)

Ref Expression
Assertion sgnnbi 
|- ( A e. RR* -> ( ( sgn ` A ) = -u 1 <-> A < 0 ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. RR* -> A e. RR* )
2 eqeq1 
 |-  ( ( sgn ` A ) = 0 -> ( ( sgn ` A ) = -u 1 <-> 0 = -u 1 ) )
3 2 imbi1d 
 |-  ( ( sgn ` A ) = 0 -> ( ( ( sgn ` A ) = -u 1 -> A < 0 ) <-> ( 0 = -u 1 -> A < 0 ) ) )
4 eqeq1 
 |-  ( ( sgn ` A ) = 1 -> ( ( sgn ` A ) = -u 1 <-> 1 = -u 1 ) )
5 4 imbi1d 
 |-  ( ( sgn ` A ) = 1 -> ( ( ( sgn ` A ) = -u 1 -> A < 0 ) <-> ( 1 = -u 1 -> A < 0 ) ) )
6 eqeq1 
 |-  ( ( sgn ` A ) = -u 1 -> ( ( sgn ` A ) = -u 1 <-> -u 1 = -u 1 ) )
7 6 imbi1d 
 |-  ( ( sgn ` A ) = -u 1 -> ( ( ( sgn ` A ) = -u 1 -> A < 0 ) <-> ( -u 1 = -u 1 -> A < 0 ) ) )
8 neg1ne0 
 |-  -u 1 =/= 0
9 8 nesymi 
 |-  -. 0 = -u 1
10 9 pm2.21i 
 |-  ( 0 = -u 1 -> A < 0 )
11 10 a1i 
 |-  ( ( A e. RR* /\ A = 0 ) -> ( 0 = -u 1 -> A < 0 ) )
12 neg1rr 
 |-  -u 1 e. RR
13 neg1lt0 
 |-  -u 1 < 0
14 0lt1 
 |-  0 < 1
15 0re 
 |-  0 e. RR
16 1re 
 |-  1 e. RR
17 12 15 16 lttri 
 |-  ( ( -u 1 < 0 /\ 0 < 1 ) -> -u 1 < 1 )
18 13 14 17 mp2an 
 |-  -u 1 < 1
19 12 18 gtneii 
 |-  1 =/= -u 1
20 19 neii 
 |-  -. 1 = -u 1
21 20 pm2.21i 
 |-  ( 1 = -u 1 -> A < 0 )
22 21 a1i 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( 1 = -u 1 -> A < 0 ) )
23 simp2 
 |-  ( ( A e. RR* /\ A < 0 /\ -u 1 = -u 1 ) -> A < 0 )
24 23 3expia 
 |-  ( ( A e. RR* /\ A < 0 ) -> ( -u 1 = -u 1 -> A < 0 ) )
25 1 3 5 7 11 22 24 sgn3da 
 |-  ( A e. RR* -> ( ( sgn ` A ) = -u 1 -> A < 0 ) )
26 25 imp 
 |-  ( ( A e. RR* /\ ( sgn ` A ) = -u 1 ) -> A < 0 )
27 sgnn 
 |-  ( ( A e. RR* /\ A < 0 ) -> ( sgn ` A ) = -u 1 )
28 26 27 impbida 
 |-  ( A e. RR* -> ( ( sgn ` A ) = -u 1 <-> A < 0 ) )