Theorem sgnsgn

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

	Ref	Expression
Assertion	sgnsgn	⊢ ( 𝐴 ∈ ℝ* → ( sgn ‘ ( sgn ‘ 𝐴 ) ) = ( sgn ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ∈ ℝ* )
2		fveq2	⊢ ( ( sgn ‘ 𝐴 ) = 0 → ( sgn ‘ ( sgn ‘ 𝐴 ) ) = ( sgn ‘ 0 ) )
3		id	⊢ ( ( sgn ‘ 𝐴 ) = 0 → ( sgn ‘ 𝐴 ) = 0 )
4	2 3	eqeq12d	⊢ ( ( sgn ‘ 𝐴 ) = 0 → ( ( sgn ‘ ( sgn ‘ 𝐴 ) ) = ( sgn ‘ 𝐴 ) ↔ ( sgn ‘ 0 ) = 0 ) )
5		fveq2	⊢ ( ( sgn ‘ 𝐴 ) = 1 → ( sgn ‘ ( sgn ‘ 𝐴 ) ) = ( sgn ‘ 1 ) )
6		id	⊢ ( ( sgn ‘ 𝐴 ) = 1 → ( sgn ‘ 𝐴 ) = 1 )
7	5 6	eqeq12d	⊢ ( ( sgn ‘ 𝐴 ) = 1 → ( ( sgn ‘ ( sgn ‘ 𝐴 ) ) = ( sgn ‘ 𝐴 ) ↔ ( sgn ‘ 1 ) = 1 ) )
8		fveq2	⊢ ( ( sgn ‘ 𝐴 ) = - 1 → ( sgn ‘ ( sgn ‘ 𝐴 ) ) = ( sgn ‘ - 1 ) )
9		id	⊢ ( ( sgn ‘ 𝐴 ) = - 1 → ( sgn ‘ 𝐴 ) = - 1 )
10	8 9	eqeq12d	⊢ ( ( sgn ‘ 𝐴 ) = - 1 → ( ( sgn ‘ ( sgn ‘ 𝐴 ) ) = ( sgn ‘ 𝐴 ) ↔ ( sgn ‘ - 1 ) = - 1 ) )
11		sgn0	⊢ ( sgn ‘ 0 ) = 0
12	11	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 = 0 ) → ( sgn ‘ 0 ) = 0 )
13		sgn1	⊢ ( sgn ‘ 1 ) = 1
14	13	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) → ( sgn ‘ 1 ) = 1 )
15		neg1rr	⊢ - 1 ∈ ℝ
16	15	rexri	⊢ - 1 ∈ ℝ*
17		neg1lt0	⊢ - 1 < 0
18		sgnn	⊢ ( ( - 1 ∈ ℝ* ∧ - 1 < 0 ) → ( sgn ‘ - 1 ) = - 1 )
19	16 17 18	mp2an	⊢ ( sgn ‘ - 1 ) = - 1
20	19	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( sgn ‘ - 1 ) = - 1 )
21	1 4 7 10 12 14 20	sgn3da	⊢ ( 𝐴 ∈ ℝ* → ( sgn ‘ ( sgn ‘ 𝐴 ) ) = ( sgn ‘ 𝐴 ) )