Description: Triangle inequality for absolute value. Proposition 10-3.7(h) of Gleason p. 133. This is Metamath 100 proof #91. (Contributed by NM, 2-Oct-1999)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | absvalsqi.1 | |- A e. CC |
|
| abssub.2 | |- B e. CC |
||
| Assertion | abstrii | |- ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | absvalsqi.1 | |- A e. CC |
|
| 2 | abssub.2 | |- B e. CC |
|
| 3 | abstri | |- ( ( A e. CC /\ B e. CC ) -> ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) ) |
|
| 4 | 1 2 3 | mp2an | |- ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) |