let a, b be Integer; :: thesis: ( a divides b iff a lcm b = |.b.| )
thus ( a divides b implies a lcm b = |.b.| ) :: thesis: ( a lcm b = |.b.| implies a divides b )
proof
assume a divides b ; :: thesis: a lcm b = |.b.|
then |.b.| = |.a.| lcm |.b.| by INT_2:16, NEWTON:44;
hence a lcm b = |.b.| by Def2; :: thesis: verum
end;
assume a lcm b = |.b.| ; :: thesis: a divides b
then |.a.| lcm |.b.| = |.b.| by Def2;
hence a divides b by NEWTON:44, INT_2:16; :: thesis: verum