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

proof

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

end;

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