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	|- ( ph -> A e. RR )
	ltnegd.2	|- ( ph -> B e. RR )
	ltadd1d.3	|- ( ph -> C e. RR )
	lt2addd.4	|- ( ph -> D e. RR )
	le2addd.5	|- ( ph -> A <_ C )
	le2addd.6	|- ( ph -> B <_ D )
Assertion	le2addd	|- ( ph -> ( A + B ) <_ ( C + D ) )

Proof

Step	Hyp	Ref	Expression
1		leidd.1	|- ( ph -> A e. RR )
2		ltnegd.2	|- ( ph -> B e. RR )
3		ltadd1d.3	|- ( ph -> C e. RR )
4		lt2addd.4	|- ( ph -> D e. RR )
5		le2addd.5	|- ( ph -> A <_ C )
6		le2addd.6	|- ( ph -> B <_ D )
7	1 2	readdcld	|- ( ph -> ( A + B ) e. RR )
8	3 2	readdcld	|- ( ph -> ( C + B ) e. RR )
9	3 4	readdcld	|- ( ph -> ( C + D ) e. RR )
10	1 3 2 5	leadd1dd	|- ( ph -> ( A + B ) <_ ( C + B ) )
11	2 4 3 6	leadd2dd	|- ( ph -> ( C + B ) <_ ( C + D ) )
12	7 8 9 10 11	letrd	|- ( ph -> ( A + B ) <_ ( C + D ) )