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

proof

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

end;

A4: (2 * p) + 1 > 5 - 3 by A2, XREAL_1:53;
then A5: not 2 is_quadratic_residue_mod (2 * p) + 1 by A3, INT_5:44, 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)) mod ((2 * p) + 1) = ((2 * p) + 1) - 1 by A4, A5, INT_5:19, B2;
then A6: (2 |^ ((2 * p) div 2)) mod ((2 * p) + 1) = ((2 * p) + 1) - 1 by NAT_D:34;
A7: (2 * p) + 1 > 5 - 4 by A2, XREAL_1:53;
then (2 * p) + 1 >= 1 + 1 by NAT_1:13;
then A8: ((2 * p) + 1) - 2 is Nat by NAT_1:21;
(Mersenne p) mod ((2 * p) + 1) = (((2 |^ p) mod ((2 * p) + 1)) - (1 mod ((2 * p) + 1))) mod ((2 * p) + 1) by INT_6:7
.= ((((2 * p) + 1) - 1) - (1 mod ((2 * p) + 1))) mod ((2 * p) + 1) by A6, NAT_D:18
.= ((((2 * p) + 1) - 1) - 1) mod ((2 * p) + 1) by PEPIN:5, A7
.= ((2 * p) + 1) - 2 by NAT_D:24, XREAL_1:46, A8 ;
hence ex q being Safe Prime st (Mersenne p) mod q = q - 2 by B2; :: thesis: verum