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

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

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

proof

A2:
( not a lcm b = 0 or a = 0 or b = 0 )
assume
b = 0
; :: thesis: a lcm b = 0

then 0 divides a lcm b by Def1;

hence a lcm b = 0 ; :: thesis: verum

end;then 0 divides a lcm b by Def1;

hence a lcm b = 0 ; :: thesis: verum

proof

( a = 0 implies a lcm b = 0 )
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;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

proof

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

then 0 divides a lcm b by Def1;

hence a lcm b = 0 ; :: thesis: verum

end;then 0 divides a lcm b by Def1;

hence a lcm b = 0 ; :: thesis: verum