let a, b be Integer; :: thesis: ( ( a = 0 or b = 0 ) iff a lcm b = 0 )
A1: ( b = 0 implies a lcm b = 0 )
proof
assume b = 0 ; :: thesis: a lcm b = 0
then 0 divides a lcm b by Def1;
hence a lcm b = 0 ; :: thesis: verum
end;
A2: ( not a lcm b = 0 or a = 0 or b = 0 )
proof
A3: ( b divides b implies b divides b * a ) ;
assume A4: a lcm b = 0 ; :: thesis: ( a = 0 or b = 0 )
( a divides a implies a divides a * b ) ;
then 0 divides a * b by A4, A3, Def1;
then a * b = 0 ;
hence ( a = 0 or b = 0 ) by XCMPLX_1:6; :: thesis: verum
end;
( a = 0 implies a lcm b = 0 )
proof
assume a = 0 ; :: thesis: a lcm b = 0
then 0 divides a lcm b by Def1;
hence a lcm b = 0 ; :: thesis: verum
end;
hence ( ( a = 0 or b = 0 ) iff a lcm b = 0 ) by A1, A2; :: thesis: verum