let p be Sophie_Germain Prime; :: thesis: ( p > 2 & p mod 4 = 3 implies ex q being Safe Prime st q divides Mersenne p )
assume A1: ( p > 2 & p mod 4 = 3 ) ; :: thesis: ex q being Safe Prime st q divides Mersenne p
set q = (2 * p) + 1;
A2: (2 * p) + 1 > 5 by A1, SGSP2;
B2: (2 * p) + 1 is Safe Prime by defSGP, defASP;
A3: ((2 * p) + 1) mod 8 = 7

proof

p = ((p div 4) * 4) + 3 by A1, INT_1:86;
then (2 * p) + 1 = ((p div 4) * 8) + 7 ;
then ((2 * p) + 1) mod 8 = 7 mod 8 by NAT_D:21
.= 7 by NAT_D:24 ;
hence ((2 * p) + 1) mod 8 = 7 ; :: thesis: verum

end;

A4: (2 * p) + 1 > 5 - 3 by A2, XREAL_1:53;
then A5: 2 is_quadratic_residue_mod (2 * p) + 1 by A3, INT_5:43, B2;
2,(2 * p) + 1 are_relative_prime by INT_2:44, INT_2:47, A4, B2;
then 2 gcd ((2 * p) + 1) = 1 by INT_2:def 4;
then ((2 |^ ((((2 * p) + 1) -' 1) div 2)) - 1) mod ((2 * p) + 1) = 0 by A4, A5, INT_5:20, B2;
then ((2 |^ ((2 * p) div 2)) - 1) mod ((2 * p) + 1) = 0 by NAT_D:34;
then ((2 |^ p) - 1) mod ((2 * p) + 1) = 0 by NAT_D:18;
then (2 * p) + 1 divides (2 |^ p) - 1 by INT_1:89;
hence ex q being Safe Prime st q divides Mersenne p by B2; :: thesis: verum