Metamath Proof Explorer

Theorem le2sub

Description: Subtracting both sides of two 'less than or equal to' relations. (Contributed by Mario Carneiro, 14-Apr-2016)

Ref Expression
Assertion le2sub ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A≤C∧D≤B→A−B≤C−D

Proof

Step Hyp Ref Expression
1 simpll ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A∈ℝ
2 simprl ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→C∈ℝ
3 simplr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→B∈ℝ
4 lesub1 ⊢A∈ℝ∧C∈ℝ∧B∈ℝ→A≤C↔A−B≤C−B
5 1 2 3 4 syl3anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A≤C↔A−B≤C−B
6 simprr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→D∈ℝ
7 lesub2 ⊢D∈ℝ∧B∈ℝ∧C∈ℝ→D≤B↔C−B≤C−D
8 6 3 2 7 syl3anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→D≤B↔C−B≤C−D
9 5 8 anbi12d ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A≤C∧D≤B↔A−B≤C−B∧C−B≤C−D
10 resubcl ⊢A∈ℝ∧B∈ℝ→A−B∈ℝ
11 10 adantr ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A−B∈ℝ
12 2 3 resubcld ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→C−B∈ℝ
13 resubcl ⊢C∈ℝ∧D∈ℝ→C−D∈ℝ
14 13 adantl ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→C−D∈ℝ
15 letr ⊢A−B∈ℝ∧C−B∈ℝ∧C−D∈ℝ→A−B≤C−B∧C−B≤C−D→A−B≤C−D
16 11 12 14 15 syl3anc ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A−B≤C−B∧C−B≤C−D→A−B≤C−D
17 9 16 sylbid ⊢A∈ℝ∧B∈ℝ∧C∈ℝ∧D∈ℝ→A≤C∧D≤B→A−B≤C−D