Theorem lt2addi

Description: Adding both side of two inequalities. Theorem I.25 of Apostol p. 20. (Contributed by NM, 14-May-1999)

	Ref	Expression
Hypotheses	lt2.1	|- A e. RR
	lt2.2	|- B e. RR
	lt2.3	|- C e. RR
	lt.4	|- D e. RR
Assertion	lt2addi	|- ( ( A < C /\ B < D ) -> ( A + B ) < ( C + D ) )

Proof

Step	Hyp	Ref	Expression
1		lt2.1	|- A e. RR
2		lt2.2	|- B e. RR
3		lt2.3	|- C e. RR
4		lt.4	|- D e. RR
5		lt2add	|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A < C /\ B < D ) -> ( A + B ) < ( C + D ) ) )
6	1 2 3 4 5	mp4an	|- ( ( A < C /\ B < D ) -> ( A + B ) < ( C + D ) )