given p, q, r, s, t being Prime such that A1: (p ^2) + (q ^2) = ((r ^2) + (s ^2)) + (t ^2) ; :: thesis: contradiction
A2: now :: thesis: not p = r
assume p = r ; :: thesis: contradiction
then (p ^2) + (q ^2) = (p ^2) + ((s ^2) + (t ^2)) by A1;
hence contradiction by Th39; :: thesis: verum
end;
A3: now :: thesis: not p = s
assume p = s ; :: thesis: contradiction
then (p ^2) + (q ^2) = (p ^2) + ((r ^2) + (t ^2)) by A1;
hence contradiction by Th39; :: thesis: verum
end;
A4: p <> t by A1, Th39;
A5: now :: thesis: not q = r
assume q = r ; :: thesis: contradiction
then (p ^2) + (q ^2) = (q ^2) + ((s ^2) + (t ^2)) by A1;
hence contradiction by Th39; :: thesis: verum
end;
A6: now :: thesis: not q = s
assume q = s ; :: thesis: contradiction
then (p ^2) + (q ^2) = (q ^2) + ((r ^2) + (t ^2)) by A1;
hence contradiction by Th39; :: thesis: verum
end;
A7: q <> t by A1, Th39;
A8: ((p ^2) + (q ^2)) mod 8 = (((p ^2) mod 8) + ((q ^2) mod 8)) mod 8 by NAT_D:66;
A9: ((r ^2) + (s ^2)) mod 8 = (((r ^2) mod 8) + ((s ^2) mod 8)) mod 8 by NAT_D:66;
A10: (((r ^2) + (s ^2)) + (t ^2)) mod 8 = ((((r ^2) + (s ^2)) mod 8) + ((t ^2) mod 8)) mod 8 by NAT_D:66;
A11: (2 ^2) mod 8 = 4 by NAT_D:24;
per cases ( p is even or q is even or ( p is odd & q is odd ) ) ;
suppose ( p is even or q is even ) ; :: thesis: contradiction
then A12: ( p = 2 or q = 2 ) by LAGRA4SQ:13;
then A13: r is odd by A2, A5, LAGRA4SQ:13;
then A14: (r ^2) mod 8 = 1 by Th37;
A15: s is odd by A3, A6, A12, LAGRA4SQ:13;
then A16: (s ^2) mod 8 = 1 by Th37;
A17: t is odd by A4, A7, A12, LAGRA4SQ:13;
then A18: (t ^2) mod 8 = 1 by Th37;
A19: ( p is even implies q is odd ) by A1, A13, A15, A17;
A20: ((p ^2) + (q ^2)) mod 8 = (1 + 4) mod 8 by A8, A12, A11, A19, Th37
.= 5 by NAT_D:24 ;
(((r ^2) + (s ^2)) + (t ^2)) mod 8 = (2 + 1) mod 8 by A9, A10, A16, A18, A14, NAT_D:24
.= 3 by NAT_D:24 ;
hence contradiction by A1, A20; :: thesis: verum
end;
suppose A21: ( p is odd & q is odd ) ; :: thesis: contradiction
then ( (p ^2) mod 8 = 1 & (q ^2) mod 8 = 1 ) by Th37;
then A22: ((p ^2) + (q ^2)) mod 8 = 2 by A8, NAT_D:24;
per cases ( ( r is even & s is odd ) or ( r is even & t is even ) or ( s is even & t is odd ) or ( s is even & r is even ) or ( t is even & r is odd ) or ( t is even & s is even ) ) by A1, A21;
end;
end;
end;