let a, b, c be Integer; :: thesis: ( (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 3 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6 )
set x = ((a ^2) + (b ^2)) + (c ^2);
A1: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = ((((a ^2) mod 8) + ((b ^2) mod 8)) + ((c ^2) mod 8)) mod 8 by NUMBER05:8;
A2: ((1 * 8) + 1) mod 8 = 1 mod 8 by NAT_D:21
.= 1 by NAT_D:24 ;
now :: thesis: ( ( (a ^2) mod 8 = 0 & ( ( (b ^2) mod 8 = 0 & ( ( (c ^2) mod 8 = 0 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 ) or ( (c ^2) mod 8 = 1 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 ) or ( (c ^2) mod 8 = 4 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 ) ) ) or ( (b ^2) mod 8 = 1 & ( ( (c ^2) mod 8 = 0 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 ) or ( (c ^2) mod 8 = 1 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2 ) or ( (c ^2) mod 8 = 4 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 ) ) ) or ( (b ^2) mod 8 = 4 & ( ( (c ^2) mod 8 = 0 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 ) or ( (c ^2) mod 8 = 1 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 ) or ( (c ^2) mod 8 = 4 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 ) ) ) ) ) or ( (a ^2) mod 8 = 1 & ( ( (b ^2) mod 8 = 0 & ( ( (c ^2) mod 8 = 0 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 ) or ( (c ^2) mod 8 = 1 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2 ) or ( (c ^2) mod 8 = 4 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 ) ) ) or ( (b ^2) mod 8 = 1 & ( ( (c ^2) mod 8 = 0 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2 ) or ( (c ^2) mod 8 = 1 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 3 ) or ( (c ^2) mod 8 = 4 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6 ) ) ) or ( (b ^2) mod 8 = 4 & ( ( (c ^2) mod 8 = 0 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 ) or ( (c ^2) mod 8 = 1 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6 ) or ( (c ^2) mod 8 = 4 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 ) ) ) ) ) or ( (a ^2) mod 8 = 4 & ( ( (b ^2) mod 8 = 0 & ( ( (c ^2) mod 8 = 0 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 ) or ( (c ^2) mod 8 = 1 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 ) or ( (c ^2) mod 8 = 4 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 ) ) ) or ( (b ^2) mod 8 = 1 & ( ( (c ^2) mod 8 = 0 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 ) or ( (c ^2) mod 8 = 1 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6 ) or ( (c ^2) mod 8 = 4 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 ) ) ) or ( (b ^2) mod 8 = 4 & ( ( (c ^2) mod 8 = 0 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 ) or ( (c ^2) mod 8 = 1 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 ) or ( (c ^2) mod 8 = 4 & (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 ) ) ) ) ) )
per cases ( (a ^2) mod 8 = 0 or (a ^2) mod 8 = 1 or (a ^2) mod 8 = 4 ) by NUMBER10:61;
case A3: (a ^2) mod 8 = 0 ; :: thesis: verum
per cases ( (b ^2) mod 8 = 0 or (b ^2) mod 8 = 1 or (b ^2) mod 8 = 4 ) by NUMBER10:61;
case A4: (b ^2) mod 8 = 0 ; :: thesis: verum
per cases ( (c ^2) mod 8 = 0 or (c ^2) mod 8 = 1 or (c ^2) mod 8 = 4 ) by NUMBER10:61;
case (c ^2) mod 8 = 0 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 by A1, A3, A4; :: thesis: verum
end;
case (c ^2) mod 8 = 1 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 by A1, A3, A4; :: thesis: verum
end;
case (c ^2) mod 8 = 4 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 by A1, A3, A4; :: thesis: verum
end;
end;
end;
case A5: (b ^2) mod 8 = 1 ; :: thesis: verum
per cases ( (c ^2) mod 8 = 0 or (c ^2) mod 8 = 1 or (c ^2) mod 8 = 4 ) by NUMBER10:61;
case (c ^2) mod 8 = 0 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 by A1, A3, A5; :: thesis: verum
end;
case (c ^2) mod 8 = 1 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2 by A1, A3, A5, NAT_D:24; :: thesis: verum
end;
case (c ^2) mod 8 = 4 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 by A1, A3, A5, NAT_D:24; :: thesis: verum
end;
end;
end;
case A6: (b ^2) mod 8 = 4 ; :: thesis: verum
per cases ( (c ^2) mod 8 = 0 or (c ^2) mod 8 = 1 or (c ^2) mod 8 = 4 ) by NUMBER10:61;
case (c ^2) mod 8 = 0 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 by A1, A3, A6; :: thesis: verum
end;
case (c ^2) mod 8 = 1 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 by A1, A3, A6, NAT_D:24; :: thesis: verum
end;
case (c ^2) mod 8 = 4 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 by A1, A3, A6, NAT_D:25; :: thesis: verum
end;
end;
end;
end;
end;
case A7: (a ^2) mod 8 = 1 ; :: thesis: verum
per cases ( (b ^2) mod 8 = 0 or (b ^2) mod 8 = 1 or (b ^2) mod 8 = 4 ) by NUMBER10:61;
case A8: (b ^2) mod 8 = 0 ; :: thesis: verum
per cases ( (c ^2) mod 8 = 0 or (c ^2) mod 8 = 1 or (c ^2) mod 8 = 4 ) by NUMBER10:61;
case (c ^2) mod 8 = 0 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 by A1, A7, A8; :: thesis: verum
end;
case (c ^2) mod 8 = 1 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2 by A1, A7, A8, NAT_D:24; :: thesis: verum
end;
case (c ^2) mod 8 = 4 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 by A1, A7, A8, NAT_D:24; :: thesis: verum
end;
end;
end;
case A9: (b ^2) mod 8 = 1 ; :: thesis: verum
per cases ( (c ^2) mod 8 = 0 or (c ^2) mod 8 = 1 or (c ^2) mod 8 = 4 ) by NUMBER10:61;
case (c ^2) mod 8 = 0 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2 by A1, A7, A9, NAT_D:24; :: thesis: verum
end;
case (c ^2) mod 8 = 1 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 3
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 3 by A1, A7, A9, NAT_D:24; :: thesis: verum
end;
case (c ^2) mod 8 = 4 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6 by A1, A7, A9, NAT_D:24; :: thesis: verum
end;
end;
end;
case A10: (b ^2) mod 8 = 4 ; :: thesis: verum
per cases ( (c ^2) mod 8 = 0 or (c ^2) mod 8 = 1 or (c ^2) mod 8 = 4 ) by NUMBER10:61;
case (c ^2) mod 8 = 0 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 by A1, A7, A10, NAT_D:24; :: thesis: verum
end;
case (c ^2) mod 8 = 1 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6 by A1, A7, A10, NAT_D:24; :: thesis: verum
end;
case (c ^2) mod 8 = 4 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 by A2, A1, A7, A10; :: thesis: verum
end;
end;
end;
end;
end;
case A11: (a ^2) mod 8 = 4 ; :: thesis: verum
per cases ( (b ^2) mod 8 = 0 or (b ^2) mod 8 = 1 or (b ^2) mod 8 = 4 ) by NUMBER10:61;
case A12: (b ^2) mod 8 = 0 ; :: thesis: verum
per cases ( (c ^2) mod 8 = 0 or (c ^2) mod 8 = 1 or (c ^2) mod 8 = 4 ) by NUMBER10:61;
case (c ^2) mod 8 = 0 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 by A1, A11, A12; :: thesis: verum
end;
case (c ^2) mod 8 = 1 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 by A1, A11, A12, NAT_D:24; :: thesis: verum
end;
case (c ^2) mod 8 = 4 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 by A1, A11, A12, NAT_D:25; :: thesis: verum
end;
end;
end;
case A13: (b ^2) mod 8 = 1 ; :: thesis: verum
per cases ( (c ^2) mod 8 = 0 or (c ^2) mod 8 = 1 or (c ^2) mod 8 = 4 ) by NUMBER10:61;
case (c ^2) mod 8 = 0 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 by A1, A11, A13, NAT_D:24; :: thesis: verum
end;
case (c ^2) mod 8 = 1 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6 by A1, A11, A13, NAT_D:24; :: thesis: verum
end;
case (c ^2) mod 8 = 4 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 by A2, A1, A11, A13; :: thesis: verum
end;
end;
end;
case A14: (b ^2) mod 8 = 4 ; :: thesis: verum
per cases ( (c ^2) mod 8 = 0 or (c ^2) mod 8 = 1 or (c ^2) mod 8 = 4 ) by NUMBER10:61;
case (c ^2) mod 8 = 0 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 by A1, A11, A14, NAT_D:25; :: thesis: verum
end;
case (c ^2) mod 8 = 1 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 by A2, A1, A11, A14; :: thesis: verum
end;
case (c ^2) mod 8 = 4 ; :: thesis: (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4
hence (((a ^2) + (b ^2)) + (c ^2)) mod 8 = ((1 * 8) + 4) mod 8 by A1, A11, A14
.= 4 mod 8 by NAT_D:21
.= 4 by NAT_D:24 ;
:: thesis: verum
end;
end;
end;
end;
end;
end;
end;
hence ( (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 0 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 1 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 2 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 3 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 4 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 5 or (((a ^2) + (b ^2)) + (c ^2)) mod 8 = 6 ) ; :: thesis: verum