Metamath Proof Explorer

Theorem mulsuble0b

Description: A condition for multiplication of subtraction to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013)

Ref Expression
Assertion mulsuble0b ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐵 ) ) ≤ 0 ↔ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ∨ ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
3 resubcl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
4 3 ancoms ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
5 4 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
6 mulle0b ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℝ ∧ ( 𝐶 − 𝐵 ) ∈ ℝ ) → ( ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐵 ) ) ≤ 0 ↔ ( ( ( 𝐴 − 𝐵 ) ≤ 0 ∧ 0 ≤ ( 𝐶 − 𝐵 ) ) ∨ ( 0 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐶 − 𝐵 ) ≤ 0 ) ) ) )
7 2 5 6 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐵 ) ) ≤ 0 ↔ ( ( ( 𝐴 − 𝐵 ) ≤ 0 ∧ 0 ≤ ( 𝐶 − 𝐵 ) ) ∨ ( 0 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐶 − 𝐵 ) ≤ 0 ) ) ) )
8 suble0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 − 𝐵 ) ≤ 0 ↔ 𝐴 ≤ 𝐵 ) )
9 8 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 − 𝐵 ) ≤ 0 ↔ 𝐴 ≤ 𝐵 ) )
10 subge0 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ ( 𝐶 − 𝐵 ) ↔ 𝐵 ≤ 𝐶 ) )
11 10 ancoms ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 0 ≤ ( 𝐶 − 𝐵 ) ↔ 𝐵 ≤ 𝐶 ) )
12 11 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 0 ≤ ( 𝐶 − 𝐵 ) ↔ 𝐵 ≤ 𝐶 ) )
13 9 12 anbi12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 − 𝐵 ) ≤ 0 ∧ 0 ≤ ( 𝐶 − 𝐵 ) ) ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
14 subge0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ ( 𝐴 − 𝐵 ) ↔ 𝐵 ≤ 𝐴 ) )
15 14 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 0 ≤ ( 𝐴 − 𝐵 ) ↔ 𝐵 ≤ 𝐴 ) )
16 suble0 ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐶 − 𝐵 ) ≤ 0 ↔ 𝐶 ≤ 𝐵 ) )
17 16 ancoms ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 − 𝐵 ) ≤ 0 ↔ 𝐶 ≤ 𝐵 ) )
18 17 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐶 − 𝐵 ) ≤ 0 ↔ 𝐶 ≤ 𝐵 ) )
19 15 18 anbi12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 0 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐶 − 𝐵 ) ≤ 0 ) ↔ ( 𝐵 ≤ 𝐴 ∧ 𝐶 ≤ 𝐵 ) ) )
20 19 biancomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 0 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐶 − 𝐵 ) ≤ 0 ) ↔ ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) )
21 13 20 orbi12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( ( 𝐴 − 𝐵 ) ≤ 0 ∧ 0 ≤ ( 𝐶 − 𝐵 ) ) ∨ ( 0 ≤ ( 𝐴 − 𝐵 ) ∧ ( 𝐶 − 𝐵 ) ≤ 0 ) ) ↔ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ∨ ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) ) )
22 7 21 bitrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 − 𝐵 ) · ( 𝐶 − 𝐵 ) ) ≤ 0 ↔ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ∨ ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) ) )