sfprmdvdsmersenne

Description: If Q is a safe prime (i.e. Q = ( ( 2 x. P ) + 1 ) for a prime P ) with Q == 7 (mod 8 ), then Q divides the P-th Mersenne number M_P. (Contributed by AV, 20-Aug-2021)

		Ref	Expression
	Assertion	sfprmdvdsmersenne	$⊢ (P \in ℙ \land (Q \in ℙ \land Q \mod 8 = 7 \land Q = 2 P + 1)) \to Q ∥ (2^{P} - 1)$

Proof

Step	Hyp	Ref	Expression
1		olc	$⊢ Q \mod 8 = 7 \to (Q \mod 8 = 1 \lor Q \mod 8 = 7)$
2		ovex	$⊢ Q \mod 8 \in V$
3		elprg	$⊢ Q \mod 8 \in V \to (Q \mod 8 \in \{1, 7\} \leftrightarrow (Q \mod 8 = 1 \lor Q \mod 8 = 7))$
4	2 3	mp1i	$⊢ Q \mod 8 = 7 \to (Q \mod 8 \in \{1, 7\} \leftrightarrow (Q \mod 8 = 1 \lor Q \mod 8 = 7))$
5	1 4	mpbird	$⊢ Q \mod 8 = 7 \to Q \mod 8 \in \{1, 7\}$
6		2lgs	$⊢ Q \in ℙ \to (2 /_{L} Q = 1 \leftrightarrow Q \mod 8 \in \{1, 7\})$
7	6	ad2antlr	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (2 /_{L} Q = 1 \leftrightarrow Q \mod 8 \in \{1, 7\})$
8		2z	$⊢ 2 \in ℤ$
9		simpr	$⊢ (P \in ℙ \land Q \in ℙ) \to Q \in ℙ$
10	9	adantr	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to Q \in ℙ$
11		2re	$⊢ 2 \in ℝ$
12	11	a1i	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to 2 \in ℝ$
13		2m1e1	$⊢ 2 - 1 = 1$
14	11	a1i	$⊢ P \in ℙ \to 2 \in ℝ$
15		prmnn	$⊢ P \in ℙ \to P \in ℕ$
16	15	nnred	$⊢ P \in ℙ \to P \in ℝ$
17		1lt2	$⊢ 1 < 2$
18	17	a1i	$⊢ P \in ℙ \to 1 < 2$
19		prmgt1	$⊢ P \in ℙ \to 1 < P$
20	14 16 18 19	mulgt1d	$⊢ P \in ℙ \to 1 < 2 P$
21	13 20	eqbrtrid	$⊢ P \in ℙ \to 2 - 1 < 2 P$
22		1red	$⊢ P \in ℙ \to 1 \in ℝ$
23		2nn	$⊢ 2 \in ℕ$
24	23	a1i	$⊢ P \in ℙ \to 2 \in ℕ$
25	24 15	nnmulcld	$⊢ P \in ℙ \to 2 P \in ℕ$
26	25	nnred	$⊢ P \in ℙ \to 2 P \in ℝ$
27	14 22 26	ltsubaddd	$⊢ P \in ℙ \to (2 - 1 < 2 P \leftrightarrow 2 < 2 P + 1)$
28	21 27	mpbid	$⊢ P \in ℙ \to 2 < 2 P + 1$
29	28	ad2antrr	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to 2 < 2 P + 1$
30		breq2	$⊢ Q = 2 P + 1 \to (2 < Q \leftrightarrow 2 < 2 P + 1)$
31	30	adantl	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (2 < Q \leftrightarrow 2 < 2 P + 1)$
32	29 31	mpbird	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to 2 < Q$
33	12 32	gtned	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to Q \neq 2$
34		eldifsn	$⊢ Q \in (ℙ ∖ \{2\}) \leftrightarrow (Q \in ℙ \land Q \neq 2)$
35	10 33 34	sylanbrc	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to Q \in (ℙ ∖ \{2\})$
36		lgsqrmodndvds	$⊢ (2 \in ℤ \land Q \in (ℙ ∖ \{2\})) \to (2 /_{L} Q = 1 \to \exists m \in ℤ (m^{2} \mod Q = 2 \mod Q \land \neg Q ∥ m))$
37	8 35 36	sylancr	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (2 /_{L} Q = 1 \to \exists m \in ℤ (m^{2} \mod Q = 2 \mod Q \land \neg Q ∥ m))$
38		prmnn	$⊢ Q \in ℙ \to Q \in ℕ$
39	38	nncnd	$⊢ Q \in ℙ \to Q \in ℂ$
40	39	adantl	$⊢ (P \in ℙ \land Q \in ℙ) \to Q \in ℂ$
41		1cnd	$⊢ (P \in ℙ \land Q \in ℙ) \to 1 \in ℂ$
42		2cnd	$⊢ P \in ℙ \to 2 \in ℂ$
43	15	nncnd	$⊢ P \in ℙ \to P \in ℂ$
44	42 43	mulcld	$⊢ P \in ℙ \to 2 P \in ℂ$
45	44	adantr	$⊢ (P \in ℙ \land Q \in ℙ) \to 2 P \in ℂ$
46	40 41 45	subadd2d	$⊢ (P \in ℙ \land Q \in ℙ) \to (Q - 1 = 2 P \leftrightarrow 2 P + 1 = Q)$
47		prmz	$⊢ Q \in ℙ \to Q \in ℤ$
48		peano2zm	$⊢ Q \in ℤ \to Q - 1 \in ℤ$
49	47 48	syl	$⊢ Q \in ℙ \to Q - 1 \in ℤ$
50	49	zcnd	$⊢ Q \in ℙ \to Q - 1 \in ℂ$
51	50	adantl	$⊢ (P \in ℙ \land Q \in ℙ) \to Q - 1 \in ℂ$
52	43	adantr	$⊢ (P \in ℙ \land Q \in ℙ) \to P \in ℂ$
53		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
54	53	a1i	$⊢ (P \in ℙ \land Q \in ℙ) \to (2 \in ℂ \land 2 \neq 0)$
55		divmul2	$⊢ (Q - 1 \in ℂ \land P \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to (\frac{Q - 1}{2} = P \leftrightarrow Q - 1 = 2 P)$
56	51 52 54 55	syl3anc	$⊢ (P \in ℙ \land Q \in ℙ) \to (\frac{Q - 1}{2} = P \leftrightarrow Q - 1 = 2 P)$
57		eqcom	$⊢ Q = 2 P + 1 \leftrightarrow 2 P + 1 = Q$
58	57	a1i	$⊢ (P \in ℙ \land Q \in ℙ) \to (Q = 2 P + 1 \leftrightarrow 2 P + 1 = Q)$
59	46 56 58	3bitr4rd	$⊢ (P \in ℙ \land Q \in ℙ) \to (Q = 2 P + 1 \leftrightarrow \frac{Q - 1}{2} = P)$
60	59	biimpa	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to \frac{Q - 1}{2} = P$
61		oveq2	$⊢ \frac{Q - 1}{2} = P \to 2^{\frac{Q - 1}{2}} = 2^{P}$
62		zsqcl	$⊢ m \in ℤ \to m^{2} \in ℤ$
63	62	ad2antlr	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land m^{2} \mod Q = 2 \mod Q) \to m^{2} \in ℤ$
64	8	a1i	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land m^{2} \mod Q = 2 \mod Q) \to 2 \in ℤ$
65		oveq1	$⊢ Q = 2 P + 1 \to Q - 1 = 2 P + 1 - 1$
66	65	adantl	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to Q - 1 = 2 P + 1 - 1$
67	66	oveq1d	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to \frac{Q - 1}{2} = \frac{2 P + 1 - 1}{2}$
68		pncan1	$⊢ 2 P \in ℂ \to 2 P + 1 - 1 = 2 P$
69	44 68	syl	$⊢ P \in ℙ \to 2 P + 1 - 1 = 2 P$
70	69	oveq1d	$⊢ P \in ℙ \to \frac{2 P + 1 - 1}{2} = \frac{2 P}{2}$
71		2ne0	$⊢ 2 \neq 0$
72	71	a1i	$⊢ P \in ℙ \to 2 \neq 0$
73	43 42 72	divcan3d	$⊢ P \in ℙ \to \frac{2 P}{2} = P$
74	70 73	eqtrd	$⊢ P \in ℙ \to \frac{2 P + 1 - 1}{2} = P$
75	74	ad2antrr	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to \frac{2 P + 1 - 1}{2} = P$
76	67 75	eqtrd	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to \frac{Q - 1}{2} = P$
77	15	nnnn0d	$⊢ P \in ℙ \to P \in ℕ_{0}$
78	77	ad2antrr	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to P \in ℕ_{0}$
79	76 78	eqeltrd	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to \frac{Q - 1}{2} \in ℕ_{0}$
80	38	nnrpd	$⊢ Q \in ℙ \to Q \in ℝ^{+}$
81	80	ad2antlr	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to Q \in ℝ^{+}$
82	79 81	jca	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (\frac{Q - 1}{2} \in ℕ_{0} \land Q \in ℝ^{+})$
83	82	ad2antrr	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land m^{2} \mod Q = 2 \mod Q) \to (\frac{Q - 1}{2} \in ℕ_{0} \land Q \in ℝ^{+})$
84		simpr	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land m^{2} \mod Q = 2 \mod Q) \to m^{2} \mod Q = 2 \mod Q$
85		modexp	$⊢ ((m^{2} \in ℤ \land 2 \in ℤ) \land (\frac{Q - 1}{2} \in ℕ_{0} \land Q \in ℝ^{+}) \land m^{2} \mod Q = 2 \mod Q) \to {(m^{2})}^{\frac{Q - 1}{2}} \mod Q = 2^{\frac{Q - 1}{2}} \mod Q$
86	63 64 83 84 85	syl211anc	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land m^{2} \mod Q = 2 \mod Q) \to {(m^{2})}^{\frac{Q - 1}{2}} \mod Q = 2^{\frac{Q - 1}{2}} \mod Q$
87	86	ex	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to (m^{2} \mod Q = 2 \mod Q \to {(m^{2})}^{\frac{Q - 1}{2}} \mod Q = 2^{\frac{Q - 1}{2}} \mod Q)$
88	87	adantr	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land \neg Q ∥ m) \to (m^{2} \mod Q = 2 \mod Q \to {(m^{2})}^{\frac{Q - 1}{2}} \mod Q = 2^{\frac{Q - 1}{2}} \mod Q)$
89		2cnd	$⊢ Q \in ℙ \to 2 \in ℂ$
90	71	a1i	$⊢ Q \in ℙ \to 2 \neq 0$
91	50 89 90	divcan2d	$⊢ Q \in ℙ \to 2 (\frac{Q - 1}{2}) = Q - 1$
92	91	eqcomd	$⊢ Q \in ℙ \to Q - 1 = 2 (\frac{Q - 1}{2})$
93	92	oveq2d	$⊢ Q \in ℙ \to m^{Q - 1} = m^{2 (\frac{Q - 1}{2})}$
94	93	ad3antlr	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to m^{Q - 1} = m^{2 (\frac{Q - 1}{2})}$
95		zcn	$⊢ m \in ℤ \to m \in ℂ$
96	95	adantl	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to m \in ℂ$
97	79	adantr	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to \frac{Q - 1}{2} \in ℕ_{0}$
98		2nn0	$⊢ 2 \in ℕ_{0}$
99	98	a1i	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to 2 \in ℕ_{0}$
100	96 97 99	expmuld	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to m^{2 (\frac{Q - 1}{2})} = {(m^{2})}^{\frac{Q - 1}{2}}$
101	94 100	eqtr2d	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to {(m^{2})}^{\frac{Q - 1}{2}} = m^{Q - 1}$
102	101	oveq1d	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to {(m^{2})}^{\frac{Q - 1}{2}} \mod Q = m^{Q - 1} \mod Q$
103	102	adantr	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land \neg Q ∥ m) \to {(m^{2})}^{\frac{Q - 1}{2}} \mod Q = m^{Q - 1} \mod Q$
104		vfermltl	$⊢ (Q \in ℙ \land m \in ℤ \land \neg Q ∥ m) \to m^{Q - 1} \mod Q = 1$
105	104	ad5ant245	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land \neg Q ∥ m) \to m^{Q - 1} \mod Q = 1$
106	103 105	eqtrd	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land \neg Q ∥ m) \to {(m^{2})}^{\frac{Q - 1}{2}} \mod Q = 1$
107		oveq1	$⊢ 2^{\frac{Q - 1}{2}} = 2^{P} \to 2^{\frac{Q - 1}{2}} \mod Q = 2^{P} \mod Q$
108	106 107	eqeqan12d	$⊢ (((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land \neg Q ∥ m) \land 2^{\frac{Q - 1}{2}} = 2^{P}) \to ({(m^{2})}^{\frac{Q - 1}{2}} \mod Q = 2^{\frac{Q - 1}{2}} \mod Q \leftrightarrow 1 = 2^{P} \mod Q)$
109		id	$⊢ 1 = 2^{P} \mod Q \to 1 = 2^{P} \mod Q$
110	109	eqcomd	$⊢ 1 = 2^{P} \mod Q \to 2^{P} \mod Q = 1$
111	38	nnred	$⊢ Q \in ℙ \to Q \in ℝ$
112		prmgt1	$⊢ Q \in ℙ \to 1 < Q$
113		1mod	$⊢ (Q \in ℝ \land 1 < Q) \to 1 \mod Q = 1$
114	111 112 113	syl2anc	$⊢ Q \in ℙ \to 1 \mod Q = 1$
115	114	eqcomd	$⊢ Q \in ℙ \to 1 = 1 \mod Q$
116	115	ad3antlr	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to 1 = 1 \mod Q$
117	110 116	sylan9eqr	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land 1 = 2^{P} \mod Q) \to 2^{P} \mod Q = 1 \mod Q$
118	38	ad4antlr	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land 1 = 2^{P} \mod Q) \to Q \in ℕ$
119		zexpcl	$⊢ (2 \in ℤ \land P \in ℕ_{0}) \to 2^{P} \in ℤ$
120	8 77 119	sylancr	$⊢ P \in ℙ \to 2^{P} \in ℤ$
121	120	ad4antr	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land 1 = 2^{P} \mod Q) \to 2^{P} \in ℤ$
122		1zzd	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land 1 = 2^{P} \mod Q) \to 1 \in ℤ$
123		moddvds	$⊢ (Q \in ℕ \land 2^{P} \in ℤ \land 1 \in ℤ) \to (2^{P} \mod Q = 1 \mod Q \leftrightarrow Q ∥ (2^{P} - 1))$
124	118 121 122 123	syl3anc	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land 1 = 2^{P} \mod Q) \to (2^{P} \mod Q = 1 \mod Q \leftrightarrow Q ∥ (2^{P} - 1))$
125	117 124	mpbid	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land 1 = 2^{P} \mod Q) \to Q ∥ (2^{P} - 1)$
126	125	ex	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to (1 = 2^{P} \mod Q \to Q ∥ (2^{P} - 1))$
127	126	ad2antrr	$⊢ (((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land \neg Q ∥ m) \land 2^{\frac{Q - 1}{2}} = 2^{P}) \to (1 = 2^{P} \mod Q \to Q ∥ (2^{P} - 1))$
128	108 127	sylbid	$⊢ (((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land \neg Q ∥ m) \land 2^{\frac{Q - 1}{2}} = 2^{P}) \to ({(m^{2})}^{\frac{Q - 1}{2}} \mod Q = 2^{\frac{Q - 1}{2}} \mod Q \to Q ∥ (2^{P} - 1))$
129	128	ex	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land \neg Q ∥ m) \to (2^{\frac{Q - 1}{2}} = 2^{P} \to ({(m^{2})}^{\frac{Q - 1}{2}} \mod Q = 2^{\frac{Q - 1}{2}} \mod Q \to Q ∥ (2^{P} - 1)))$
130	129	com23	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land \neg Q ∥ m) \to ({(m^{2})}^{\frac{Q - 1}{2}} \mod Q = 2^{\frac{Q - 1}{2}} \mod Q \to (2^{\frac{Q - 1}{2}} = 2^{P} \to Q ∥ (2^{P} - 1)))$
131	88 130	syld	$⊢ ((((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \land \neg Q ∥ m) \to (m^{2} \mod Q = 2 \mod Q \to (2^{\frac{Q - 1}{2}} = 2^{P} \to Q ∥ (2^{P} - 1)))$
132	131	ex	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to (\neg Q ∥ m \to (m^{2} \mod Q = 2 \mod Q \to (2^{\frac{Q - 1}{2}} = 2^{P} \to Q ∥ (2^{P} - 1))))$
133	132	com23	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to (m^{2} \mod Q = 2 \mod Q \to (\neg Q ∥ m \to (2^{\frac{Q - 1}{2}} = 2^{P} \to Q ∥ (2^{P} - 1))))$
134	133	impd	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to ((m^{2} \mod Q = 2 \mod Q \land \neg Q ∥ m) \to (2^{\frac{Q - 1}{2}} = 2^{P} \to Q ∥ (2^{P} - 1)))$
135	134	com23	$⊢ (((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \land m \in ℤ) \to (2^{\frac{Q - 1}{2}} = 2^{P} \to ((m^{2} \mod Q = 2 \mod Q \land \neg Q ∥ m) \to Q ∥ (2^{P} - 1)))$
136	135	ex	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (m \in ℤ \to (2^{\frac{Q - 1}{2}} = 2^{P} \to ((m^{2} \mod Q = 2 \mod Q \land \neg Q ∥ m) \to Q ∥ (2^{P} - 1))))$
137	136	com23	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (2^{\frac{Q - 1}{2}} = 2^{P} \to (m \in ℤ \to ((m^{2} \mod Q = 2 \mod Q \land \neg Q ∥ m) \to Q ∥ (2^{P} - 1))))$
138	61 137	syl5	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (\frac{Q - 1}{2} = P \to (m \in ℤ \to ((m^{2} \mod Q = 2 \mod Q \land \neg Q ∥ m) \to Q ∥ (2^{P} - 1))))$
139	60 138	mpd	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (m \in ℤ \to ((m^{2} \mod Q = 2 \mod Q \land \neg Q ∥ m) \to Q ∥ (2^{P} - 1)))$
140	139	rexlimdv	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (\exists m \in ℤ (m^{2} \mod Q = 2 \mod Q \land \neg Q ∥ m) \to Q ∥ (2^{P} - 1))$
141	37 140	syld	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (2 /_{L} Q = 1 \to Q ∥ (2^{P} - 1))$
142	7 141	sylbird	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (Q \mod 8 \in \{1, 7\} \to Q ∥ (2^{P} - 1))$
143	5 142	syl5	$⊢ ((P \in ℙ \land Q \in ℙ) \land Q = 2 P + 1) \to (Q \mod 8 = 7 \to Q ∥ (2^{P} - 1))$
144	143	ex	$⊢ (P \in ℙ \land Q \in ℙ) \to (Q = 2 P + 1 \to (Q \mod 8 = 7 \to Q ∥ (2^{P} - 1)))$
145	144	com23	$⊢ (P \in ℙ \land Q \in ℙ) \to (Q \mod 8 = 7 \to (Q = 2 P + 1 \to Q ∥ (2^{P} - 1)))$
146	145	ex	$⊢ P \in ℙ \to (Q \in ℙ \to (Q \mod 8 = 7 \to (Q = 2 P + 1 \to Q ∥ (2^{P} - 1))))$
147	146	3imp2	$⊢ (P \in ℙ \land (Q \in ℙ \land Q \mod 8 = 7 \land Q = 2 P + 1)) \to Q ∥ (2^{P} - 1)$

Metamath Proof Explorer

Theorem sfprmdvdsmersenne

Proof