Description: Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 27-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | leidd.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
| ltnegd.2 | ⊢ ( 𝜑 → 𝐵 ∈ ℝ ) | ||
| ltadd1d.3 | ⊢ ( 𝜑 → 𝐶 ∈ ℝ ) | ||
| lt2addd.4 | ⊢ ( 𝜑 → 𝐷 ∈ ℝ ) | ||
| lt2addd.5 | ⊢ ( 𝜑 → 𝐴 < 𝐶 ) | ||
| lt2addd.6 | ⊢ ( 𝜑 → 𝐵 < 𝐷 ) | ||
| Assertion | lt2subd | ⊢ ( 𝜑 → ( 𝐴 − 𝐷 ) < ( 𝐶 − 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leidd.1 | ⊢ ( 𝜑 → 𝐴 ∈ ℝ ) | |
| 2 | ltnegd.2 | ⊢ ( 𝜑 → 𝐵 ∈ ℝ ) | |
| 3 | ltadd1d.3 | ⊢ ( 𝜑 → 𝐶 ∈ ℝ ) | |
| 4 | lt2addd.4 | ⊢ ( 𝜑 → 𝐷 ∈ ℝ ) | |
| 5 | lt2addd.5 | ⊢ ( 𝜑 → 𝐴 < 𝐶 ) | |
| 6 | lt2addd.6 | ⊢ ( 𝜑 → 𝐵 < 𝐷 ) | |
| 7 | lt2sub | ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ) → ( ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐷 ) → ( 𝐴 − 𝐷 ) < ( 𝐶 − 𝐵 ) ) ) | |
| 8 | 1 4 3 2 7 | syl22anc | ⊢ ( 𝜑 → ( ( 𝐴 < 𝐶 ∧ 𝐵 < 𝐷 ) → ( 𝐴 − 𝐷 ) < ( 𝐶 − 𝐵 ) ) ) |
| 9 | 5 6 8 | mp2and | ⊢ ( 𝜑 → ( 𝐴 − 𝐷 ) < ( 𝐶 − 𝐵 ) ) |