let p be Safe Prime; :: thesis: ( p <> 7 implies p mod 3 = 2 )

set k = p mod 3;

consider q being Prime such that

A1: (2 * q) + 1 = p by Def1;

assume A2: p <> 7 ; :: thesis: p mod 3 = 2

then p mod 3 <= 0 + 2 by NAT_1:13;

then not not p mod 3 = 0 & ... & not p mod 3 = 2 ;

hence p mod 3 = 2 by A3; :: thesis: verum

set k = p mod 3;

consider q being Prime such that

A1: (2 * q) + 1 = p by Def1;

assume A2: p <> 7 ; :: thesis: p mod 3 = 2

A3: now :: thesis: ( not p mod 3 = 0 & not p mod 3 = 1 )

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

end;now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( p mod 3 = 0 or p mod 3 = 1 )
by A4;

end;

suppose A5:
p mod 3 = 1
; :: thesis: contradiction

2,3 are_coprime
by INT_2:28, INT_2:30, PEPIN:41;

then A6: 2 gcd 3 = 1 by INT_2:def 3;

3 divides ((2 * q) + 1) - 1 by A1, A5, PEPIN:8;

then 3 divides q by A6, WSIERP_1:29;

then 3 = q by INT_2:def 4;

hence contradiction by A2, A1; :: thesis: verum

end;then A6: 2 gcd 3 = 1 by INT_2:def 3;

3 divides ((2 * q) + 1) - 1 by A1, A5, PEPIN:8;

then 3 divides q by A6, WSIERP_1:29;

then 3 = q by INT_2:def 4;

hence contradiction by A2, A1; :: thesis: verum

then p mod 3 <= 0 + 2 by NAT_1:13;

then not not p mod 3 = 0 & ... & not p mod 3 = 2 ;

hence p mod 3 = 2 by A3; :: thesis: verum