per cases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;

suppose A1: a = 0 ; :: thesis: ex b₁ being Nat st
( b₁ divides a & b₁ divides b & ( for m being Integer st m divides a & m divides b holds
m divides b₁ ) )

b in INT by INT_1:def 2;
then consider k being Nat such that
A2: ( b = k or b = - k ) by INT_1:def 1;
take k ; :: thesis: ( k divides a & k divides b & ( for m being Integer st m divides a & m divides b holds
m divides k ) )
thus ( k divides a & k divides b ) by A1, A2, Lm4, Lm5; :: thesis: for m being Integer st m divides a & m divides b holds
m divides k
let m be Integer; :: thesis: ( m divides a & m divides b implies m divides k )
assume that
m divides a and
A3: m divides b ; :: thesis: m divides k
thus m divides k by A2, A3, Lm3; :: thesis: verum

end;

suppose A4: b = 0 ; :: thesis: ex b₁ being Nat st
( b₁ divides a & b₁ divides b & ( for m being Integer st m divides a & m divides b holds
m divides b₁ ) )

a in INT by INT_1:def 2;
then consider k being Nat such that
A5: ( a = k or a = - k ) by INT_1:def 1;
take k ; :: thesis: ( k divides a & k divides b & ( for m being Integer st m divides a & m divides b holds
m divides k ) )
thus ( k divides a & k divides b ) by A4, A5, Lm4, Lm5; :: thesis: for m being Integer st m divides a & m divides b holds
m divides k
let m be Integer; :: thesis: ( m divides a & m divides b implies m divides k )
assume that
A6: m divides a and
m divides b ; :: thesis: m divides k
thus m divides k by A5, A6, Lm3; :: thesis: verum

end;

suppose A7: ( a <> 0 & b <> 0 ) ; :: thesis: ex b₁ being Nat st
( b₁ divides a & b₁ divides b & ( for m being Integer st m divides a & m divides b holds
m divides b₁ ) )

defpred S₁[ Nat] means ( $1 divides a & $1 divides b & $1 <> 0 );
A8: a divides a * b ;
a * b in INT by INT_1:def 2;
then consider k being Nat such that
A9: ( a * b = k or a * b = - k ) by INT_1:def 1;
k <> 0 by A7, A9, XCMPLX_1:6;
then A10: k > 0 ;
A11: for i being Nat st S₁[i] holds
i <= k

proof

let i be Nat; :: thesis: ( S₁[i] implies i <= k )
assume S₁[i] ; :: thesis: i <= k
then i divides a * b by A8, Lm2;
hence i <= k by A9, Lm3, A10, Lm9; :: thesis: verum

end;

( 1 divides a & 1 divides b ) by Lm5;
then A12: ex k being Nat st S₁[k] ;
consider k being Nat such that
A13: S₁[k] and
A14: for n being Nat st S₁[n] holds
n <= k from NAT_1:sch 6(A11, A12);
take k ; :: thesis: ( k divides a & k divides b & ( for m being Integer st m divides a & m divides b holds
m divides k ) )
thus ( k divides a & k divides b ) by A13; :: thesis: for m being Integer st m divides a & m divides b holds
m divides k
let m be Integer; :: thesis: ( m divides a & m divides b implies m divides k )
assume that
A15: m divides a and
A16: m divides b ; :: thesis: m divides k
m in INT by INT_1:def 2;
then consider n being Nat such that
A17: ( m = n or m = - n ) by INT_1:def 1;
set i = n lcm k;
A18: k divides n lcm k by Def1;

now :: thesis: not n lcm k = 0

assume n lcm k = 0 ; :: thesis: contradiction
then ( n = 0 or k = 0 ) by Th4;
hence contradiction by A7, A13, A17, A15; :: thesis: verum

end;

then 0 < n lcm k ;
then A19: k <= n lcm k by A18, Lm9;
n divides b by A17, A16, Lm4;
then A20: n lcm k divides b by A13, Def1;
n divides a by A17, A15, Lm4;
then n lcm k divides a by A13, Def1;
then k >= n lcm k by A14, A20;
then k = n lcm k by A19, XXREAL_0:1;
then A21: n divides k by Def1;
assume not m divides k ; :: thesis: contradiction
hence contradiction by A17, A21, Lm4; :: thesis: verum

end;

end;