Metamath Proof Explorer


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 ) )