let i be Integer; :: thesis: ( i <> 1 & i <> - 1 implies for m being Multiple of i holds
( not m is prime or m = i or m = - i ) )
assume that
A1: i <> 1 and
A2: i <> - 1 ; :: thesis: for m being Multiple of i holds
( not m is prime or m = i or m = - i )
let m be Multiple of i; :: thesis: ( not m is prime or m = i or m = - i )
assume A3: m is prime ; :: thesis: ( m = i or m = - i )

per cases ( i >= 0 or i < 0 ) ;

suppose i >= 0 ; :: thesis: ( m = i or m = - i )

then i in NAT by INT_1:3;
hence ( m = i or m = - i ) by A1, A3, Def15; :: thesis: verum

end;

suppose i < 0 ; :: thesis: ( m = i or m = - i )

then A4: - i in NAT by INT_1:3;
- i divides m by Def15, INT_2:10;
then ( - i = 1 or - i = m ) by A3, A4;
hence ( m = i or m = - i ) by A2; :: thesis: verum

end;

end;