let m be Nat; :: thesis: for i being Integer st 0 < m & m * i divides m & not i = 1 holds
i = - 1
let i be Integer; :: thesis: ( 0 < m & m * i divides m & not i = 1 implies i = - 1 )
assume that
A1: 0 < m and
A2: m * i divides m ; :: thesis: ( i = 1 or i = - 1 )
m divides m * i ;
then ( m = m * i or m = - (- (- (m * i))) ) by A2, INT_2:11;
hence ( i = 1 or i = - 1 ) by A1, XCMPLX_1:7, XCMPLX_1:181; :: thesis: verum