let a, b, c be Integer; :: thesis: ( (((a ^2) + (b ^2)) + (c ^2)) mod 4 = 0 implies ( a is even & b is even & c is even ) )
assume A1: (((a ^2) + (b ^2)) + (c ^2)) mod 4 = 0 ; :: thesis: ( a is even & b is even & c is even )
A2: (((a ^2) + (b ^2)) + (c ^2)) mod 4 = ((((a ^2) mod 4) + ((b ^2) mod 4)) + ((c ^2) mod 4)) mod 4 by NUMBER05:8;
assume ( not a is even or not b is even or not c is even ) ; :: thesis: contradiction

per cases then ( a is odd or b is odd or c is odd ) ;

suppose a is odd ; :: thesis: contradiction

then A3: (a ^2) mod 4 = 1 by PYTHTRIP:4;

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

suppose b is even ; :: thesis: contradiction

then A4: (b ^2) mod 4 = 0 by PYTHTRIP:3;

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

suppose c is odd ; :: thesis: contradiction

then (c ^2) mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1, A2, A3, A4, NAT_D:24; :: thesis: verum

end;

suppose c is even ; :: thesis: contradiction

then (c ^2) mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1, A2, A3, A4; :: thesis: verum

end;

end;

end;

suppose b is odd ; :: thesis: contradiction

then A5: (b ^2) mod 4 = 1 by PYTHTRIP:4;

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

suppose c is odd ; :: thesis: contradiction

then (c ^2) mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1, A2, A3, A5, NAT_D:24; :: thesis: verum

end;

suppose c is even ; :: thesis: contradiction

then (c ^2) mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1, A2, A3, A5, NAT_D:24; :: thesis: verum

end;

end;

end;

end;

end;

suppose b is odd ; :: thesis: contradiction

then A6: (b ^2) mod 4 = 1 by PYTHTRIP:4;

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

suppose a is even ; :: thesis: contradiction

then A7: (a ^2) mod 4 = 0 by PYTHTRIP:3;

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

suppose c is odd ; :: thesis: contradiction

then (c ^2) mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1, A2, A6, A7, NAT_D:24; :: thesis: verum

end;

suppose c is even ; :: thesis: contradiction

then (c ^2) mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1, A2, A6, A7; :: thesis: verum

end;

end;

end;

suppose a is odd ; :: thesis: contradiction

then A8: (a ^2) mod 4 = 1 by PYTHTRIP:4;

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

suppose c is odd ; :: thesis: contradiction

then (c ^2) mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1, A2, A6, A8, NAT_D:24; :: thesis: verum

end;

suppose c is even ; :: thesis: contradiction

then (c ^2) mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1, A2, A6, A8, NAT_D:24; :: thesis: verum

end;

end;

end;

end;

end;

suppose c is odd ; :: thesis: contradiction

then A9: (c ^2) mod 4 = 1 by PYTHTRIP:4;

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

suppose a is even ; :: thesis: contradiction

then A10: (a ^2) mod 4 = 0 by PYTHTRIP:3;

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

suppose b is odd ; :: thesis: contradiction

then (b ^2) mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1, A2, A9, A10, NAT_D:24; :: thesis: verum

end;

suppose b is even ; :: thesis: contradiction

then (b ^2) mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1, A2, A9, A10; :: thesis: verum

end;

end;

end;

suppose a is odd ; :: thesis: contradiction

then A11: (a ^2) mod 4 = 1 by PYTHTRIP:4;

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

suppose b is odd ; :: thesis: contradiction

then (b ^2) mod 4 = 1 by PYTHTRIP:4;
hence contradiction by A1, A2, A9, A11, NAT_D:24; :: thesis: verum

end;

suppose b is even ; :: thesis: contradiction

then (b ^2) mod 4 = 0 by PYTHTRIP:3;
hence contradiction by A1, A2, A9, A11, NAT_D:24; :: thesis: verum

end;

end;

end;

end;

end;

end;