lighneal

Description: If a power of a prime P (i.e. P ^ M ) is of the form 2 ^ N - 1 , then N must be prime and M must be 1 . Generalization of mersenne (where M = 1 is a prerequisite). Theorem of S. Ligh and L. Neal (1974) "A note on Mersenne mumbers", Mathematics Magazine, 47:4, 231-233. (Contributed by AV, 16-Aug-2021)

		Ref	Expression
	Assertion	lighneal	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land 2^{N} - 1 = P^{M}) \to (M = 1 \land N \in ℙ)$

Proof

Step	Hyp	Ref	Expression
1		lighneallem1	$⊢ (P = 2 \land M \in ℕ \land N \in ℕ) \to 2^{N} - 1 \neq P^{M}$
2		eqneqall	$⊢ 2^{N} - 1 = P^{M} \to (2^{N} - 1 \neq P^{M} \to M = 1)$
3	1 2	syl5com	$⊢ (P = 2 \land M \in ℕ \land N \in ℕ) \to (2^{N} - 1 = P^{M} \to M = 1)$
4	3	3exp	$⊢ P = 2 \to (M \in ℕ \to (N \in ℕ \to (2^{N} - 1 = P^{M} \to M = 1)))$
5	4	a1d	$⊢ P = 2 \to (P \in ℙ \to (M \in ℕ \to (N \in ℕ \to (2^{N} - 1 = P^{M} \to M = 1))))$
6		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
7		lighneallem2	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land 2 ∥ N \land 2^{N} - 1 = P^{M}) \to M = 1$
8	7	3exp	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to (2 ∥ N \to (2^{N} - 1 = P^{M} \to M = 1))$
9	8	3exp	$⊢ P \in (ℙ ∖ \{2\}) \to (M \in ℕ \to (N \in ℕ \to (2 ∥ N \to (2^{N} - 1 = P^{M} \to M = 1))))$
10	9	com3r	$⊢ N \in ℕ \to (P \in (ℙ ∖ \{2\}) \to (M \in ℕ \to (2 ∥ N \to (2^{N} - 1 = P^{M} \to M = 1))))$
11	10	com24	$⊢ N \in ℕ \to (2 ∥ N \to (M \in ℕ \to (P \in (ℙ ∖ \{2\}) \to (2^{N} - 1 = P^{M} \to M = 1))))$
12		lighneallem3	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg 2 ∥ N \land 2 ∥ M) \land 2^{N} - 1 = P^{M}) \to M = 1$
13	12	3exp	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ((\neg 2 ∥ N \land 2 ∥ M) \to (2^{N} - 1 = P^{M} \to M = 1))$
14	13	3exp	$⊢ P \in (ℙ ∖ \{2\}) \to (M \in ℕ \to (N \in ℕ \to ((\neg 2 ∥ N \land 2 ∥ M) \to (2^{N} - 1 = P^{M} \to M = 1))))$
15	14	com24	$⊢ P \in (ℙ ∖ \{2\}) \to ((\neg 2 ∥ N \land 2 ∥ M) \to (N \in ℕ \to (M \in ℕ \to (2^{N} - 1 = P^{M} \to M = 1))))$
16	15	com14	$⊢ M \in ℕ \to ((\neg 2 ∥ N \land 2 ∥ M) \to (N \in ℕ \to (P \in (ℙ ∖ \{2\}) \to (2^{N} - 1 = P^{M} \to M = 1))))$
17	16	expcomd	$⊢ M \in ℕ \to (2 ∥ M \to (\neg 2 ∥ N \to (N \in ℕ \to (P \in (ℙ ∖ \{2\}) \to (2^{N} - 1 = P^{M} \to M = 1)))))$
18		lighneallem4	$⊢ ((P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \land (\neg 2 ∥ N \land \neg 2 ∥ M) \land 2^{N} - 1 = P^{M}) \to M = 1$
19	18	3exp	$⊢ (P \in (ℙ ∖ \{2\}) \land M \in ℕ \land N \in ℕ) \to ((\neg 2 ∥ N \land \neg 2 ∥ M) \to (2^{N} - 1 = P^{M} \to M = 1))$
20	19	3exp	$⊢ P \in (ℙ ∖ \{2\}) \to (M \in ℕ \to (N \in ℕ \to ((\neg 2 ∥ N \land \neg 2 ∥ M) \to (2^{N} - 1 = P^{M} \to M = 1))))$
21	20	com24	$⊢ P \in (ℙ ∖ \{2\}) \to ((\neg 2 ∥ N \land \neg 2 ∥ M) \to (N \in ℕ \to (M \in ℕ \to (2^{N} - 1 = P^{M} \to M = 1))))$
22	21	com14	$⊢ M \in ℕ \to ((\neg 2 ∥ N \land \neg 2 ∥ M) \to (N \in ℕ \to (P \in (ℙ ∖ \{2\}) \to (2^{N} - 1 = P^{M} \to M = 1))))$
23	22	expcomd	$⊢ M \in ℕ \to (\neg 2 ∥ M \to (\neg 2 ∥ N \to (N \in ℕ \to (P \in (ℙ ∖ \{2\}) \to (2^{N} - 1 = P^{M} \to M = 1)))))$
24	17 23	pm2.61d	$⊢ M \in ℕ \to (\neg 2 ∥ N \to (N \in ℕ \to (P \in (ℙ ∖ \{2\}) \to (2^{N} - 1 = P^{M} \to M = 1))))$
25	24	com13	$⊢ N \in ℕ \to (\neg 2 ∥ N \to (M \in ℕ \to (P \in (ℙ ∖ \{2\}) \to (2^{N} - 1 = P^{M} \to M = 1))))$
26	11 25	pm2.61d	$⊢ N \in ℕ \to (M \in ℕ \to (P \in (ℙ ∖ \{2\}) \to (2^{N} - 1 = P^{M} \to M = 1)))$
27	26	com13	$⊢ P \in (ℙ ∖ \{2\}) \to (M \in ℕ \to (N \in ℕ \to (2^{N} - 1 = P^{M} \to M = 1)))$
28	6 27	sylbir	$⊢ (P \in ℙ \land P \neq 2) \to (M \in ℕ \to (N \in ℕ \to (2^{N} - 1 = P^{M} \to M = 1)))$
29	28	expcom	$⊢ P \neq 2 \to (P \in ℙ \to (M \in ℕ \to (N \in ℕ \to (2^{N} - 1 = P^{M} \to M = 1))))$
30	5 29	pm2.61ine	$⊢ P \in ℙ \to (M \in ℕ \to (N \in ℕ \to (2^{N} - 1 = P^{M} \to M = 1)))$
31	30	3imp1	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land 2^{N} - 1 = P^{M}) \to M = 1$
32		oveq2	$⊢ M = 1 \to P^{M} = P^{1}$
33	32	eqeq2d	$⊢ M = 1 \to (2^{N} - 1 = P^{M} \leftrightarrow 2^{N} - 1 = P^{1})$
34	33	adantl	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land M = 1) \to (2^{N} - 1 = P^{M} \leftrightarrow 2^{N} - 1 = P^{1})$
35		prmnn	$⊢ P \in ℙ \to P \in ℕ$
36	35	nncnd	$⊢ P \in ℙ \to P \in ℂ$
37	36	3ad2ant1	$⊢ (P \in ℙ \land M \in ℕ \land N \in ℕ) \to P \in ℂ$
38	37	exp1d	$⊢ (P \in ℙ \land M \in ℕ \land N \in ℕ) \to P^{1} = P$
39	38	eqeq2d	$⊢ (P \in ℙ \land M \in ℕ \land N \in ℕ) \to (2^{N} - 1 = P^{1} \leftrightarrow 2^{N} - 1 = P)$
40		nnz	$⊢ N \in ℕ \to N \in ℤ$
41	40	3ad2ant3	$⊢ (P \in ℙ \land M \in ℕ \land N \in ℕ) \to N \in ℤ$
42		simpl1	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land 2^{N} - 1 = P) \to P \in ℙ$
43		eleq1	$⊢ 2^{N} - 1 = P \to (2^{N} - 1 \in ℙ \leftrightarrow P \in ℙ)$
44	43	adantl	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land 2^{N} - 1 = P) \to (2^{N} - 1 \in ℙ \leftrightarrow P \in ℙ)$
45	42 44	mpbird	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land 2^{N} - 1 = P) \to 2^{N} - 1 \in ℙ$
46		mersenne	$⊢ (N \in ℤ \land 2^{N} - 1 \in ℙ) \to N \in ℙ$
47	41 45 46	syl2an2r	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land 2^{N} - 1 = P) \to N \in ℙ$
48	47	ex	$⊢ (P \in ℙ \land M \in ℕ \land N \in ℕ) \to (2^{N} - 1 = P \to N \in ℙ)$
49	39 48	sylbid	$⊢ (P \in ℙ \land M \in ℕ \land N \in ℕ) \to (2^{N} - 1 = P^{1} \to N \in ℙ)$
50	49	adantr	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land M = 1) \to (2^{N} - 1 = P^{1} \to N \in ℙ)$
51	34 50	sylbid	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land M = 1) \to (2^{N} - 1 = P^{M} \to N \in ℙ)$
52	51	impancom	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land 2^{N} - 1 = P^{M}) \to (M = 1 \to N \in ℙ)$
53	31 52	jcai	$⊢ ((P \in ℙ \land M \in ℕ \land N \in ℕ) \land 2^{N} - 1 = P^{M}) \to (M = 1 \land N \in ℙ)$

Metamath Proof Explorer

Theorem lighneal

Proof