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 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B ⁢ C − B ≤ 0 ↔ A ≤ B ∧ B ≤ C ∨ C ≤ B ∧ B ≤ A

Proof

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