Theorem le2add

Description: Adding both sides of two 'less than or equal to' relations. (Contributed by NM, 17-Apr-2005) (Proof shortened by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	le2add	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷 ) → ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
2		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
3		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
4		leadd1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐶 ↔ ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐵 ) ) )
5	1 2 3 4	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 ≤ 𝐶 ↔ ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐵 ) ) )
6		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℝ )
7		leadd2	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ≤ 𝐷 ↔ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) )
8	3 6 2 7	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 ≤ 𝐷 ↔ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) )
9	5 8	anbi12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷 ) ↔ ( ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐵 ) ∧ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) ) )
10	1 3	readdcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
11	2 3	readdcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
12	2 6	readdcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐶 + 𝐷 ) ∈ ℝ )
13		letr	⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ ( 𝐶 + 𝐵 ) ∈ ℝ ∧ ( 𝐶 + 𝐷 ) ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐵 ) ∧ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) → ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) )
14	10 11 12 13	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐵 ) ∧ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) → ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) )
15	9 14	sylbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷 ) → ( 𝐴 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) )