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