let x, y, z be positive Nat; :: thesis: ( ((x |^ 3) + (y |^ 3)) + (z |^ 3) = ((3 * x) * y) * z implies ( x = y & y = z ) )
assume A1: ((x |^ 3) + (y |^ 3)) + (z |^ 3) = ((3 * x) * y) * z ; :: thesis: ( x = y & 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)
.= (((3 * x) * y) * z) / ((x * y) * z) by A1
.= 3 * (((x * y) * z) / ((x * y) * z))
.= 3 * 1 by XCMPLX_1:60
.= 3 ;
then ((((x ^2) * y) / ((y ^2) * z)) + (((y ^2) * z) / ((z ^2) * x))) + (((z ^2) * x) / ((x ^2) * y)) = 3 by A2, A3, A4;
then C0: ( (x ^2) * y = (y ^2) * z & (y ^2) * z = (z ^2) * x ) by NUMBER12:63;
set n = (x ^2) * y;
(((x ^2) * y) * ((y ^2) * z)) * ((z ^2) * x) = (((x ^2) * y) * ((x ^2) * y)) * ((x ^2) * y) by C0;
then (((x * y) * z) * ((x * y) * z)) * ((x * y) * z) = (((x ^2) * y) * ((x ^2) * y)) * ((x ^2) * y) ;
then ((x * y) * z) |^ 3 = (((x ^2) * y) * ((x ^2) * y)) * ((x ^2) * y) by Lm1;
then ((x * y) * z) |^ 3 = ((x ^2) * y) |^ 3 by Lm1;
then D1: (x * y) * z = (x ^2) * y by NEWTON03:12;
z / x = (z * (x * y)) / (x * (x * y)) by XCMPLX_1:91
.= 1 by D1, XCMPLX_1:60 ;
then T1: z = x by XCMPLX_1:58;
x / y = (x * (y * z)) / (y * (y * z)) by XCMPLX_1:91
.= 1 by C0, D1, XCMPLX_1:60 ;
hence ( x = y & y = z ) by T1, XCMPLX_1:58; :: thesis: verum