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	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) )

Proof

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