let t, z be Integer; :: thesis: ( t divides z iff t gcd z = |.t.| )
( |.t.| in NAT & |.z.| in NAT ) by INT_1:3;
then consider k, l being Nat such that
A1: ( k = |.t.| & l = |.z.| ) ;
( k divides l iff k gcd l = k ) by NEWTON:49, INT_2:def 2;
hence ( t divides z iff t gcd z = |.t.| ) by A1, INT_2:34, INT_2:16; :: thesis: verum