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