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

Metamath Proof Explorer

Theorem le2addd

Description: Adding both side of two inequalities. (Contributed by Mario Carneiro, 27-May-2016) (Proof shortened by Glauco Siliprandi, 5-Apr-2020)

		Ref	Expression
	Hypotheses	leidd.1	$⊢ φ \to A \in ℝ$
		ltnegd.2	$⊢ φ \to B \in ℝ$
		ltadd1d.3	$⊢ φ \to C \in ℝ$
		lt2addd.4	$⊢ φ \to D \in ℝ$
		le2addd.5	$⊢ φ \to A \leq C$
		le2addd.6	$⊢ φ \to B \leq D$
	Assertion	le2addd	$⊢ φ \to A + B \leq C + D$

Proof

Step	Hyp	Ref	Expression
1		leidd.1	$⊢ φ \to A \in ℝ$
2		ltnegd.2	$⊢ φ \to B \in ℝ$
3		ltadd1d.3	$⊢ φ \to C \in ℝ$
4		lt2addd.4	$⊢ φ \to D \in ℝ$
5		le2addd.5	$⊢ φ \to A \leq C$
6		le2addd.6	$⊢ φ \to B \leq D$
7	1 2	readdcld	$⊢ φ \to A + B \in ℝ$
8	3 2	readdcld	$⊢ φ \to C + B \in ℝ$
9	3 4	readdcld	$⊢ φ \to C + D \in ℝ$
10	1 3 2 5	leadd1dd	$⊢ φ \to A + B \leq C + B$
11	2 4 3 6	leadd2dd	$⊢ φ \to C + B \leq C + D$
12	7 8 9 10 11	letrd	$⊢ φ \to A + B \leq C + D$