mersenne

Description: A Mersenne prime is a prime number of the form 2 ^ P - 1 . This theorem shows that the P in this expression is necessarily also prime. (Contributed by Mario Carneiro, 17-May-2016)

		Ref	Expression
	Assertion	mersenne	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to P \in ℙ$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to P \in ℤ$
2		2nn0	$⊢ 2 \in ℕ_{0}$
3	2	numexp1	$⊢ 2^{1} = 2$
4		df-2	$⊢ 2 = 1 + 1$
5	3 4	eqtri	$⊢ 2^{1} = 1 + 1$
6		prmuz2	$⊢ 2^{P} - 1 \in ℙ \to 2^{P} - 1 \in ℤ_{\geq 2}$
7	6	adantl	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 2^{P} - 1 \in ℤ_{\geq 2}$
8		eluz2gt1	$⊢ 2^{P} - 1 \in ℤ_{\geq 2} \to 1 < 2^{P} - 1$
9	7 8	syl	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 1 < 2^{P} - 1$
10		1red	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 1 \in ℝ$
11		2re	$⊢ 2 \in ℝ$
12	11	a1i	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 2 \in ℝ$
13		2ne0	$⊢ 2 \neq 0$
14	13	a1i	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 2 \neq 0$
15	12 14 1	reexpclzd	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 2^{P} \in ℝ$
16	10 10 15	ltaddsubd	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to (1 + 1 < 2^{P} \leftrightarrow 1 < 2^{P} - 1)$
17	9 16	mpbird	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 1 + 1 < 2^{P}$
18	5 17	eqbrtrid	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 2^{1} < 2^{P}$
19		1zzd	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 1 \in ℤ$
20		1lt2	$⊢ 1 < 2$
21	20	a1i	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 1 < 2$
22	12 19 1 21	ltexp2d	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to (1 < P \leftrightarrow 2^{1} < 2^{P})$
23	18 22	mpbird	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to 1 < P$
24		eluz2b1	$⊢ P \in ℤ_{\geq 2} \leftrightarrow (P \in ℤ \land 1 < P)$
25	1 23 24	sylanbrc	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to P \in ℤ_{\geq 2}$
26		simpllr	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{P} - 1 \in ℙ$
27		prmnn	$⊢ 2^{P} - 1 \in ℙ \to 2^{P} - 1 \in ℕ$
28	26 27	syl	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{P} - 1 \in ℕ$
29	28	nncnd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{P} - 1 \in ℂ$
30		2nn	$⊢ 2 \in ℕ$
31		elfzuz	$⊢ k \in (2 \dots P - 1) \to k \in ℤ_{\geq 2}$
32	31	ad2antlr	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to k \in ℤ_{\geq 2}$
33		eluz2nn	$⊢ k \in ℤ_{\geq 2} \to k \in ℕ$
34	32 33	syl	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to k \in ℕ$
35	34	nnnn0d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to k \in ℕ_{0}$
36		nnexpcl	$⊢ (2 \in ℕ \land k \in ℕ_{0}) \to 2^{k} \in ℕ$
37	30 35 36	sylancr	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} \in ℕ$
38	37	nnzd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} \in ℤ$
39		peano2zm	$⊢ 2^{k} \in ℤ \to 2^{k} - 1 \in ℤ$
40	38 39	syl	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} - 1 \in ℤ$
41	40	zred	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} - 1 \in ℝ$
42	41	recnd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} - 1 \in ℂ$
43		0red	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 0 \in ℝ$
44		1red	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 1 \in ℝ$
45		0lt1	$⊢ 0 < 1$
46	45	a1i	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 0 < 1$
47		eluz2gt1	$⊢ k \in ℤ_{\geq 2} \to 1 < k$
48	32 47	syl	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 1 < k$
49	11	a1i	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2 \in ℝ$
50		1zzd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 1 \in ℤ$
51		elfzelz	$⊢ k \in (2 \dots P - 1) \to k \in ℤ$
52	51	ad2antlr	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to k \in ℤ$
53	20	a1i	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 1 < 2$
54	49 50 52 53	ltexp2d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to (1 < k \leftrightarrow 2^{1} < 2^{k})$
55	48 54	mpbid	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{1} < 2^{k}$
56	5 55	eqbrtrrid	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 1 + 1 < 2^{k}$
57	37	nnred	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} \in ℝ$
58	44 44 57	ltaddsubd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to (1 + 1 < 2^{k} \leftrightarrow 1 < 2^{k} - 1)$
59	56 58	mpbid	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 1 < 2^{k} - 1$
60	43 44 41 46 59	lttrd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 0 < 2^{k} - 1$
61		elnnz	$⊢ 2^{k} - 1 \in ℕ \leftrightarrow (2^{k} - 1 \in ℤ \land 0 < 2^{k} - 1)$
62	40 60 61	sylanbrc	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} - 1 \in ℕ$
63	62	nnne0d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} - 1 \neq 0$
64	29 42 63	divcan2d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to (2^{k} - 1) (\frac{2^{P} - 1}{2^{k} - 1}) = 2^{P} - 1$
65	64 26	eqeltrd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to (2^{k} - 1) (\frac{2^{P} - 1}{2^{k} - 1}) \in ℙ$
66		eluz2b2	$⊢ 2^{k} - 1 \in ℤ_{\geq 2} \leftrightarrow (2^{k} - 1 \in ℕ \land 1 < 2^{k} - 1)$
67	62 59 66	sylanbrc	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} - 1 \in ℤ_{\geq 2}$
68	37	nncnd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} \in ℂ$
69		ax-1cn	$⊢ 1 \in ℂ$
70		subeq0	$⊢ (2^{k} \in ℂ \land 1 \in ℂ) \to (2^{k} - 1 = 0 \leftrightarrow 2^{k} = 1)$
71	68 69 70	sylancl	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to (2^{k} - 1 = 0 \leftrightarrow 2^{k} = 1)$
72	71	necon3bid	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to (2^{k} - 1 \neq 0 \leftrightarrow 2^{k} \neq 1)$
73	63 72	mpbid	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} \neq 1$
74		simpr	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to k ∥ P$
75		eluz2nn	$⊢ P \in ℤ_{\geq 2} \to P \in ℕ$
76	25 75	syl	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to P \in ℕ$
77	76	ad2antrr	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to P \in ℕ$
78		nndivdvds	$⊢ (P \in ℕ \land k \in ℕ) \to (k ∥ P \leftrightarrow \frac{P}{k} \in ℕ)$
79	77 34 78	syl2anc	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to (k ∥ P \leftrightarrow \frac{P}{k} \in ℕ)$
80	74 79	mpbid	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to \frac{P}{k} \in ℕ$
81	80	nnnn0d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to \frac{P}{k} \in ℕ_{0}$
82	68 73 81	geoser	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to \sum_{n = 0}^{(\frac{P}{k}) - 1} {(2^{k})}^{n} = \frac{1 - {(2^{k})}^{\frac{P}{k}}}{1 - 2^{k}}$
83	15	ad2antrr	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{P} \in ℝ$
84	83	recnd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{P} \in ℂ$
85		negsubdi2	$⊢ (2^{P} \in ℂ \land 1 \in ℂ) \to - (2^{P} - 1) = 1 - 2^{P}$
86	84 69 85	sylancl	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to - (2^{P} - 1) = 1 - 2^{P}$
87	77	nncnd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to P \in ℂ$
88	34	nncnd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to k \in ℂ$
89	34	nnne0d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to k \neq 0$
90	87 88 89	divcan2d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to k (\frac{P}{k}) = P$
91	90	oveq2d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k (\frac{P}{k})} = 2^{P}$
92	49	recnd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2 \in ℂ$
93	92 81 35	expmuld	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k (\frac{P}{k})} = {(2^{k})}^{\frac{P}{k}}$
94	91 93	eqtr3d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{P} = {(2^{k})}^{\frac{P}{k}}$
95	94	oveq2d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 1 - 2^{P} = 1 - {(2^{k})}^{\frac{P}{k}}$
96	86 95	eqtrd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to - (2^{P} - 1) = 1 - {(2^{k})}^{\frac{P}{k}}$
97		negsubdi2	$⊢ (2^{k} \in ℂ \land 1 \in ℂ) \to - (2^{k} - 1) = 1 - 2^{k}$
98	68 69 97	sylancl	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to - (2^{k} - 1) = 1 - 2^{k}$
99	96 98	oveq12d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to \frac{- (2^{P} - 1)}{- (2^{k} - 1)} = \frac{1 - {(2^{k})}^{\frac{P}{k}}}{1 - 2^{k}}$
100	29 42 63	div2negd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to \frac{- (2^{P} - 1)}{- (2^{k} - 1)} = \frac{2^{P} - 1}{2^{k} - 1}$
101	82 99 100	3eqtr2d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to \sum_{n = 0}^{(\frac{P}{k}) - 1} {(2^{k})}^{n} = \frac{2^{P} - 1}{2^{k} - 1}$
102		fzfid	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to (0 \dots (\frac{P}{k}) - 1) \in Fin$
103		elfznn0	$⊢ n \in (0 \dots (\frac{P}{k}) - 1) \to n \in ℕ_{0}$
104		zexpcl	$⊢ (2^{k} \in ℤ \land n \in ℕ_{0}) \to {(2^{k})}^{n} \in ℤ$
105	38 103 104	syl2an	$⊢ ((((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \land n \in (0 \dots (\frac{P}{k}) - 1)) \to {(2^{k})}^{n} \in ℤ$
106	102 105	fsumzcl	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to \sum_{n = 0}^{(\frac{P}{k}) - 1} {(2^{k})}^{n} \in ℤ$
107	101 106	eqeltrrd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to \frac{2^{P} - 1}{2^{k} - 1} \in ℤ$
108	42	mulid2d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 1 (2^{k} - 1) = 2^{k} - 1$
109		2z	$⊢ 2 \in ℤ$
110		elfzm11	$⊢ (2 \in ℤ \land P \in ℤ) \to (k \in (2 \dots P - 1) \leftrightarrow (k \in ℤ \land 2 \leq k \land k < P))$
111	109 1 110	sylancr	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to (k \in (2 \dots P - 1) \leftrightarrow (k \in ℤ \land 2 \leq k \land k < P))$
112	111	biimpa	$⊢ ((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \to (k \in ℤ \land 2 \leq k \land k < P)$
113	112	simp3d	$⊢ ((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \to k < P$
114	113	adantr	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to k < P$
115	1	ad2antrr	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to P \in ℤ$
116	49 52 115 53	ltexp2d	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to (k < P \leftrightarrow 2^{k} < 2^{P})$
117	114 116	mpbid	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} < 2^{P}$
118	57 83 44 117	ltsub1dd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{k} - 1 < 2^{P} - 1$
119	108 118	eqbrtrd	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 1 (2^{k} - 1) < 2^{P} - 1$
120	28	nnred	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 2^{P} - 1 \in ℝ$
121		ltmuldiv	$⊢ (1 \in ℝ \land 2^{P} - 1 \in ℝ \land (2^{k} - 1 \in ℝ \land 0 < 2^{k} - 1)) \to (1 (2^{k} - 1) < 2^{P} - 1 \leftrightarrow 1 < \frac{2^{P} - 1}{2^{k} - 1})$
122	44 120 41 60 121	syl112anc	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to (1 (2^{k} - 1) < 2^{P} - 1 \leftrightarrow 1 < \frac{2^{P} - 1}{2^{k} - 1})$
123	119 122	mpbid	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to 1 < \frac{2^{P} - 1}{2^{k} - 1}$
124		eluz2b1	$⊢ \frac{2^{P} - 1}{2^{k} - 1} \in ℤ_{\geq 2} \leftrightarrow (\frac{2^{P} - 1}{2^{k} - 1} \in ℤ \land 1 < \frac{2^{P} - 1}{2^{k} - 1})$
125	107 123 124	sylanbrc	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to \frac{2^{P} - 1}{2^{k} - 1} \in ℤ_{\geq 2}$
126		nprm	$⊢ (2^{k} - 1 \in ℤ_{\geq 2} \land \frac{2^{P} - 1}{2^{k} - 1} \in ℤ_{\geq 2}) \to \neg (2^{k} - 1) (\frac{2^{P} - 1}{2^{k} - 1}) \in ℙ$
127	67 125 126	syl2anc	$⊢ (((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \land k ∥ P) \to \neg (2^{k} - 1) (\frac{2^{P} - 1}{2^{k} - 1}) \in ℙ$
128	65 127	pm2.65da	$⊢ ((P \in ℤ \land 2^{P} - 1 \in ℙ) \land k \in (2 \dots P - 1)) \to \neg k ∥ P$
129	128	ralrimiva	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to \forall k \in (2 \dots P - 1) \neg k ∥ P$
130		isprm3	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall k \in (2 \dots P - 1) \neg k ∥ P)$
131	25 129 130	sylanbrc	$⊢ (P \in ℤ \land 2^{P} - 1 \in ℙ) \to P \in ℙ$

Metamath Proof Explorer

Theorem mersenne

Proof