Description: Lemma for tcphcph : the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tcphval.n | |
|
tcphcph.v | |
||
tcphcph.f | |
||
tcphcph.1 | |
||
tcphcph.2 | |
||
tcphcph.h | |
||
tcphcph.3 | |
||
tcphcph.4 | |
||
tcphcph.k | |
||
tcphcph.m | |
||
tcphcphlem1.3 | |
||
tcphcphlem1.4 | |
||
Assertion | tcphcphlem1 | |