let n, m be Nat; :: thesis: n gcd m divides n lcm m
set K = n gcd m;
set N = n lcm m;
A1: ( n gcd m divides n & n gcd m divides m & ( for i being Nat st i divides n & i divides m holds
i divides n gcd m ) ) by NAT_D:def 5;
( n divides n lcm m & m divides n lcm m & ( for r being Nat st n divides r & m divides r holds
n lcm m divides r ) ) by NAT_D:def 4;
hence n gcd m divides n lcm m by A1, NAT_D:4; :: thesis: verum