let IT be Nat; :: thesis: ( IT = k lcm n iff ( k divides IT & n divides IT & ( for m being Nat st k divides m & n divides m holds
IT divides m ) ) )
thus ( IT = k lcm n implies ( k divides IT & n divides IT & ( for m being Nat st k divides m & n divides m holds
IT divides m ) ) ) by INT_2:def 1; :: thesis: ( k divides IT & n divides IT & ( for m being Nat st k divides m & n divides m holds
IT divides m ) implies IT = k lcm n )
assume that
A1: k divides IT and
A2: n divides IT and
A3: for m being Nat st k divides m & n divides m holds
IT divides m ; :: thesis: IT = k lcm n
for m being Integer st k divides m & n divides m holds
IT divides m
proof
let m be Integer; :: thesis: ( k divides m & n divides m implies IT divides m )
m in INT by INT_1:def 2;
then consider i being Nat such that
A4: ( m = i or m = - i ) by INT_1:def 1;
assume that
A5: k divides m and
A6: n divides m ; :: thesis: IT divides m
A7: k divides i by A4, A5, INT_2:10;
n divides i by A4, A6, INT_2:10;
then IT divides i by A3, A7;
hence IT divides m by A4, INT_2:10; :: thesis: verum
end;
hence IT = k lcm n by A1, A2, INT_2:def 1; :: thesis: verum