let m be Real; :: thesis: ( 0 <= m & m < 4 implies for x, y, z, t being positive Integer holds not (((x / y) + (y / z)) + (z / t)) + (t / x) = m )
assume A1: 0 <= m ; :: thesis: ( not m < 4 or for x, y, z, t being positive Integer holds not (((x / y) + (y / z)) + (z / t)) + (t / x) = m )
assume m < 4 ; :: thesis: for x, y, z, t being positive Integer holds not (((x / y) + (y / z)) + (z / t)) + (t / x) = m
then A2: m / 4 < 4 / 4 by XREAL_1:74;
given x, y, z, t being positive Integer such that A3: (((x / y) + (y / z)) + (z / t)) + (t / x) = m ; :: thesis: contradiction
(((x / y) * (y / z)) * (z / t)) * (t / x) = 1 by Lm18;
then (m / 4) |^ 4 >= 1 |^ 4 by A3, Lm20;
hence contradiction by A1, A2, PREPOWER:10; :: thesis: verum