Metamath Proof Explorer

Theorem lt2add

Description: Adding both sides of two 'less than' relations. Theorem I.25 of Apostol p. 20. (Contributed by NM, 15-Aug-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	lt2add	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ((A < C \land B < D) \to A + B < C + D)$

Proof

Step	Hyp	Ref	Expression
1		ltle	$⊢ (A \in ℝ \land C \in ℝ) \to (A < C \to A \leq C)$
2	1	ad2ant2r	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A < C \to A \leq C)$
3		leltadd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ((A \leq C \land B < D) \to A + B < C + D)$
4	2 3	syland	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ((A < C \land B < D) \to A + B < C + D)$