suppose A1: ( a = 0 or b = 0 ) ; :: thesis:

take 0 ; :: thesis:
thus ( a divides 0 & b divides 0 ) by Lm5; :: thesis:
thus for m being Integer st a divides m & b divides m holds
0 divides m by A1; :: thesis:

end;

suppose A2: ( a <> 0 & b <> 0 ) ; :: thesis:

defpred S₁[ Nat] means ( a divides $1 & b divides $1 & $1 <> 0 );
a * b in INT by INT_1:def 2;
then consider k being Nat such that
A3: ( a * b = k or a * b = - k ) by INT_1:def 1;
b divides a * b ;
then A4: b divides k by A3, Lm3;
a divides a * b ;
then A5: a divides k by A3, Lm3;
k <> 0 by A2, A3, XCMPLX_1:6;
then A6: ex k being Nat st S₁[k] by A5, A4;
consider k being Nat such that
A7: S₁[k] and
A8: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A6);
take k ; :: thesis:
thus ( a divides k & b divides k ) by A7; :: thesis:
let m be Integer; :: thesis:
m in INT by INT_1:def 2;
then consider n being Nat such that
A9: ( m = n or m = - n ) by INT_1:def 1;
assume that
A10: a divides m and
A11: b divides m ; :: thesis:
b divides n by A9, A11, Lm3;
then A12: b divides n mod k by A7, Lm6;
A13: k > 0 by A7;
n mod k in NAT by INT_1:3, INT_1:57;
then reconsider i = n mod k as Nat ;
assume A14: not k divides m ; :: thesis:

A15: now :: thesis:

assume i = 0 ; :: thesis:
then n - ((n div k) * k) = 0 by A7, INT_1:def 10;
then k divides n ;
hence contradiction by A9, A14, Lm3; :: thesis:

end;

a divides n by A9, A10, Lm3;
then a divides n mod k by A7, Lm6;
hence contradiction by A8, A13, A12, A15, INT_1:58; :: thesis:

end;

end;