let i, j be Nat; :: thesis: ( i divides j & j divides i implies i = j )

assume i divides j ; :: thesis: ( not j divides i or i = j )

then consider a being Integer such that

A1: j = i * a ;

assume j divides i ; :: thesis: i = j

then consider b being Integer such that

A2: i = j * b ;

( i <> 0 implies i = j )

assume i divides j ; :: thesis: ( not j divides i or i = j )

then consider a being Integer such that

A1: j = i * a ;

assume j divides i ; :: thesis: i = j

then consider b being Integer such that

A2: i = j * b ;

( i <> 0 implies i = j )

proof

hence
i = j
by A1; :: thesis: verum
A3:
i >= 0
;

assume A4: i <> 0 ; :: thesis: i = j

1 * i = i * (a * b) by A1, A2;

then a * b = 1 by A4, XCMPLX_1:5;

then ( i = j * 1 or i = j * (- 1) ) by A2, INT_1:9;

hence i = j by A4, A3; :: thesis: verum

end;assume A4: i <> 0 ; :: thesis: i = j

1 * i = i * (a * b) by A1, A2;

then a * b = 1 by A4, XCMPLX_1:5;

then ( i = j * 1 or i = j * (- 1) ) by A2, INT_1:9;

hence i = j by A4, A3; :: thesis: verum