let a, b be non zero Nat; :: thesis: ( not a,b are_coprime implies ex k being non zero Nat st
( k <> 1 & k divides a & k divides b ) )
assume Z1: not a,b are_coprime ; :: thesis: ex k being non zero Nat st
( k <> 1 & k divides a & k divides b )
set k = a gcd b;
( a gcd b divides a & a gcd b divides b ) by NAT_D:def 5;
hence ex k being non zero Nat st
( k <> 1 & k divides a & k divides b ) by Z1; :: thesis: verum