let p be Prime; :: thesis: ( not p is prime or p = 2 or p mod 4 = 1 or p mod 4 = 3 )
assume that
A1: p is prime and
A2: ( p <> 2 & p mod 4 <> 1 & p mod 4 <> 3 ) ; :: thesis: contradiction
set D = p div 4;
not not p mod (3 + 1) = 0 & ... & not p mod (3 + 1) = 3 by NUMBER03:11;

per cases then ( p mod 4 = 0 or p mod 4 = 2 ) by A2;

suppose p mod 4 = 0 ; :: thesis: contradiction

then 4 divides p by PEPIN:6;
hence contradiction by A1, INT_2:29; :: thesis: verum

end;

suppose p mod 4 = 2 ; :: thesis: contradiction

then p = (4 * (p div 4)) + 2 by INT_1:59;
then p = 2 * ((2 * (p div 4)) + 1) ;
then 2 divides p ;
hence contradiction by A2, A1; :: thesis: verum

end;

end;