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

end;

suppose A1:
a = 0
; :: thesis: ex b_{1} being Nat st

( b_{1} divides a & b_{1} divides b & ( for m being Integer st m divides a & m divides b holds

m divides b_{1} ) )

( b

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

suppose A4:
b = 0
; :: thesis: ex b_{1} being Nat st

( b_{1} divides a & b_{1} divides b & ( for m being Integer st m divides a & m divides b holds

m divides b_{1} ) )

( b

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

suppose A7:
( a <> 0 & b <> 0 )
; :: thesis: ex b_{1} being Nat st

( b_{1} divides a & b_{1} divides b & ( for m being Integer st m divides a & m divides b holds

m divides b_{1} ) )

( b

m divides b

defpred S_{1}[ 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_{1}[i] holds

i <= k

then A12: ex k being Nat st S_{1}[k]
;

consider k being Nat such that

A13: S_{1}[k]
and

A14: for n being Nat st S_{1}[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;

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

proof

( 1 divides a & 1 divides b )
by Lm5;
let i be Nat; :: thesis: ( S_{1}[i] implies i <= k )

assume S_{1}[i]
; :: thesis: i <= k

then i divides a * b by A8, Lm2;

then i divides k by A9, Lm3;

hence i <= k by A10, Lm9; :: thesis: verum

end;assume S

then i divides a * b by A8, Lm2;

then i divides k by A9, Lm3;

hence i <= k by A10, Lm9; :: thesis: verum

then A12: ex k being Nat st S

consider k being Nat such that

A13: S

A14: for n being Nat st S

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

then
0 < n lcm k
;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 ( n = 0 or k = 0 ) by Th4;

hence contradiction by A7, A13, A17, A15; :: thesis: verum

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