Metamath Proof Explorer

Theorem sgnsgn

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

Ref Expression
Assertion sgnsgn ⊢A∈ℝ*→sgn⁡sgn⁡A=sgn⁡A

Proof

Step Hyp Ref Expression
1 id ⊢A∈ℝ*→A∈ℝ*
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=−1→sgn⁡sgn⁡A=sgn⁡−1
9 id ⊢sgn⁡A=−1→sgn⁡A=−1
10 8 9 eqeq12d ⊢sgn⁡A=−1→sgn⁡sgn⁡A=sgn⁡A↔sgn⁡−1=−1
11 sgn0 ⊢sgn⁡0=0
12 11 a1i ⊢A∈ℝ*∧A=0→sgn⁡0=0
13 sgn1 ⊢sgn⁡1=1
14 13 a1i ⊢A∈ℝ*∧0<A→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 ⊢A∈ℝ*∧A<0→sgn⁡−1=−1
21 1 4 7 10 12 14 20 sgn3da ⊢A∈ℝ*→sgn⁡sgn⁡A=sgn⁡A