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 \in ℙ \land P \mod 4 = 3) \land (Q = 2 P + 1 \land Q \in ℙ)) \to Q ∥ (2^{P} - 1)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((P \in ℙ \land P \mod 4 = 3) \land (Q = 2 P + 1 \land Q \in ℙ)) \to P \in ℙ$
2		simprr	$⊢ ((P \in ℙ \land P \mod 4 = 3) \land (Q = 2 P + 1 \land Q \in ℙ)) \to Q \in ℙ$
3		oveq1	$⊢ Q = 2 P + 1 \to Q \mod 8 = (2 P + 1) \mod 8$
4	3	adantr	$⊢ (Q = 2 P + 1 \land Q \in ℙ) \to Q \mod 8 = (2 P + 1) \mod 8$
5		prmz	$⊢ P \in ℙ \to P \in ℤ$
6		mod42tp1mod8	$⊢ (P \in ℤ \land P \mod 4 = 3) \to (2 P + 1) \mod 8 = 7$
7	5 6	sylan	$⊢ (P \in ℙ \land P \mod 4 = 3) \to (2 P + 1) \mod 8 = 7$
8	4 7	sylan9eqr	$⊢ ((P \in ℙ \land P \mod 4 = 3) \land (Q = 2 P + 1 \land Q \in ℙ)) \to Q \mod 8 = 7$
9		simprl	$⊢ ((P \in ℙ \land P \mod 4 = 3) \land (Q = 2 P + 1 \land Q \in ℙ)) \to Q = 2 P + 1$
10		sfprmdvdsmersenne	$⊢ (P \in ℙ \land (Q \in ℙ \land Q \mod 8 = 7 \land Q = 2 P + 1)) \to Q ∥ (2^{P} - 1)$
11	1 2 8 9 10	syl13anc	$⊢ ((P \in ℙ \land P \mod 4 = 3) \land (Q = 2 P + 1 \land Q \in ℙ)) \to Q ∥ (2^{P} - 1)$