sgnmulsgp

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

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

Proof

Step	Hyp	Ref	Expression
1		0lt1	$⊢ 0 < 1$
2		breq2	$⊢ sgn (A B) = 1 \to (0 < sgn (A B) \leftrightarrow 0 < 1)$
3	1 2	mpbiri	$⊢ sgn (A B) = 1 \to 0 < sgn (A B)$
4	3	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land sgn (A B) = 1) \to 0 < sgn (A B)$
5		simplr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \land sgn (A B) = - 1) \to 0 < sgn (A B)$
6		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \land sgn (A B) = - 1) \to sgn (A B) = - 1$
7	5 6	breqtrd	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \land sgn (A B) = - 1) \to 0 < - 1$
8		1nn0	$⊢ 1 \in ℕ_{0}$
9		nn0nlt0	$⊢ 1 \in ℕ_{0} \to \neg 1 < 0$
10	8 9	ax-mp	$⊢ \neg 1 < 0$
11		1re	$⊢ 1 \in ℝ$
12		lt0neg1	$⊢ 1 \in ℝ \to (1 < 0 \leftrightarrow 0 < - 1)$
13	11 12	ax-mp	$⊢ 1 < 0 \leftrightarrow 0 < - 1$
14	10 13	mtbi	$⊢ \neg 0 < - 1$
15	14	a1i	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \land sgn (A B) = - 1) \to \neg 0 < - 1$
16	7 15	pm2.21dd	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \land sgn (A B) = - 1) \to sgn (A B) = 1$
17		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \land sgn (A B) = 0) \to sgn (A B) = 0$
18		simplr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \land sgn (A B) = 0) \to 0 < sgn (A B)$
19	18	gt0ne0d	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \land sgn (A B) = 0) \to sgn (A B) \neq 0$
20	17 19	pm2.21ddne	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \land sgn (A B) = 0) \to sgn (A B) = 1$
21		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \land sgn (A B) = 1) \to sgn (A B) = 1$
22		remulcl	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ$
23	22	rexrd	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ^{*}$
24	23	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \to A B \in ℝ^{*}$
25		sgncl	$⊢ A B \in ℝ^{*} \to sgn (A B) \in \{- 1, 0, 1\}$
26		eltpi	$⊢ sgn (A B) \in \{- 1, 0, 1\} \to (sgn (A B) = - 1 \lor sgn (A B) = 0 \lor sgn (A B) = 1)$
27	24 25 26	3syl	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \to (sgn (A B) = - 1 \lor sgn (A B) = 0 \lor sgn (A B) = 1)$
28	16 20 21 27	mpjao3dan	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < sgn (A B)) \to sgn (A B) = 1$
29	4 28	impbida	$⊢ (A \in ℝ \land B \in ℝ) \to (sgn (A B) = 1 \leftrightarrow 0 < sgn (A B))$
30		sgnpbi	$⊢ A B \in ℝ^{*} \to (sgn (A B) = 1 \leftrightarrow 0 < A B)$
31	23 30	syl	$⊢ (A \in ℝ \land B \in ℝ) \to (sgn (A B) = 1 \leftrightarrow 0 < A B)$
32		sgnmul	$⊢ (A \in ℝ \land B \in ℝ) \to sgn (A B) = sgn (A) sgn (B)$
33	32	breq2d	$⊢ (A \in ℝ \land B \in ℝ) \to (0 < sgn (A B) \leftrightarrow 0 < sgn (A) sgn (B))$
34	29 31 33	3bitr3d	$⊢ (A \in ℝ \land B \in ℝ) \to (0 < A B \leftrightarrow 0 < sgn (A) sgn (B))$

Metamath Proof Explorer

Theorem sgnmulsgp

Proof