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