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 e. Prime /\ ( P mod 4 ) = 3 ) /\ ( Q = ( ( 2 x. P ) + 1 ) /\ Q e. Prime ) ) -> Q || ( ( 2 ^ P ) - 1 ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 3 ) /\ ( Q = ( ( 2 x. P ) + 1 ) /\ Q e. Prime ) ) -> P e. Prime )
2 simprr 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 3 ) /\ ( Q = ( ( 2 x. P ) + 1 ) /\ Q e. Prime ) ) -> Q e. Prime )
3 oveq1 
 |-  ( Q = ( ( 2 x. P ) + 1 ) -> ( Q mod 8 ) = ( ( ( 2 x. P ) + 1 ) mod 8 ) )
4 3 adantr 
 |-  ( ( Q = ( ( 2 x. P ) + 1 ) /\ Q e. Prime ) -> ( Q mod 8 ) = ( ( ( 2 x. P ) + 1 ) mod 8 ) )
5 prmz 
 |-  ( P e. Prime -> P e. ZZ )
6 mod42tp1mod8 
 |-  ( ( P e. ZZ /\ ( P mod 4 ) = 3 ) -> ( ( ( 2 x. P ) + 1 ) mod 8 ) = 7 )
7 5 6 sylan 
 |-  ( ( P e. Prime /\ ( P mod 4 ) = 3 ) -> ( ( ( 2 x. P ) + 1 ) mod 8 ) = 7 )
8 4 7 sylan9eqr 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 3 ) /\ ( Q = ( ( 2 x. P ) + 1 ) /\ Q e. Prime ) ) -> ( Q mod 8 ) = 7 )
9 simprl 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 3 ) /\ ( Q = ( ( 2 x. P ) + 1 ) /\ Q e. Prime ) ) -> Q = ( ( 2 x. P ) + 1 ) )
10 sfprmdvdsmersenne 
 |-  ( ( P e. Prime /\ ( Q e. Prime /\ ( Q mod 8 ) = 7 /\ Q = ( ( 2 x. P ) + 1 ) ) ) -> Q || ( ( 2 ^ P ) - 1 ) )
11 1 2 8 9 10 syl13anc 
 |-  ( ( ( P e. Prime /\ ( P mod 4 ) = 3 ) /\ ( Q = ( ( 2 x. P ) + 1 ) /\ Q e. Prime ) ) -> Q || ( ( 2 ^ P ) - 1 ) )