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