sgn0bi

		Ref	Expression
	Assertion	sgn0bi	$⊢ A \in ℝ^{*} \to (sgn (A) = 0 \leftrightarrow A = 0)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ A \in ℝ^{} \to A \in ℝ^{}$
2		eqeq1	$⊢ sgn (A) = 0 \to (sgn (A) = 0 \leftrightarrow 0 = 0)$
3	2	bibi1d	$⊢ sgn (A) = 0 \to ((sgn (A) = 0 \leftrightarrow A = 0) \leftrightarrow (0 = 0 \leftrightarrow A = 0))$
4		eqeq1	$⊢ sgn (A) = 1 \to (sgn (A) = 0 \leftrightarrow 1 = 0)$
5	4	bibi1d	$⊢ sgn (A) = 1 \to ((sgn (A) = 0 \leftrightarrow A = 0) \leftrightarrow (1 = 0 \leftrightarrow A = 0))$
6		eqeq1	$⊢ sgn (A) = - 1 \to (sgn (A) = 0 \leftrightarrow - 1 = 0)$
7	6	bibi1d	$⊢ sgn (A) = - 1 \to ((sgn (A) = 0 \leftrightarrow A = 0) \leftrightarrow (- 1 = 0 \leftrightarrow A = 0))$
8		simpr	$⊢ (A \in ℝ^{*} \land A = 0) \to A = 0$
9	8	eqcomd	$⊢ (A \in ℝ^{*} \land A = 0) \to 0 = A$
10	9	eqeq1d	$⊢ (A \in ℝ^{*} \land A = 0) \to (0 = 0 \leftrightarrow A = 0)$
11		ax-1ne0	$⊢ 1 \neq 0$
12	11	a1i	$⊢ (A \in ℝ^{*} \land 0 < A) \to 1 \neq 0$
13	12	neneqd	$⊢ (A \in ℝ^{*} \land 0 < A) \to \neg 1 = 0$
14		simpr	$⊢ (A \in ℝ^{*} \land 0 < A) \to 0 < A$
15	14	gt0ne0d	$⊢ (A \in ℝ^{*} \land 0 < A) \to A \neq 0$
16	15	neneqd	$⊢ (A \in ℝ^{*} \land 0 < A) \to \neg A = 0$
17	13 16	2falsed	$⊢ (A \in ℝ^{*} \land 0 < A) \to (1 = 0 \leftrightarrow A = 0)$
18		1cnd	$⊢ (A \in ℝ^{*} \land A < 0) \to 1 \in ℂ$
19	11	a1i	$⊢ (A \in ℝ^{*} \land A < 0) \to 1 \neq 0$
20	18 19	negne0d	$⊢ (A \in ℝ^{*} \land A < 0) \to - 1 \neq 0$
21	20	neneqd	$⊢ (A \in ℝ^{*} \land A < 0) \to \neg - 1 = 0$
22		simpr	$⊢ (A \in ℝ^{*} \land A < 0) \to A < 0$
23	22	lt0ne0d	$⊢ (A \in ℝ^{*} \land A < 0) \to A \neq 0$
24	23	neneqd	$⊢ (A \in ℝ^{*} \land A < 0) \to \neg A = 0$
25	21 24	2falsed	$⊢ (A \in ℝ^{*} \land A < 0) \to (- 1 = 0 \leftrightarrow A = 0)$
26	1 3 5 7 10 17 25	sgn3da	$⊢ A \in ℝ^{*} \to (sgn (A) = 0 \leftrightarrow A = 0)$

Metamath Proof Explorer

Theorem sgn0bi

Proof