Description: Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ltadd12dd.a | |- ( ph -> A e. RR ) |
|
ltadd12dd.b | |- ( ph -> B e. RR ) |
||
ltadd12dd.c | |- ( ph -> C e. RR ) |
||
ltadd12dd.d | |- ( ph -> D e. RR ) |
||
ltadd12dd.ac | |- ( ph -> A < C ) |
||
ltadd12dd.bd | |- ( ph -> B < D ) |
||
Assertion | ltadd12dd | |- ( ph -> ( A + B ) < ( C + D ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltadd12dd.a | |- ( ph -> A e. RR ) |
|
2 | ltadd12dd.b | |- ( ph -> B e. RR ) |
|
3 | ltadd12dd.c | |- ( ph -> C e. RR ) |
|
4 | ltadd12dd.d | |- ( ph -> D e. RR ) |
|
5 | ltadd12dd.ac | |- ( ph -> A < C ) |
|
6 | ltadd12dd.bd | |- ( ph -> B < D ) |
|
7 | 1 2 | readdcld | |- ( ph -> ( A + B ) e. RR ) |
8 | 3 2 | readdcld | |- ( ph -> ( C + B ) e. RR ) |
9 | 3 4 | readdcld | |- ( ph -> ( C + D ) e. RR ) |
10 | 1 3 2 5 | ltadd1dd | |- ( ph -> ( A + B ) < ( C + B ) ) |
11 | 2 4 3 6 | ltadd2dd | |- ( ph -> ( C + B ) < ( C + D ) ) |
12 | 7 8 9 10 11 | lttrd | |- ( ph -> ( A + B ) < ( C + D ) ) |