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 that
A1: p > 2 and
A2: p mod 4 = 3 ; :: thesis: ex q being Safe Prime st q divides Mersenne p
set q = (2 * p) + 1;
A3: (2 * p) + 1 is Safe Prime by Def1, Def2;
(2 * p) + 1 > 5 by A1, Lm1;
then A4: (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 A5: 2 gcd ((2 * p) + 1) = 1 by INT_2:def 3;
p = ((p div 4) * 4) + 3 by A2, INT_1:59;
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 ;
then 2 is_quadratic_residue_mod (2 * p) + 1 by A3, A4, INT_5:43;
then ((2 |^ ((((2 * p) + 1) -' 1) div 2)) - 1) mod ((2 * p) + 1) = 0 by A3, A4, A5, INT_5:20;
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:62;
hence ex q being Safe Prime st q divides Mersenne p by A3; :: thesis: verum