sgncl

Description: Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018)

		Ref	Expression
	Assertion	sgncl	$⊢ A \in ℝ^{*} \to sgn (A) \in \{- 1, 0, 1\}$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in ℝ^{*} \land A = 0) \to A = 0$
2	1	fveq2d	$⊢ (A \in ℝ^{*} \land A = 0) \to sgn (A) = sgn (0)$
3		sgn0	$⊢ sgn (0) = 0$
4	2 3	eqtrdi	$⊢ (A \in ℝ^{*} \land A = 0) \to sgn (A) = 0$
5		c0ex	$⊢ 0 \in V$
6	5	tpid2	$⊢ 0 \in \{- 1, 0, 1\}$
7	4 6	eqeltrdi	$⊢ (A \in ℝ^{*} \land A = 0) \to sgn (A) \in \{- 1, 0, 1\}$
8		sgnn	$⊢ (A \in ℝ^{*} \land A < 0) \to sgn (A) = - 1$
9		negex	$⊢ - 1 \in V$
10	9	tpid1	$⊢ - 1 \in \{- 1, 0, 1\}$
11	8 10	eqeltrdi	$⊢ (A \in ℝ^{*} \land A < 0) \to sgn (A) \in \{- 1, 0, 1\}$
12	11	adantlr	$⊢ ((A \in ℝ^{*} \land A \neq 0) \land A < 0) \to sgn (A) \in \{- 1, 0, 1\}$
13		sgnp	$⊢ (A \in ℝ^{*} \land 0 < A) \to sgn (A) = 1$
14		1ex	$⊢ 1 \in V$
15	14	tpid3	$⊢ 1 \in \{- 1, 0, 1\}$
16	13 15	eqeltrdi	$⊢ (A \in ℝ^{*} \land 0 < A) \to sgn (A) \in \{- 1, 0, 1\}$
17	16	adantlr	$⊢ ((A \in ℝ^{*} \land A \neq 0) \land 0 < A) \to sgn (A) \in \{- 1, 0, 1\}$
18		0xr	$⊢ 0 \in ℝ^{*}$
19		xrlttri2	$⊢ (A \in ℝ^{} \land 0 \in ℝ^{}) \to (A \neq 0 \leftrightarrow (A < 0 \lor 0 < A))$
20	19	biimpa	$⊢ ((A \in ℝ^{} \land 0 \in ℝ^{}) \land A \neq 0) \to (A < 0 \lor 0 < A)$
21	18 20	mpanl2	$⊢ (A \in ℝ^{*} \land A \neq 0) \to (A < 0 \lor 0 < A)$
22	12 17 21	mpjaodan	$⊢ (A \in ℝ^{*} \land A \neq 0) \to sgn (A) \in \{- 1, 0, 1\}$
23	7 22	pm2.61dane	$⊢ A \in ℝ^{*} \to sgn (A) \in \{- 1, 0, 1\}$

Metamath Proof Explorer