Metamath Proof Explorer

Theorem sgncl

Description: Closure of the signum: The signum of an extended real is either -1 or 0 or 1. (Contributed by Thierry Arnoux, 28-Sep-2018)

Ref Expression
Assertion sgncl ⊢ A ∈ ℝ * → sgn ⁡ A ∈ − 1 0 1

Proof

Step Hyp Ref Expression
1 simpr ⊢ A ∈ ℝ * ∧ A = 0 → A = 0
2 1 fveq2d ⊢ A ∈ ℝ * ∧ A = 0 → sgn ⁡ A = sgn ⁡ 0
3 sgn0 ⊢ sgn ⁡ 0 = 0
4 2 3 eqtrdi ⊢ A ∈ ℝ * ∧ A = 0 → sgn ⁡ A = 0
5 c0ex ⊢ 0 ∈ V
6 5 tpid2 ⊢ 0 ∈ − 1 0 1
7 4 6 eqeltrdi ⊢ A ∈ ℝ * ∧ A = 0 → sgn ⁡ A ∈ − 1 0 1
8 sgnn ⊢ A ∈ ℝ * ∧ A < 0 → sgn ⁡ A = − 1
9 negex ⊢ − 1 ∈ V
10 9 tpid1 ⊢ − 1 ∈ − 1 0 1
11 8 10 eqeltrdi ⊢ A ∈ ℝ * ∧ A < 0 → sgn ⁡ A ∈ − 1 0 1
12 11 adantlr ⊢ A ∈ ℝ * ∧ A ≠ 0 ∧ A < 0 → sgn ⁡ A ∈ − 1 0 1
13 sgnp ⊢ A ∈ ℝ * ∧ 0 < A → sgn ⁡ A = 1
14 1ex ⊢ 1 ∈ V
15 14 tpid3 ⊢ 1 ∈ − 1 0 1
16 13 15 eqeltrdi ⊢ A ∈ ℝ * ∧ 0 < A → sgn ⁡ A ∈ − 1 0 1
17 16 adantlr ⊢ A ∈ ℝ * ∧ A ≠ 0 ∧ 0 < A → sgn ⁡ A ∈ − 1 0 1
18 0xr ⊢ 0 ∈ ℝ *
19 xrlttri2 ⊢ A ∈ ℝ * ∧ 0 ∈ ℝ * → A ≠ 0 ↔ A < 0 ∨ 0 < A
20 19 biimpa ⊢ A ∈ ℝ * ∧ 0 ∈ ℝ * ∧ A ≠ 0 → A < 0 ∨ 0 < A
21 18 20 mpanl2 ⊢ A ∈ ℝ * ∧ A ≠ 0 → A < 0 ∨ 0 < A
22 12 17 21 mpjaodan ⊢ A ∈ ℝ * ∧ A ≠ 0 → sgn ⁡ A ∈ − 1 0 1
23 7 22 pm2.61dane ⊢ A ∈ ℝ * → sgn ⁡ A ∈ − 1 0 1