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

proof

assume a gcd b = 0 ; :: thesis: ( a = 0 & b = 0 )
then ( 0 divides a & 0 divides b ) by Def3;
hence ( a = 0 & b = 0 ) by Th3; :: thesis: verum

end;

( a = 0 & b = 0 implies a gcd b = 0 )

proof

assume ( a = 0 & b = 0 ) ; :: thesis: a gcd b = 0
then 0 divides a gcd b by Def3;
hence a gcd b = 0 by Th3; :: thesis: verum

end;

hence ( ( a = 0 & b = 0 ) iff a gcd b = 0 ) by A1; :: thesis: verum