Metamath Proof Explorer

Theorem 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 ( ( ( 𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ( 2 ↑ 𝑁 ) − 1 ) = ( 𝑃 ↑ 𝑀 ) ) → ( 𝑀 = 1 ∧ 𝑁 ∈ ℙ ) )

Proof

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