This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lt2sub

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

Ref Expression
Assertion lt2sub ⊢ 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 ltsub1 ⊢ 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 ltsub2 ⊢ 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 lttr ⊢ 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