given x, y, z being Rational such that A1: ((x ^2) + (y ^2)) + (z ^2) = 7 ; :: thesis: contradiction
consider n1, m1 being Integer such that
A2: m1 > 0 and
A3: x = n1 / m1 by RAT_1:2;
consider n2, m2 being Integer such that
A4: m2 > 0 and
A5: y = n2 / m2 by RAT_1:2;
consider n3, m3 being Integer such that
A6: m3 > 0 and
A7: z = n3 / m3 by RAT_1:2;
set m = (m1 * m2) * m3;
reconsider m = (m1 * m2) * m3 as Element of NAT by A2, A4, A6, INT_1:3;
set a = (n1 * m2) * m3;
set b = (n2 * m1) * m3;
set c = (n3 * m1) * m2;
defpred S₁[ Nat] means ( $1 <> 0 & ex a, b, c being Integer st 7 * ($1 ^2) = ((a ^2) + (b ^2)) + (c ^2) );
A8: ( (n1 / m1) ^2 = (n1 ^2) / (m1 ^2) & (n2 / m2) ^2 = (n2 ^2) / (m2 ^2) & (n3 / m3) ^2 = (n3 ^2) / (m3 ^2) ) by XCMPLX_1:76;
((n1 ^2) / (m1 ^2)) + ((n2 ^2) / (m2 ^2)) = (((n1 ^2) * (m2 ^2)) + ((n2 ^2) * (m1 ^2))) / ((m1 ^2) * (m2 ^2)) by A2, A4, XCMPLX_1:116;
then 7 = (((((n1 ^2) * (m2 ^2)) + ((n2 ^2) * (m1 ^2))) * (m3 ^2)) + ((n3 ^2) * ((m1 ^2) * (m2 ^2)))) / (((m1 ^2) * (m2 ^2)) * (m3 ^2)) by A1, A2, A3, A4, A5, A6, A7, A8, XCMPLX_1:116
.= (((((n1 * m2) * m3) ^2) + (((n2 * m1) * m3) ^2)) + (((n3 * m1) * m2) ^2)) / (m ^2) ;
then ((((n1 * m2) * m3) ^2) + (((n2 * m1) * m3) ^2)) + (((n3 * m1) * m2) ^2) = 7 * (m ^2) by A2, A4, A6, XCMPLX_1:87;
then A9: ex k being Nat st S₁[k] by A2, A4, A6;
consider M being Nat such that
A10: S₁[M] and
A11: for n being Nat st S₁[n] holds
M <= n from NAT_1:sch 5(A9);
consider a, b, c being Integer such that
A12: 7 * (M ^2) = ((a ^2) + (b ^2)) + (c ^2) by A10;

per cases ( M is even or M is odd ) ;

suppose M is even ; :: thesis: contradiction

then consider n being Nat such that
A13: M = 2 * n ;
A14: (4 * (7 * (n ^2))) mod 4 = 0 by NAT_D:13;
a is even by A13, A12, A14, Th91;
then consider a1 being Integer such that
A15: a = 2 * a1 by ABIAN:11;
b is even by A13, A12, A14, Th91;
then consider b1 being Integer such that
A16: b = 2 * b1 by ABIAN:11;
c is even by A13, A12, A14, Th91;
then consider c1 being Integer such that
A17: c = 2 * c1 by ABIAN:11;
A18: n <> 0 by A10, A13;
((a1 ^2) + (b1 ^2)) + (c1 ^2) = (((a / 2) ^2) + ((b / 2) ^2)) + ((c / 2) ^2) by A15, A16, A17
.= (7 * (M ^2)) / 4 by A12
.= 7 * (n ^2) by A13 ;
then 2 * n <= 1 * n by A18, A11, A13;
hence contradiction by A18, XREAL_1:68; :: thesis: verum

end;

suppose M is odd ; :: thesis: contradiction

then (M ^2) mod 8 = 1 by NUMBER05:41;
then (7 * (M ^2)) mod 8 = ((7 mod 8) * 1) mod 8 by NAT_D:67
.= 7 by NAT_D:24 ;
hence contradiction by A12, Th92; :: thesis: verum

end;

end;