sgnsub

Description: Signum of a difference with a number of opposite sign. (Contributed by Thierry Arnoux, 2-Oct-2018)

		Ref	Expression
	Assertion	sgnsub	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to sgn (A - B) = sgn (A)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to A \in ℝ$
2	1	rexrd	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to A \in ℝ^{*}$
3		eqeq2	$⊢ sgn (A) = 0 \to (sgn (A - B) = sgn (A) \leftrightarrow sgn (A - B) = 0)$
4		eqeq2	$⊢ sgn (A) = 1 \to (sgn (A - B) = sgn (A) \leftrightarrow sgn (A - B) = 1)$
5		eqeq2	$⊢ sgn (A) = - 1 \to (sgn (A - B) = sgn (A) \leftrightarrow sgn (A - B) = - 1)$
6		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to A = 0$
7	1	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to A \in ℂ$
8	7	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to A \in ℂ$
9		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to B \in ℝ$
10	9	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to B \in ℂ$
11	10	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to B \in ℂ$
12		simplr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to A B < 0$
13	12	lt0ne0d	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to A B \neq 0$
14	8 11 13	mulne0bad	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to A \neq 0$
15	6 14	pm2.21ddne	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A = 0) \to sgn (A - B) = 0$
16		simplll	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to A \in ℝ$
17		simpllr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to B \in ℝ$
18	16 17	resubcld	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to A - B \in ℝ$
19	18	rexrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to A - B \in ℝ^{*}$
20		0red	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to 0 \in ℝ$
21		simpr	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to A B < 0$
22	1 9 21	mul2lt0lgt0	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to B < 0$
23		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to 0 < A$
24	17 20 16 22 23	lttrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to B < A$
25		simpr	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ$
26		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
27	25 26	posdifd	$⊢ (A \in ℝ \land B \in ℝ) \to (B < A \leftrightarrow 0 < A - B)$
28	27	biimpa	$⊢ ((A \in ℝ \land B \in ℝ) \land B < A) \to 0 < A - B$
29	16 17 24 28	syl21anc	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to 0 < A - B$
30		sgnp	$⊢ (A - B \in ℝ^{*} \land 0 < A - B) \to sgn (A - B) = 1$
31	19 29 30	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land 0 < A) \to sgn (A - B) = 1$
32		simplll	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to A \in ℝ$
33		simpllr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to B \in ℝ$
34	32 33	resubcld	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to A - B \in ℝ$
35	34	rexrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to A - B \in ℝ^{*}$
36		0red	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to 0 \in ℝ$
37	7	adantr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to A \in ℂ$
38	37	subid1d	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to A - 0 = A$
39		simpr	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to A < 0$
40	1 9 21	mul2lt0llt0	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to 0 < B$
41	32 36 33 39 40	lttrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to A < B$
42	38 41	eqbrtrd	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to A - 0 < B$
43	32 36 33 42	ltsub23d	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to A - B < 0$
44		sgnn	$⊢ (A - B \in ℝ^{*} \land A - B < 0) \to sgn (A - B) = - 1$
45	35 43 44	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ) \land A B < 0) \land A < 0) \to sgn (A - B) = - 1$
46	2 3 4 5 15 31 45	sgn3da	$⊢ ((A \in ℝ \land B \in ℝ) \land A B < 0) \to sgn (A - B) = sgn (A)$

Metamath Proof Explorer

Theorem sgnsub

Proof