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

end;

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

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

b_{1} divides m ) )

( a divides b

b

take
0
; :: thesis: ( a divides 0 & b divides 0 & ( for m being Integer st a divides m & b divides m holds

0 divides m ) )

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

0 divides m

thus for m being Integer st a divides m & b divides m holds

0 divides m by A1; :: thesis: verum

end;0 divides m ) )

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

0 divides m

thus for m being Integer st a divides m & b divides m holds

0 divides m by A1; :: thesis: verum

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

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

b_{1} divides m ) )

( a divides b

b

defpred S_{1}[ 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_{1}[k]
by A5, A4;

consider k being Nat such that

A7: S_{1}[k]
and

A8: for n being Nat st S_{1}[n] holds

k <= n from NAT_1:sch 5(A6);

take k ; :: thesis: ( a divides k & b divides k & ( for m being Integer st a divides m & b divides m holds

k divides m ) )

thus ( a divides k & b divides k ) by A7; :: thesis: for m being Integer st a divides m & b divides m holds

k divides m

let m be Integer; :: thesis: ( a divides m & b divides m implies k divides m )

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: k divides m

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: contradiction

then a divides n mod k by A7, Lm6;

then k divides n by A8, A13, A12, A15, INT_1:58;

hence contradiction by A9, A14, Lm3; :: thesis: verum

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

consider k being Nat such that

A7: S

A8: for n being Nat st S

k <= n from NAT_1:sch 5(A6);

take k ; :: thesis: ( a divides k & b divides k & ( for m being Integer st a divides m & b divides m holds

k divides m ) )

thus ( a divides k & b divides k ) by A7; :: thesis: for m being Integer st a divides m & b divides m holds

k divides m

let m be Integer; :: thesis: ( a divides m & b divides m implies k divides m )

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: k divides m

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: contradiction

A15: now :: thesis: not i = 0

a divides n
by A9, A10, Lm3;assume
i = 0
; :: thesis: contradiction

then n - ((n div k) * k) = 0 by A7, INT_1:def 10;

then k divides n ;

hence contradiction by A9, A14, Lm3; :: thesis: verum

end;then n - ((n div k) * k) = 0 by A7, INT_1:def 10;

then k divides n ;

hence contradiction by A9, A14, Lm3; :: thesis: verum

then a divides n mod k by A7, Lm6;

then k divides n by A8, A13, A12, A15, INT_1:58;

hence contradiction by A9, A14, Lm3; :: thesis: verum