let x, y, z, t be positive Integer; :: thesis: ( (((1 / (x ^2)) + (1 / (y ^2))) + (1 / (z ^2))) + (1 / (t ^2)) = 1 iff ( x = 2 & y = 2 & z = 2 & t = 2 ) )
thus ( (((1 / (x ^2)) + (1 / (y ^2))) + (1 / (z ^2))) + (1 / (t ^2)) = 1 implies ( x = 2 & y = 2 & z = 2 & t = 2 ) ) :: thesis: ( x = 2 & y = 2 & z = 2 & t = 2 implies (((1 / (x ^2)) + (1 / (y ^2))) + (1 / (z ^2))) + (1 / (t ^2)) = 1 )

proof

assume A1: (((1 / (x ^2)) + (1 / (y ^2))) + (1 / (z ^2))) + (1 / (t ^2)) = 1 ; :: thesis: ( x = 2 & y = 2 & z = 2 & t = 2 )
( (((1 / (x ^2)) + (1 / (y ^2))) + (1 / (z ^2))) + (1 / (t ^2)) = (((1 / (t ^2)) + (1 / (x ^2))) + (1 / (y ^2))) + (1 / (z ^2)) & (((1 / (t ^2)) + (1 / (x ^2))) + (1 / (y ^2))) + (1 / (z ^2)) = (((1 / (z ^2)) + (1 / (t ^2))) + (1 / (x ^2))) + (1 / (y ^2)) & (((1 / (z ^2)) + (1 / (t ^2))) + (1 / (x ^2))) + (1 / (y ^2)) = (((1 / (y ^2)) + (1 / (z ^2))) + (1 / (t ^2))) + (1 / (x ^2)) ) ;
then A2: ( x <> 1 + 0 & y <> 1 + 0 & z <> 1 + 0 & t <> 1 + 0 ) by A1, XREAL_1:6;
then A3: ( x >= 2 & y >= 2 & z >= 2 & t >= 2 ) by NAT_1:23;
A4: ( 1 / (x ^2) <= 1 / 4 & 1 / (y ^2) <= 1 / 4 & 1 / (z ^2) <= 1 / 4 & 1 / (t ^2) <= 1 / 4 ) by A2, Lm10, NAT_1:23;

A5: now :: thesis: not x > 2

assume x > 2 ; :: thesis: contradiction
then A6: 1 / (x ^2) <= 1 / 9 by Lm11;
(1 / (y ^2)) + (1 / (z ^2)) <= (1 / 4) + (1 / 4) by A4, XREAL_1:7;
then ((1 / (y ^2)) + (1 / (z ^2))) + (1 / (t ^2)) <= ((1 / 4) + (1 / 4)) + (1 / 4) by A4, XREAL_1:7;
then (1 / (x ^2)) + (((1 / (y ^2)) + (1 / (z ^2))) + (1 / (t ^2))) <= (1 / 9) + (((1 / 4) + (1 / 4)) + (1 / 4)) by A6, XREAL_1:7;
hence contradiction by A1; :: thesis: verum

end;

A7: now :: thesis: not y > 2

assume y > 2 ; :: thesis: contradiction
then A8: 1 / (y ^2) <= 1 / 9 by Lm11;
(1 / (z ^2)) + (1 / (t ^2)) <= (1 / 4) + (1 / 4) by A4, XREAL_1:7;
then ((1 / (z ^2)) + (1 / (t ^2))) + (1 / (x ^2)) <= ((1 / 4) + (1 / 4)) + (1 / 4) by A4, XREAL_1:7;
then (1 / (y ^2)) + (((1 / (z ^2)) + (1 / (t ^2))) + (1 / (x ^2))) <= (1 / 9) + (((1 / 4) + (1 / 4)) + (1 / 4)) by A8, XREAL_1:7;
hence contradiction by A1; :: thesis: verum

end;

A9: now :: thesis: not z > 2

assume z > 2 ; :: thesis: contradiction
then A10: 1 / (z ^2) <= 1 / 9 by Lm11;
(1 / (t ^2)) + (1 / (x ^2)) <= (1 / 4) + (1 / 4) by A4, XREAL_1:7;
then ((1 / (t ^2)) + (1 / (x ^2))) + (1 / (y ^2)) <= ((1 / 4) + (1 / 4)) + (1 / 4) by A4, XREAL_1:7;
then (1 / (z ^2)) + (((1 / (t ^2)) + (1 / (x ^2))) + (1 / (y ^2))) <= (1 / 9) + (((1 / 4) + (1 / 4)) + (1 / 4)) by A10, XREAL_1:7;
hence contradiction by A1; :: thesis: verum

end;

now :: thesis: not t > 2

assume t > 2 ; :: thesis: contradiction
then A11: 1 / (t ^2) <= 1 / 9 by Lm11;
(1 / (x ^2)) + (1 / (y ^2)) <= (1 / 4) + (1 / 4) by A4, XREAL_1:7;
then ((1 / (x ^2)) + (1 / (y ^2))) + (1 / (z ^2)) <= ((1 / 4) + (1 / 4)) + (1 / 4) by A4, XREAL_1:7;
then (1 / (t ^2)) + (((1 / (x ^2)) + (1 / (y ^2))) + (1 / (z ^2))) <= (1 / 9) + (((1 / 4) + (1 / 4)) + (1 / 4)) by A11, XREAL_1:7;
hence contradiction by A1; :: thesis: verum

end;

hence ( x = 2 & y = 2 & z = 2 & t = 2 ) by A3, A5, A7, A9, XXREAL_0:1; :: thesis: verum

end;

thus ( x = 2 & y = 2 & z = 2 & t = 2 implies (((1 / (x ^2)) + (1 / (y ^2))) + (1 / (z ^2))) + (1 / (t ^2)) = 1 ) ; :: thesis: verum