let m be Nat; :: thesis: ( m <> 3 implies for x, y, z being non zero Integer holds
( not ((x / y) + (y / z)) + (z / x) = m or not x,y,z are_mutually_coprime ) )
assume A1: m <> 3 ; :: thesis: for x, y, z being non zero Integer holds
( not ((x / y) + (y / z)) + (z / x) = m or not x,y,z are_mutually_coprime )
given x, y, z being non zero Integer such that A2: ((x / y) + (y / z)) + (z / x) = m and
A3: x,y,z are_mutually_coprime ; :: thesis: contradiction
( ( x = 1 or x = - 1 ) & ( y = 1 or y = - 1 ) & ( z = 1 or z = - 1 ) ) by A2, A3, Th108;
hence contradiction by A1, A2; :: thesis: verum