let m be Integer; :: thesis: for x, y, z being non zero Integer st ((x / y) + (y / z)) + (z / x) = m & x,y,z are_mutually_coprime holds
( ( x = 1 or x = - 1 ) & ( y = 1 or y = - 1 ) & ( z = 1 or z = - 1 ) )
let x, y, z be non zero Integer; :: thesis: ( ((x / y) + (y / z)) + (z / x) = m & x,y,z are_mutually_coprime implies ( ( x = 1 or x = - 1 ) & ( y = 1 or y = - 1 ) & ( z = 1 or z = - 1 ) ) )
assume ((x / y) + (y / z)) + (z / x) = m ; :: thesis: ( not x,y,z are_mutually_coprime or ( ( x = 1 or x = - 1 ) & ( y = 1 or y = - 1 ) & ( z = 1 or z = - 1 ) ) )
then A1: (((x ^2) * z) + ((y ^2) * x)) + ((z ^2) * y) = ((m * x) * y) * z by Th107;
assume A2: x,y,z are_mutually_coprime ; :: thesis: ( ( x = 1 or x = - 1 ) & ( y = 1 or y = - 1 ) & ( z = 1 or z = - 1 ) )
A3: y divides ((m * x) * z) * y ;
A4: y divides (z ^2) * y ;
y divides (x * y) * y ;
then y divides (((m * x) * z) * y) - ((y ^2) * x) by A3, INT_5:1;
then A5: y divides ((((m * x) * z) * y) - ((y ^2) * x)) - ((z ^2) * y) by A4, INT_5:1;
A6: z divides ((m * x) * y) * z ;
A7: z divides (y * z) * z ;
z divides (x ^2) * z ;
then z divides (((m * x) * y) * z) - ((x ^2) * z) by A6, INT_5:1;
then A8: z divides ((((m * x) * y) * z) - ((x ^2) * z)) - ((z ^2) * y) by A7, INT_5:1;
A9: x divides ((m * y) * z) * x ;
A10: x divides (x * z) * x ;
x divides (y ^2) * x ;
then x divides (((m * y) * z) * x) - ((y ^2) * x) by A9, INT_5:1;
then A11: x divides ((((m * y) * z) * x) - ((y ^2) * x)) - ((x ^2) * z) by A10, INT_5:1;
z ^2 = z |^ 2 by WSIERP_1:1;
then z ^2 ,x are_coprime by A2, WSIERP_1:10;
hence ( x = 1 or x = - 1 ) by A1, A2, A11, INT_2:25, Th14; :: thesis: ( ( y = 1 or y = - 1 ) & ( z = 1 or z = - 1 ) )
x ^2 = x |^ 2 by WSIERP_1:1;
then x ^2 ,y are_coprime by A2, WSIERP_1:10;
hence ( y = 1 or y = - 1 ) by A1, A2, A5, INT_2:25, Th14; :: thesis: ( z = 1 or z = - 1 )
y ^2 = y |^ 2 by WSIERP_1:1;
then y ^2 ,z are_coprime by A2, WSIERP_1:10;
hence ( z = 1 or z = - 1 ) by A1, A2, A8, INT_2:25, Th14; :: thesis: verum