let p be Sophie_Germain Prime; ( 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
; 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; verum