let a, b be Integer; :: thesis: ( ( a = 0 or b = 0 ) iff a lcm b = 0 )
A1: ( a = 0 implies a lcm b = 0 )

proof

assume a = 0 ; :: thesis: a lcm b = 0
then 0 divides a lcm b by Def2;
hence a lcm b = 0 by Th3; :: thesis: verum

end;

A2: ( b = 0 implies a lcm b = 0 )

proof

assume b = 0 ; :: thesis: a lcm b = 0
then 0 divides a lcm b by Def2;
hence a lcm b = 0 by Th3; :: thesis: verum

end;

( not a lcm b = 0 or a = 0 or b = 0 )

proof

assume A3: a lcm b = 0 ; :: thesis: ( a = 0 or b = 0 )
A4: ( a divides a implies a divides a * b ) by Th2;
( b divides b implies b divides b * a ) by Th2;
then 0 divides a * b by A3, A4, Def2;
then a * b = 0 by Th3;
hence ( a = 0 or b = 0 ) by XCMPLX_1:6; :: thesis: verum

end;

hence ( ( a = 0 or b = 0 ) iff a lcm b = 0 ) by A1, A2; :: thesis: verum