Theorem sgnsub

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

	Ref	Expression
Assertion	sgnsub	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( sgn ‘ ( 𝐴 − 𝐵 ) ) = ( sgn ‘ 𝐴 ) )

Proof

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