Metamath Proof Explorer

Theorem sgnsgn

Description: Signum is idempotent. (Contributed by Thierry Arnoux, 2-Oct-2018)

Ref Expression
Assertion sgnsgn 
|- ( A e. RR* -> ( sgn ` ( sgn ` A ) ) = ( sgn ` A ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. RR* -> A e. RR* )
2 fveq2 
 |-  ( ( sgn ` A ) = 0 -> ( sgn ` ( sgn ` A ) ) = ( sgn ` 0 ) )
3 id 
 |-  ( ( sgn ` A ) = 0 -> ( sgn ` A ) = 0 )
4 2 3 eqeq12d 
 |-  ( ( sgn ` A ) = 0 -> ( ( sgn ` ( sgn ` A ) ) = ( sgn ` A ) <-> ( sgn ` 0 ) = 0 ) )
5 fveq2 
 |-  ( ( sgn ` A ) = 1 -> ( sgn ` ( sgn ` A ) ) = ( sgn ` 1 ) )
6 id 
 |-  ( ( sgn ` A ) = 1 -> ( sgn ` A ) = 1 )
7 5 6 eqeq12d 
 |-  ( ( sgn ` A ) = 1 -> ( ( sgn ` ( sgn ` A ) ) = ( sgn ` A ) <-> ( sgn ` 1 ) = 1 ) )
8 fveq2 
 |-  ( ( sgn ` A ) = -u 1 -> ( sgn ` ( sgn ` A ) ) = ( sgn ` -u 1 ) )
9 id 
 |-  ( ( sgn ` A ) = -u 1 -> ( sgn ` A ) = -u 1 )
10 8 9 eqeq12d 
 |-  ( ( sgn ` A ) = -u 1 -> ( ( sgn ` ( sgn ` A ) ) = ( sgn ` A ) <-> ( sgn ` -u 1 ) = -u 1 ) )
11 sgn0 
 |-  ( sgn ` 0 ) = 0
12 11 a1i 
 |-  ( ( A e. RR* /\ A = 0 ) -> ( sgn ` 0 ) = 0 )
13 sgn1 
 |-  ( sgn ` 1 ) = 1
14 13 a1i 
 |-  ( ( A e. RR* /\ 0 < A ) -> ( sgn ` 1 ) = 1 )
15 neg1rr 
 |-  -u 1 e. RR
16 15 rexri 
 |-  -u 1 e. RR*
17 neg1lt0 
 |-  -u 1 < 0
18 sgnn 
 |-  ( ( -u 1 e. RR* /\ -u 1 < 0 ) -> ( sgn ` -u 1 ) = -u 1 )
19 16 17 18 mp2an 
 |-  ( sgn ` -u 1 ) = -u 1
20 19 a1i 
 |-  ( ( A e. RR* /\ A < 0 ) -> ( sgn ` -u 1 ) = -u 1 )
21 1 4 7 10 12 14 20 sgn3da 
 |-  ( A e. RR* -> ( sgn ` ( sgn ` A ) ) = ( sgn ` A ) )