Metamath Proof Explorer

Theorem sgnsub

Description: Signum of a difference with 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 ‘ 𝐴 ) )