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	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 3 ) ∧ ( 𝑄 = ( ( 2 · 𝑃 ) + 1 ) ∧ 𝑄 ∈ ℙ ) ) → 𝑄 ∥ ( ( 2 ↑ 𝑃 ) − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 3 ) ∧ ( 𝑄 = ( ( 2 · 𝑃 ) + 1 ) ∧ 𝑄 ∈ ℙ ) ) → 𝑃 ∈ ℙ )
2		simprr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 3 ) ∧ ( 𝑄 = ( ( 2 · 𝑃 ) + 1 ) ∧ 𝑄 ∈ ℙ ) ) → 𝑄 ∈ ℙ )
3		oveq1	⊢ ( 𝑄 = ( ( 2 · 𝑃 ) + 1 ) → ( 𝑄 mod 8 ) = ( ( ( 2 · 𝑃 ) + 1 ) mod 8 ) )
4	3	adantr	⊢ ( ( 𝑄 = ( ( 2 · 𝑃 ) + 1 ) ∧ 𝑄 ∈ ℙ ) → ( 𝑄 mod 8 ) = ( ( ( 2 · 𝑃 ) + 1 ) mod 8 ) )
5		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
6		mod42tp1mod8	⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑃 mod 4 ) = 3 ) → ( ( ( 2 · 𝑃 ) + 1 ) mod 8 ) = 7 )
7	5 6	sylan	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 3 ) → ( ( ( 2 · 𝑃 ) + 1 ) mod 8 ) = 7 )
8	4 7	sylan9eqr	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 3 ) ∧ ( 𝑄 = ( ( 2 · 𝑃 ) + 1 ) ∧ 𝑄 ∈ ℙ ) ) → ( 𝑄 mod 8 ) = 7 )
9		simprl	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 3 ) ∧ ( 𝑄 = ( ( 2 · 𝑃 ) + 1 ) ∧ 𝑄 ∈ ℙ ) ) → 𝑄 = ( ( 2 · 𝑃 ) + 1 ) )
10		sfprmdvdsmersenne	⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑄 ∈ ℙ ∧ ( 𝑄 mod 8 ) = 7 ∧ 𝑄 = ( ( 2 · 𝑃 ) + 1 ) ) ) → 𝑄 ∥ ( ( 2 ↑ 𝑃 ) − 1 ) )
11	1 2 8 9 10	syl13anc	⊢ ( ( ( 𝑃 ∈ ℙ ∧ ( 𝑃 mod 4 ) = 3 ) ∧ ( 𝑄 = ( ( 2 · 𝑃 ) + 1 ) ∧ 𝑄 ∈ ℙ ) ) → 𝑄 ∥ ( ( 2 ↑ 𝑃 ) − 1 ) )