let i be Integer; :: thesis: for p being Prime holds
( not i divides p or i = 1 or i = - 1 or i = p or i = - p )
let p be Prime; :: thesis: ( not i divides p or i = 1 or i = - 1 or i = p or i = - p )
assume A1: i divides p ; :: thesis: ( i = 1 or i = - 1 or i = p or i = - p )

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

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

then i in NAT by INT_1:3;
hence ( i = 1 or i = - 1 or i = p or i = - p ) by A1, INT_2:def 4; :: thesis: verum

end;

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

then - i in NAT by INT_1:3;
then ( - i = 1 or - i = p ) by A1, INT_2:10, INT_2:def 4;
hence ( i = 1 or i = - 1 or i = p or i = - p ) ; :: thesis: verum

end;

end;