let t, u, z be Integer; :: thesis: ( t * u divides z * u iff |.u.| * (t gcd z) = |.u.| * |.t.| )
A1: ( t * u divides z * u iff (t * u) gcd (z * u) = |.(t * u).| ) by Th3;
(t * u) gcd (z * u) = |.u.| * (t gcd z) by INT_6:16;
hence ( t * u divides z * u iff |.u.| * (t gcd z) = |.u.| * |.t.| ) by A1, COMPLEX1:65; :: thesis: verum