Metamath Proof Explorer


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
lt2.2 B
lt2.3 C
lt.4 D
Assertion lt2addi A<CB<DA+B<C+D

Proof

Step Hyp Ref Expression
1 lt2.1 A
2 lt2.2 B
3 lt2.3 C
4 lt.4 D
5 lt2add ABCDA<CB<DA+B<C+D
6 1 2 3 4 5 mp4an A<CB<DA+B<C+D