sgnmulsgn

Description: If two real numbers are of different signs, so are their signums. (Contributed by Thierry Arnoux, 12-Oct-2018)

		Ref	Expression
	Assertion	sgnmulsgn	$⊢ (A \in ℝ \land B \in ℝ) \to (A B < 0 \leftrightarrow sgn (A) sgn (B) < 0)$

Proof

Step	Hyp	Ref	Expression
1		neg1lt0	$⊢ - 1 < 0$
2		breq1	$⊢ sgn (A B) = - 1 \to (sgn (A B) < 0 \leftrightarrow - 1 < 0)$
3	1 2	mpbiri	$⊢ sgn (A B) = - 1 \to sgn (A B) < 0$
4	3	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land sgn (A B) = - 1) \to sgn (A B) < 0$
5		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \land sgn (A B) = - 1) \to sgn (A B) = - 1$
6		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \land sgn (A B) = 0) \to sgn (A B) = 0$
7		simplr	$⊢ (((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \land sgn (A B) = 0) \to sgn (A B) < 0$
8	7	lt0ne0d	$⊢ (((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \land sgn (A B) = 0) \to sgn (A B) \neq 0$
9	6 8	pm2.21ddne	$⊢ (((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \land sgn (A B) = 0) \to sgn (A B) = - 1$
10		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \land sgn (A B) = 1) \to sgn (A B) = 1$
11		simplr	$⊢ (((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \land sgn (A B) = 1) \to sgn (A B) < 0$
12	10 11	eqbrtrrd	$⊢ (((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \land sgn (A B) = 1) \to 1 < 0$
13		1nn0	$⊢ 1 \in ℕ_{0}$
14		nn0nlt0	$⊢ 1 \in ℕ_{0} \to \neg 1 < 0$
15	13 14	mp1i	$⊢ (((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \land sgn (A B) = 1) \to \neg 1 < 0$
16	12 15	pm2.21dd	$⊢ (((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \land sgn (A B) = 1) \to sgn (A B) = - 1$
17		remulcl	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ$
18	17	rexrd	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ^{*}$
19	18	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \to A B \in ℝ^{*}$
20		sgncl	$⊢ A B \in ℝ^{*} \to sgn (A B) \in \{- 1, 0, 1\}$
21		eltpi	$⊢ sgn (A B) \in \{- 1, 0, 1\} \to (sgn (A B) = - 1 \lor sgn (A B) = 0 \lor sgn (A B) = 1)$
22	19 20 21	3syl	$⊢ ((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \to (sgn (A B) = - 1 \lor sgn (A B) = 0 \lor sgn (A B) = 1)$
23	5 9 16 22	mpjao3dan	$⊢ ((A \in ℝ \land B \in ℝ) \land sgn (A B) < 0) \to sgn (A B) = - 1$
24	4 23	impbida	$⊢ (A \in ℝ \land B \in ℝ) \to (sgn (A B) = - 1 \leftrightarrow sgn (A B) < 0)$
25		sgnnbi	$⊢ A B \in ℝ^{*} \to (sgn (A B) = - 1 \leftrightarrow A B < 0)$
26	18 25	syl	$⊢ (A \in ℝ \land B \in ℝ) \to (sgn (A B) = - 1 \leftrightarrow A B < 0)$
27		sgnmul	$⊢ (A \in ℝ \land B \in ℝ) \to sgn (A B) = sgn (A) sgn (B)$
28	27	breq1d	$⊢ (A \in ℝ \land B \in ℝ) \to (sgn (A B) < 0 \leftrightarrow sgn (A) sgn (B) < 0)$
29	24 26 28	3bitr3d	$⊢ (A \in ℝ \land B \in ℝ) \to (A B < 0 \leftrightarrow sgn (A) sgn (B) < 0)$

Metamath Proof Explorer

Theorem sgnmulsgn

Proof