Theorem xle2addd

Description: Adding both side of two inequalities. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	xle2addd.1	|- ( ph -> A e. RR* )
	xle2addd.2	|- ( ph -> B e. RR* )
	xle2addd.3	|- ( ph -> C e. RR* )
	xle2addd.4	|- ( ph -> D e. RR* )
	xle2addd.5	|- ( ph -> A <_ C )
	xrle2addd.6	|- ( ph -> B <_ D )
Assertion	xle2addd	|- ( ph -> ( A +e B ) <_ ( C +e D ) )

Proof

Step	Hyp	Ref	Expression
1		xle2addd.1	|- ( ph -> A e. RR* )
2		xle2addd.2	|- ( ph -> B e. RR* )
3		xle2addd.3	|- ( ph -> C e. RR* )
4		xle2addd.4	|- ( ph -> D e. RR* )
5		xle2addd.5	|- ( ph -> A <_ C )
6		xrle2addd.6	|- ( ph -> B <_ D )
7	1 2	xaddcld	|- ( ph -> ( A +e B ) e. RR* )
8	1 4	xaddcld	|- ( ph -> ( A +e D ) e. RR* )
9	3 4	xaddcld	|- ( ph -> ( C +e D ) e. RR* )
10	2 4 1 6	xleadd2d	|- ( ph -> ( A +e B ) <_ ( A +e D ) )
11	1 3 4 5	xleadd1d	|- ( ph -> ( A +e D ) <_ ( C +e D ) )
12	7 8 9 10 11	xrletrd	|- ( ph -> ( A +e B ) <_ ( C +e D ) )