assume ex x, y, z being positive Nat st ((x |^ 3) + (y |^ 3)) + (z |^ 3) = (x * y) * z ; :: thesis: contradiction
then consider x, y, z being positive Nat such that
A1: ((x |^ 3) + (y |^ 3)) + (z |^ 3) = (x * y) * z ;
set X = (x ^2) * y;
set Y = (y ^2) * z;
set Z = (z ^2) * x;
A2: ((x ^2) * y) / ((y ^2) * z) = ((x * x) * y) / ((y * z) * y)
.= (x * x) / (y * z) by XCMPLX_1:91
.= ((x * x) * x) / ((y * z) * x) by XCMPLX_1:91
.= (x |^ 3) / ((x * y) * z) by Lm1 ;
A3: ((y ^2) * z) / ((z ^2) * x) = ((y * y) * z) / ((z * x) * z)
.= (y * y) / (z * x) by XCMPLX_1:91
.= ((y * y) * y) / ((z * x) * y) by XCMPLX_1:91
.= (y |^ 3) / ((x * y) * z) by Lm1 ;
A4: ((z ^2) * x) / ((x ^2) * y) = ((z * z) * x) / ((x * y) * x)
.= (z * z) / (x * y) by XCMPLX_1:91
.= ((z * z) * z) / ((x * y) * z) by XCMPLX_1:91
.= (z |^ 3) / ((x * y) * z) by Lm1 ;
(((x |^ 3) / ((x * y) * z)) + ((y |^ 3) / ((x * y) * z))) + ((z |^ 3) / ((x * y) * z)) = (((x |^ 3) + (y |^ 3)) + (z |^ 3)) / ((x * y) * z)
.= 1 by A1, XCMPLX_1:60 ;
hence contradiction by A2, A3, A4, NUMBER12:59; :: thesis: verum