Description: A sum is less than the whole if each term is less than half. (Contributed by Thierry Arnoux, 29-Nov-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | le2halvesd.1 | |- ( ph -> A e. RR ) |
|
le2halvesd.2 | |- ( ph -> B e. RR ) |
||
le2halvesd.3 | |- ( ph -> C e. RR ) |
||
le2halvesd.4 | |- ( ph -> A <_ ( C / 2 ) ) |
||
le2halvesd.5 | |- ( ph -> B <_ ( C / 2 ) ) |
||
Assertion | le2halvesd | |- ( ph -> ( A + B ) <_ C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | le2halvesd.1 | |- ( ph -> A e. RR ) |
|
2 | le2halvesd.2 | |- ( ph -> B e. RR ) |
|
3 | le2halvesd.3 | |- ( ph -> C e. RR ) |
|
4 | le2halvesd.4 | |- ( ph -> A <_ ( C / 2 ) ) |
|
5 | le2halvesd.5 | |- ( ph -> B <_ ( C / 2 ) ) |
|
6 | 3 | rehalfcld | |- ( ph -> ( C / 2 ) e. RR ) |
7 | 1 2 6 6 4 5 | le2addd | |- ( ph -> ( A + B ) <_ ( ( C / 2 ) + ( C / 2 ) ) ) |
8 | 3 | recnd | |- ( ph -> C e. CC ) |
9 | 8 | 2halvesd | |- ( ph -> ( ( C / 2 ) + ( C / 2 ) ) = C ) |
10 | 7 9 | breqtrd | |- ( ph -> ( A + B ) <_ C ) |