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 that
A1: p > 2 and
A2: p mod 4 = 1 ; :: thesis: ex q being Safe Prime st (Mersenne p) mod q = q - 2
set q = (2 * p) + 1;
A3: (2 * p) + 1 is Safe Prime by Def1, Def2;
A4: (2 * p) + 1 > 5 by A1, Lm1;
then A5: (2 * p) + 1 > 5 - 3 by XREAL_1:51;
then 2,(2 * p) + 1 are_coprime by A3, INT_2:28, INT_2:30;
then A6: 2 gcd ((2 * p) + 1) = 1 by INT_2:def 3;
p = ((p div 4) * 4) + 1 by A2, INT_1:59;
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 ;
then not 2 is_quadratic_residue_mod (2 * p) + 1 by A3, A5, INT_5:44;
then (2 |^ ((((2 * p) + 1) -' 1) div 2)) mod ((2 * p) + 1) = ((2 * p) + 1) - 1 by A3, A5, A6, INT_5:19;
then A7: (2 |^ ((2 * p) div 2)) mod ((2 * p) + 1) = ((2 * p) + 1) - 1 by NAT_D:34;
A8: (2 * p) + 1 > 5 - 4 by A4, XREAL_1:51;
then (2 * p) + 1 >= 1 + 1 by NAT_1:13;
then A9: ((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 A7, NAT_D:18
.= ((((2 * p) + 1) - 1) - 1) mod ((2 * p) + 1) by A8, PEPIN:5
.= ((2 * p) + 1) - 2 by A9, NAT_D:24, XREAL_1:44 ;
hence ex q being Safe Prime st (Mersenne p) mod q = q - 2 by A3; :: thesis: verum