Re: Struggling to prove simple triangle inequality

• To: mathgroup at smc.vnet.net
• Subject: [mg126331] Re: Struggling to prove simple triangle inequality
• Date: Tue, 1 May 2012 14:57:32 -0400 (EDT)
• Delivered-to: l-mathgroup@mail-archive0.wolfram.com
• References: <201204300842.EAA23670@smc.vnet.net> <jnoa64\$54o\$1@smc.vnet.net>

```On May 1, 12:25 pm, Andrzej Kozlowski <akozlow... at gmail.com> wrote:
> > Given two 3D vectors A and B, I want to prove that length of their sum
> > is less or equal than the sum of their lengths:
>
> > length[v_] := Sqrt[v.v];
> > a = {ax, ay, az};
> > b = {bx, by, bz};
> > inequality = length[a + b] <= length[a] + length[b];
>
> > vars = {ax, ay, az, bx, by, bz};
> > Reduce[inequality, vars, Reals]
>
> Not really. To solve this sort of problem Reduce uses the algorithm
> called cylindrical algebraic decomposition, which is implemented in
> Mathematica as CylindricalDecomposition. This algorithm's complexity is
> double exponential (i.e. 2^n^n where n is the number of variables.).

Thanks for explanation. Meanwhile, Reduce has run for a few days
at 3 GHz, taking gigabytes of memory and finally crashed the kernel.
Looks like besides checking many combinations, a huge memory is
needed for something (list-based methods instead of iteration-based?)

Anyway, if not Reduce, maybe something else could help
to automatically prove this seemingly simple problem?

--
All the best,