Metamath Proof Explorer

Theorem sgnpbi

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

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

Proof

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