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 
|- ( ( ( P e. Prime /\ M e. NN /\ N e. NN ) /\ ( ( 2 ^ N ) - 1 ) = ( P ^ M ) ) -> ( M = 1 /\ N e. Prime ) )

Proof

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