let p be Sophie_Germain Prime; :: thesis: ( not p > 2 or p mod 4 = 1 or p mod 4 = 3 )
set k = p mod 4;
assume A1: p > 2 ; :: thesis: ( p mod 4 = 1 or p mod 4 = 3 )
A2: now :: thesis: ( not p mod 4 = 0 & not p mod 4 = 2 )
assume A3: ( p mod 4 = 0 or p mod 4 = 2 ) ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( p mod 4 = 0 or p mod 4 = 2 ) by A3;
suppose p mod 4 = 2 ; :: thesis: contradiction
then p = ((p div 4) * 4) + 2 by INT_1:59
.= (((p div 4) * 2) + 1) * 2 ;
then 2 divides p by INT_1:def 3;
hence contradiction by A1, INT_2:def 4; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
p mod 4 < 3 + 1 by NAT_D:62;
then p mod 4 <= 0 + 3 by NAT_1:13;
then not not p mod 4 = 0 & ... & not p mod 4 = 3 ;
hence ( p mod 4 = 1 or p mod 4 = 3 ) by A2; :: thesis: verum