let a, b be Integer; :: thesis: ( ( a = 0 & b = 0 ) iff a gcd b = 0 )

0 divides 0 gcd 0 by Def2;

hence ( a = 0 & b = 0 implies a gcd b = 0 ) ; :: thesis: ( a gcd b = 0 implies ( a = 0 & b = 0 ) )

assume a gcd b = 0 ; :: thesis: ( a = 0 & b = 0 )

then ( 0 divides a & 0 divides b ) by Def2;

hence ( a = 0 & b = 0 ) ; :: thesis: verum

0 divides 0 gcd 0 by Def2;

hence ( a = 0 & b = 0 implies a gcd b = 0 ) ; :: thesis: ( a gcd b = 0 implies ( a = 0 & b = 0 ) )

assume a gcd b = 0 ; :: thesis: ( a = 0 & b = 0 )

then ( 0 divides a & 0 divides b ) by Def2;

hence ( a = 0 & b = 0 ) ; :: thesis: verum