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