let n, m, l be Nat; :: thesis: ( m divides l implies m lcm (n gcd l) divides (m lcm n) gcd l )
set M = m lcm n;
set K = (m lcm n) gcd l;
set N = n gcd l;
A1: m divides m lcm n by NAT_D:def 4;
A2: n gcd l divides n by NAT_D:def 5;
A3: n gcd l divides l by NAT_D:def 5;
n divides m lcm n by NAT_D:def 4;
then n gcd l divides m lcm n by A2, NAT_D:4;
then A4: n gcd l divides (m lcm n) gcd l by A3, NAT_D:def 5;
assume m divides l ; :: thesis: m lcm (n gcd l) divides (m lcm n) gcd l
then m divides (m lcm n) gcd l by A1, NAT_D:def 5;
hence m lcm (n gcd l) divides (m lcm n) gcd l by A4, NAT_D:def 4; :: thesis: verum