let k, n, m be Nat; :: thesis: (n gcd m) lcm (n gcd k) divides n gcd (m lcm k)
set M = m lcm k;
set N = n gcd k;
set P = n gcd m;
set L = (n gcd m) lcm (n gcd k);
A1: n gcd k divides k by NAT_D:def 5;
k divides m lcm k by NAT_D:def 4;
then A2: n gcd k divides m lcm k by A1, NAT_D:4;
A3: n gcd m divides m by NAT_D:def 5;
m divides m lcm k by NAT_D:def 4;
then n gcd m divides m lcm k by A3, NAT_D:4;
then A4: (n gcd m) lcm (n gcd k) divides m lcm k by A2, NAT_D:def 4;
A5: n gcd m divides n by NAT_D:def 5;
n gcd k divides n by NAT_D:def 5;
then (n gcd m) lcm (n gcd k) divides n by A5, NAT_D:def 4;
hence (n gcd m) lcm (n gcd k) divides n gcd (m lcm k) by A4, NAT_D:def 5; :: thesis: verum