This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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