Metamath Proof Explorer


Theorem sgprmdvdsmersenne

Description: If P is a Sophie Germain prime (i.e. Q = ( ( 2 x. P ) + 1 ) is also prime) with P == 3 (mod 4 ), then Q divides the P-th Mersenne number M_P. (Contributed by AV, 20-Aug-2021)

Ref Expression
Assertion sgprmdvdsmersenne P P mod 4 = 3 Q = 2 P + 1 Q Q 2 P 1

Proof

Step Hyp Ref Expression
1 simpll P P mod 4 = 3 Q = 2 P + 1 Q P
2 simprr P P mod 4 = 3 Q = 2 P + 1 Q Q
3 oveq1 Q = 2 P + 1 Q mod 8 = 2 P + 1 mod 8
4 3 adantr Q = 2 P + 1 Q Q mod 8 = 2 P + 1 mod 8
5 prmz P P
6 mod42tp1mod8 P P mod 4 = 3 2 P + 1 mod 8 = 7
7 5 6 sylan P P mod 4 = 3 2 P + 1 mod 8 = 7
8 4 7 sylan9eqr P P mod 4 = 3 Q = 2 P + 1 Q Q mod 8 = 7
9 simprl P P mod 4 = 3 Q = 2 P + 1 Q Q = 2 P + 1
10 sfprmdvdsmersenne P Q Q mod 8 = 7 Q = 2 P + 1 Q 2 P 1
11 1 2 8 9 10 syl13anc P P mod 4 = 3 Q = 2 P + 1 Q Q 2 P 1