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 )

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

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 )

p mod 4 < 3 + 1
by NAT_D:62;assume A3:
( p mod 4 = 0 or p mod 4 = 2 )
; :: thesis: contradiction

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( p mod 4 = 0 or p mod 4 = 2 )
by A3;

end;

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;.= (((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

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