Triangle Requirements based of triangle Inequality In a Geometry course we are dealing with triangle inequality and two statements arose:
"For any triangle, any side is smaller the the sum of the others." and "For any triangle, the largest side is smaller than the sum of the others."
I can represent that logically using
$$(\forall A,B,C)(\triangle ABC \Leftrightarrow ((AB<BC+CA)\wedge (BC<CA+AB)\wedge (CA<AB+BC)))$$
and 
$$\begin{align}
(\forall A,B,C)(\triangle ABC \Leftrightarrow &
(((AB<BC+CA)\wedge (AB\ge BC)\wedge (AB\ge CA))\vee\\
&((BC<CA+AB)\wedge (BC\ge AB)\wedge (BC\ge CA))\vee\\
&((CA<AB+BC)\wedge (CA\ge AB)\wedge (CA\ge BC))))
\end{align}$$
How can I go from one logical statement to the other?
EDIT: Fixed the quantifiers, now I can read it as: "For any A, B, C, ABC forms a triangle if and only if ... right hand side conditions ..."
 A: Edited to match the revised question and to reduce notational clash:
You’re making matters much more difficult than they need to be by trying to formalize the notion symbolically. If you simply want to show that the two definitions are equivalent, don’t mess around with the formalizations. It’s also simpler if you denote the lengths of the sides by single letters.
The first definition clearly implies the second. To go from the second to the first, let the lengths of the sides be $x,y$, and $z$, and assume that $x\le y\le z$ and $z<x+y$ (i.e., the longest side is less than the sum of the other two). You need to show that $x<y+z$ and $y<x+z$. To show that $y<x+z$, merely observe that $y\le z<x+y\le x+z$; the proof that $x<y+z$ is similar.
A: Here is the passage from the second statement to the first.
We start with this:
$$(((AB<BC+CA)\wedge (AB\ge BC)\wedge (AB\ge CA))\vee\\
((BC<CA+AB)\wedge (BC\ge AB)\wedge (BC\ge CA))\vee\\
((CA<AB+BC)\wedge (CA\ge AB)\wedge (CA\ge BC)))$$
Lets use letters P1, P2, P3, Q1, Q2, Q3, R1, R2, R3 to identify each invividual sentence of the expression, also we double negate everything:
$$\neg\neg ((P1\wedge P2\wedge P3)\vee (Q1\wedge Q2\wedge Q3)\vee (R1\wedge R2\wedge R3))$$
$$\neg ((\neg P1\vee \neg P2 \vee \neg P3)\wedge (\neg Q1\vee \neg Q2\vee \neg Q3)\wedge (\neg R1\vee \neg R2\vee \neg R3))$$
Expanding we arrive at this messy monster:
$$\neg 
(\neg P1 \wedge \neg Q1 \wedge \neg R1) \vee
(\neg P1 \wedge \neg Q1 \wedge \neg R2) \vee
(\neg P1 \wedge \neg Q1 \wedge \neg R3) \vee\\
(\neg P1 \wedge \neg Q2 \wedge \neg R1) \vee
(\neg P1 \wedge \neg Q2 \wedge \neg R2) \vee
(\neg P1 \wedge \neg Q2 \wedge \neg R3) \vee\\
(\neg P1 \wedge \neg Q3 \wedge \neg R1) \vee
(\neg P1 \wedge \neg Q3 \wedge \neg R2) \vee
(\neg P1 \wedge \neg Q3 \wedge \neg R3) \vee\\
(\neg P2 \wedge \neg Q1 \wedge \neg R1) \vee
(\neg P2 \wedge \neg Q1 \wedge \neg R2) \vee
(\neg P2 \wedge \neg Q1 \wedge \neg R3) \vee\\
(\neg P2 \wedge \neg Q2 \wedge \neg R1) \vee
(\neg P2 \wedge \neg Q2 \wedge \neg R2) \vee
(\neg P2 \wedge \neg Q2 \wedge \neg R3) \vee\\
(\neg P2 \wedge \neg Q3 \wedge \neg R1) \vee
(\neg P2 \wedge \neg Q3 \wedge \neg R2) \vee
(\neg P2 \wedge \neg Q3 \wedge \neg R3) \vee\\
(\neg P3 \wedge \neg Q1 \wedge \neg R1) \vee
(\neg P3 \wedge \neg Q1 \wedge \neg R2) \vee
(\neg P3 \wedge \neg Q1 \wedge \neg R3) \vee\\
(\neg P3 \wedge \neg Q2 \wedge \neg R1) \vee
(\neg P3 \wedge \neg Q2 \wedge \neg R2) \vee
(\neg P3 \wedge \neg Q2 \wedge \neg R3) \vee\\
(\neg P3 \wedge \neg Q3 \wedge \neg R1) \vee
(\neg P3 \wedge \neg Q3 \wedge \neg R2) \vee
(\neg P3 \wedge \neg Q3 \wedge \neg R3) )$$
Many sentences will be obvious contradictions and can be eliminated, like: $\neg P2\wedge  \neg Q2$, which essentially says $AB<BC\wedge BC<AB$, and $\neg P1\wedge\neg Q1$ (since every side is bigger than 0). Thus ending up with this (rearranged):
$$\neg 
(\neg P1 \wedge \neg Q2 \wedge \neg R2) \vee
(\neg P1 \wedge \neg Q2 \wedge \neg R3) \vee
(\neg P1 \wedge \neg Q3 \wedge \neg R2) \vee\\
(\neg Q1 \wedge \neg P2 \wedge \neg R2) \vee
(\neg Q1 \wedge \neg P2 \wedge \neg R3) \vee
(\neg Q1 \wedge \neg P3 \wedge \neg R3) \vee\\
(\neg R1 \wedge \neg P2 \wedge \neg Q3) \vee
(\neg R1 \wedge \neg P3 \wedge \neg Q2) \vee
(\neg R1 \wedge \neg P3 \wedge \neg Q3) \vee\\
(\neg P2 \wedge \neg Q3 \wedge \neg R2) \vee
(\neg P3 \wedge \neg Q2 \wedge \neg R3))$$
Then we can group by P1, Q1 and R1, and also eliminate the last two sentences since they are obvious contradictions, eg: $AB<BC\wedge BC<CA\wedge CA<AB$.
$$\neg (
(\neg P1 \wedge ((\neg Q2 \wedge \neg R2) \vee (\neg Q2 \wedge \neg R3) \vee (\neg Q3 \wedge \neg R2)))\vee\\
(\neg Q1 \wedge ((\neg P2 \wedge \neg R2) \vee (\neg P2 \wedge \neg R3) \vee (\neg P3 \wedge \neg R3)))\vee\\
(\neg R1 \wedge ((\neg P2 \wedge \neg Q3) \vee (\neg P3 \wedge \neg Q2) \vee (\neg P3 \wedge \neg Q3)))
)$$
Since all cases are similar lets evaluate just the first one and replicate the results:
$$(\neg P1 \wedge ((\neg Q2 \wedge \neg R2) \vee (\neg Q2 \wedge \neg R3) \vee (\neg Q3 \wedge \neg R2)))$$
Using the actual expressions and rearraging:
$$((AB\ge BC+CA) \wedge \\((AB>BC \wedge AB>CA) \vee (AB>BC>CA) \vee (AB>CA>BC)))$$
Since I'm already saying the AB is greater or equal than the sum of the other sides, then AB is greater than any side alone and the 3 possible relations between BC and CA are ORed, so rest of the expression must evaluate to true, therefore the above expression can be resumed to $(AB\ge BC+CA)$ which is $(\neg P1)$ in our case. Going back and replicating this result we obtain:
$$\neg ((\neg P1)\vee(\neg Q1)\vee(\neg R1))$$
Applying the final negation we get:
$$P1\wedge Q1\wedge R1$$
Which is:
$$(AB<BC+CA)\wedge(BC<CA+AB)\wedge(CA<AB+BC)$$
Q.E.D. ;)
Is there anything wrong with my process? I only accept that anwser if it can be verified to be true.
BTW: I double negate the expression just because some relations got easier to see. Also, in a long list of ORed expressions you can just remove the contradictory ones, where in a list of ANDed expressions you have to prove the tautology of any expression to be able to remove it, and that is generally harder to prove than a contradiction.
