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

( |.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