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;
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