let t, u, z be Integer; :: thesis: ((t + u) + z) |^ 3,((t |^ 3) + (u |^ 3)) + (z |^ 3) are_congruent_mod 3
((t + u) + z) |^ 3 = ((((((t |^ 3) + (u |^ 3)) + (z |^ 3)) + (((3 * (t |^ 2)) * u) + ((3 * (t |^ 2)) * z))) + (((3 * (u |^ 2)) * t) + ((3 * (u |^ 2)) * z))) + (((3 * (z |^ 2)) * t) + ((3 * (z |^ 2)) * u))) + (((6 * t) * u) * z) by SERIES_4:8;
then (((t + u) + z) |^ 3) - (((t |^ 3) + (u |^ 3)) + (z |^ 3)) = 3 * ((((((t |^ 2) * u) + ((t |^ 2) * z)) + (((u |^ 2) * t) + ((u |^ 2) * z))) + (((z |^ 2) * t) + ((z |^ 2) * u))) + (((2 * t) * u) * z)) ;
hence ((t + u) + z) |^ 3,((t |^ 3) + (u |^ 3)) + (z |^ 3) are_congruent_mod 3 ; :: thesis: verum