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	⊢ ( 𝐴 ∈ ℝ* → ( sgn ‘ 𝐴 ) ∈ { - 1 , 0 , 1 } )

Proof

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