let t, u, z be Integer; :: thesis: ( not 3 divides (u + t) + z or 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )
assume A1: 3 divides (u + t) + z ; :: thesis: ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )
then A2: ((u + t) + z) mod 3 = 0 by INT_1:62;
A3: (u + t) mod 3 = ((u mod 3) + (t mod 3)) mod 3 by NAT_D:66;

per cases ( u mod 3 = 0 or u mod 3 = 1 or u mod 3 = 2 ) by Lm3;

suppose u mod 3 = 0 ; :: thesis: ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )

then 3 divides u by INT_1:62;
then 3 divides u * (t * z) by INT_2:2;
hence ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) ) ; :: thesis: verum

end;

suppose B1: u mod 3 = 1 ; :: thesis: ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )

per cases ( t mod 3 = 0 or t mod 3 = 1 or t mod 3 = 2 ) by Lm3;

suppose t mod 3 = 0 ; :: thesis: ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )

then 3 divides t by INT_1:62;
then 3 divides t * (u * z) by INT_2:2;
hence ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) ) ; :: thesis: verum

end;

suppose C1: t mod 3 = 1 ; :: thesis: ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )

then (u + t) mod 3 = 3 - 1 by B1, A3, NAT_D:24;
then ((u + t) + 1) mod 3 = ((u + t) + z) mod 3 by A2, Th90;
then (u + t) + z,(u + t) + 1 are_congruent_mod 3 by NAT_D:64;
then z,1 are_congruent_mod 3 ;
then z mod 3 = 1 mod 3 by NAT_D:64
.= 1 by NAT_D:14 ;
hence ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) ) by C1, B1; :: thesis: verum

end;

suppose t mod 3 = 2 ; :: thesis: ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )

then (u + t) mod 3 = 0 by B1, A3, NAT_D:25;
then 3 divides u + t by INT_1:62;
then 3 divides z by A1, INT_2:1;
hence ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) ) by INT_2:2; :: thesis: verum

end;

end;

end;

suppose B1: u mod 3 = 2 ; :: thesis: ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )

per cases ( t mod 3 = 0 or t mod 3 = 1 or t mod 3 = 2 ) by Lm3;

suppose t mod 3 = 0 ; :: thesis: ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )

then 3 divides t by INT_1:62;
then 3 divides t * (u * z) by INT_2:2;
hence ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) ) ; :: thesis: verum

end;

suppose t mod 3 = 1 ; :: thesis: ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )

then (u + t) mod 3 = 0 by B1, A3, NAT_D:25;
then 3 divides u + t by INT_1:62;
then 3 divides z by A1, INT_2:1;
hence ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) ) by INT_2:2; :: thesis: verum

end;

suppose C1: t mod 3 = 2 ; :: thesis: ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) )

then C2: (u + t) mod 3 = (1 + 3) mod 3 by B1, A3
.= ((1 mod 3) + (3 mod 3)) mod 3 by NAT_D:66
.= (1 + (3 mod 3)) mod 3 by RADIX_2:2
.= (1 + 0) mod 3 by NAT_D:25
.= 1 by NAT_D:14 ;
((u + t) + 2) mod 3 = ((2 mod 3) + ((u + t) mod 3)) mod 3 by NAT_D:66
.= (2 + 1) mod 3 by NAT_D:24, C2
.= ((u + t) + z) mod 3 by A2, NAT_D:25 ;
then (u + t) + z,(u + t) + 2 are_congruent_mod 3 by NAT_D:64;
then z,2 are_congruent_mod 3 ;
then z mod 3 = 2 mod 3 by NAT_D:64
.= 2 by NAT_D:24 ;
hence ( 3 divides (u * t) * z or ( u mod 3 = t mod 3 & t mod 3 = z mod 3 ) ) by B1, C1; :: thesis: verum

end;

end;

end;

end;