given x, y, z being positive Nat such that A1: ((x / y) + (y / z)) + (z / x) = 2 ; :: thesis: contradiction

per cases ( ( x / y = y / z & y / z = z / x ) or x / y <> y / z or y / z <> z / x ) ;

suppose A2: ( x / y = y / z & y / z = z / x ) ; :: thesis: contradiction

((x / y) * (y / z)) * (z / x) = 1 by Multiply1;
then ((x / y) |^ 2) * (z / x) = 1 by A2, NEWTON:81;
then (x / y) |^ (2 + 1) = 1 by A2, NEWTON:6;
then x / y = 3 -Root 1 by PREPOWER:19;
then x / y = 1 by PREPOWER:20;
hence contradiction by A1, A2; :: thesis: verum

end;

suppose D1: ( x / y <> y / z or y / z <> z / x ) ; :: thesis: contradiction

set a = x / y;
set b = y / z;
set c = z / x;
((((x / y) + (y / z)) + (z / x)) / 3) |^ 3 > ((x / y) * (y / z)) * (z / x) by SERIES3, D1;
then ((((x / y) + (y / z)) + (z / x)) / 3) |^ 3 > 1 by Multiply1;
then 3 -Root (((((x / y) + (y / z)) + (z / x)) / 3) |^ 3) > 3 -Root 1 by PREPOWER:28;
then 3 -Root (((((x / y) + (y / z)) + (z / x)) / 3) |^ 3) > 1 by PREPOWER:20;
then (((x / y) + (y / z)) + (z / x)) / 3 > 1 by PREPOWER:19;
hence contradiction by A1; :: thesis: verum

end;

end;