let k, n, m be Nat; :: thesis: ( ( m divides n & m divides k ) iff m divides n gcd k )
( m divides n gcd k implies ( m divides n & m divides k ) )

proof

set M = n gcd k;
A1: n gcd k divides n by NAT_D:def 5;
A2: n gcd k divides k by NAT_D:def 5;
assume m divides n gcd k ; :: thesis: ( m divides n & m divides k )
hence ( m divides n & m divides k ) by A1, A2, NAT_D:4; :: thesis: verum

end;

hence ( ( m divides n & m divides k ) iff m divides n gcd k ) by NAT_D:def 5; :: thesis: verum