Metamath Proof Explorer


Theorem lighneallem2

Description: Lemma 2 for lighneal . (Contributed by AV, 13-Aug-2021)

Ref Expression
Assertion lighneallem2
|- ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ 2 || N /\ ( ( 2 ^ N ) - 1 ) = ( P ^ M ) ) -> M = 1 )

Proof

Step Hyp Ref Expression
1 evennn2n
 |-  ( N e. NN -> ( 2 || N <-> E. k e. NN ( 2 x. k ) = N ) )
2 1 3ad2ant3
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( 2 || N <-> E. k e. NN ( 2 x. k ) = N ) )
3 oveq2
 |-  ( N = ( 2 x. k ) -> ( 2 ^ N ) = ( 2 ^ ( 2 x. k ) ) )
4 3 eqcoms
 |-  ( ( 2 x. k ) = N -> ( 2 ^ N ) = ( 2 ^ ( 2 x. k ) ) )
5 2cnd
 |-  ( k e. NN -> 2 e. CC )
6 nncn
 |-  ( k e. NN -> k e. CC )
7 5 6 mulcomd
 |-  ( k e. NN -> ( 2 x. k ) = ( k x. 2 ) )
8 7 oveq2d
 |-  ( k e. NN -> ( 2 ^ ( 2 x. k ) ) = ( 2 ^ ( k x. 2 ) ) )
9 2nn0
 |-  2 e. NN0
10 9 a1i
 |-  ( k e. NN -> 2 e. NN0 )
11 nnnn0
 |-  ( k e. NN -> k e. NN0 )
12 5 10 11 expmuld
 |-  ( k e. NN -> ( 2 ^ ( k x. 2 ) ) = ( ( 2 ^ k ) ^ 2 ) )
13 8 12 eqtrd
 |-  ( k e. NN -> ( 2 ^ ( 2 x. k ) ) = ( ( 2 ^ k ) ^ 2 ) )
14 13 adantl
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ k e. NN ) -> ( 2 ^ ( 2 x. k ) ) = ( ( 2 ^ k ) ^ 2 ) )
15 4 14 sylan9eqr
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ k e. NN ) /\ ( 2 x. k ) = N ) -> ( 2 ^ N ) = ( ( 2 ^ k ) ^ 2 ) )
16 15 oveq1d
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ k e. NN ) /\ ( 2 x. k ) = N ) -> ( ( 2 ^ N ) - 1 ) = ( ( ( 2 ^ k ) ^ 2 ) - 1 ) )
17 16 eqeq1d
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ k e. NN ) /\ ( 2 x. k ) = N ) -> ( ( ( 2 ^ N ) - 1 ) = ( P ^ M ) <-> ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) ) )
18 elnn1uz2
 |-  ( k e. NN <-> ( k = 1 \/ k e. ( ZZ>= ` 2 ) ) )
19 oveq2
 |-  ( k = 1 -> ( 2 ^ k ) = ( 2 ^ 1 ) )
20 2cn
 |-  2 e. CC
21 exp1
 |-  ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
22 20 21 ax-mp
 |-  ( 2 ^ 1 ) = 2
23 19 22 eqtrdi
 |-  ( k = 1 -> ( 2 ^ k ) = 2 )
24 23 oveq1d
 |-  ( k = 1 -> ( ( 2 ^ k ) ^ 2 ) = ( 2 ^ 2 ) )
25 24 oveq1d
 |-  ( k = 1 -> ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( ( 2 ^ 2 ) - 1 ) )
26 sq2
 |-  ( 2 ^ 2 ) = 4
27 26 oveq1i
 |-  ( ( 2 ^ 2 ) - 1 ) = ( 4 - 1 )
28 4m1e3
 |-  ( 4 - 1 ) = 3
29 27 28 eqtri
 |-  ( ( 2 ^ 2 ) - 1 ) = 3
30 25 29 eqtrdi
 |-  ( k = 1 -> ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = 3 )
31 30 eqeq1d
 |-  ( k = 1 -> ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) <-> 3 = ( P ^ M ) ) )
32 31 adantr
 |-  ( ( k = 1 /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) <-> 3 = ( P ^ M ) ) )
33 eqcom
 |-  ( 3 = ( P ^ M ) <-> ( P ^ M ) = 3 )
34 eldifi
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
35 prmnn
 |-  ( P e. Prime -> P e. NN )
36 nnre
 |-  ( P e. NN -> P e. RR )
37 34 35 36 3syl
 |-  ( P e. ( Prime \ { 2 } ) -> P e. RR )
38 37 3ad2ant1
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> P e. RR )
39 nnnn0
 |-  ( M e. NN -> M e. NN0 )
40 39 3ad2ant2
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> M e. NN0 )
41 38 40 reexpcld
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( P ^ M ) e. RR )
42 41 adantr
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( P ^ M ) = 3 ) -> ( P ^ M ) e. RR )
43 simpr
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( P ^ M ) = 3 ) -> ( P ^ M ) = 3 )
44 42 43 eqled
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( P ^ M ) = 3 ) -> ( P ^ M ) <_ 3 )
45 44 ex
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( P ^ M ) = 3 -> ( P ^ M ) <_ 3 ) )
46 33 45 syl5bi
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( 3 = ( P ^ M ) -> ( P ^ M ) <_ 3 ) )
47 35 nnred
 |-  ( P e. Prime -> P e. RR )
48 prmgt1
 |-  ( P e. Prime -> 1 < P )
49 47 48 jca
 |-  ( P e. Prime -> ( P e. RR /\ 1 < P ) )
50 34 49 syl
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. RR /\ 1 < P ) )
51 50 3ad2ant1
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( P e. RR /\ 1 < P ) )
52 nnz
 |-  ( M e. NN -> M e. ZZ )
53 52 3ad2ant2
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> M e. ZZ )
54 3rp
 |-  3 e. RR+
55 54 a1i
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> 3 e. RR+ )
56 efexple
 |-  ( ( ( P e. RR /\ 1 < P ) /\ M e. ZZ /\ 3 e. RR+ ) -> ( ( P ^ M ) <_ 3 <-> M <_ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) ) )
57 51 53 55 56 syl3anc
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( P ^ M ) <_ 3 <-> M <_ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) ) )
58 oddprmge3
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 3 ) )
59 eluzle
 |-  ( P e. ( ZZ>= ` 3 ) -> 3 <_ P )
60 58 59 syl
 |-  ( P e. ( Prime \ { 2 } ) -> 3 <_ P )
61 54 a1i
 |-  ( P e. ( Prime \ { 2 } ) -> 3 e. RR+ )
62 nnrp
 |-  ( P e. NN -> P e. RR+ )
63 34 35 62 3syl
 |-  ( P e. ( Prime \ { 2 } ) -> P e. RR+ )
64 61 63 logled
 |-  ( P e. ( Prime \ { 2 } ) -> ( 3 <_ P <-> ( log ` 3 ) <_ ( log ` P ) ) )
65 60 64 mpbid
 |-  ( P e. ( Prime \ { 2 } ) -> ( log ` 3 ) <_ ( log ` P ) )
66 65 3ad2ant1
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( log ` 3 ) <_ ( log ` P ) )
67 relogcl
 |-  ( 3 e. RR+ -> ( log ` 3 ) e. RR )
68 54 67 ax-mp
 |-  ( log ` 3 ) e. RR
69 rplogcl
 |-  ( ( P e. RR /\ 1 < P ) -> ( log ` P ) e. RR+ )
70 34 49 69 3syl
 |-  ( P e. ( Prime \ { 2 } ) -> ( log ` P ) e. RR+ )
71 70 3ad2ant1
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( log ` P ) e. RR+ )
72 divle1le
 |-  ( ( ( log ` 3 ) e. RR /\ ( log ` P ) e. RR+ ) -> ( ( ( log ` 3 ) / ( log ` P ) ) <_ 1 <-> ( log ` 3 ) <_ ( log ` P ) ) )
73 68 71 72 sylancr
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( ( log ` 3 ) / ( log ` P ) ) <_ 1 <-> ( log ` 3 ) <_ ( log ` P ) ) )
74 66 73 mpbird
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( log ` 3 ) / ( log ` P ) ) <_ 1 )
75 fldivle
 |-  ( ( ( log ` 3 ) e. RR /\ ( log ` P ) e. RR+ ) -> ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) <_ ( ( log ` 3 ) / ( log ` P ) ) )
76 68 71 75 sylancr
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) <_ ( ( log ` 3 ) / ( log ` P ) ) )
77 nnre
 |-  ( M e. NN -> M e. RR )
78 77 3ad2ant2
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> M e. RR )
79 68 a1i
 |-  ( P e. ( Prime \ { 2 } ) -> ( log ` 3 ) e. RR )
80 62 relogcld
 |-  ( P e. NN -> ( log ` P ) e. RR )
81 34 35 80 3syl
 |-  ( P e. ( Prime \ { 2 } ) -> ( log ` P ) e. RR )
82 35 nnrpd
 |-  ( P e. Prime -> P e. RR+ )
83 1red
 |-  ( P e. Prime -> 1 e. RR )
84 83 48 gtned
 |-  ( P e. Prime -> P =/= 1 )
85 82 84 jca
 |-  ( P e. Prime -> ( P e. RR+ /\ P =/= 1 ) )
86 logne0
 |-  ( ( P e. RR+ /\ P =/= 1 ) -> ( log ` P ) =/= 0 )
87 34 85 86 3syl
 |-  ( P e. ( Prime \ { 2 } ) -> ( log ` P ) =/= 0 )
88 79 81 87 redivcld
 |-  ( P e. ( Prime \ { 2 } ) -> ( ( log ` 3 ) / ( log ` P ) ) e. RR )
89 88 flcld
 |-  ( P e. ( Prime \ { 2 } ) -> ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) e. ZZ )
90 89 zred
 |-  ( P e. ( Prime \ { 2 } ) -> ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) e. RR )
91 90 3ad2ant1
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) e. RR )
92 88 3ad2ant1
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( log ` 3 ) / ( log ` P ) ) e. RR )
93 letr
 |-  ( ( M e. RR /\ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) e. RR /\ ( ( log ` 3 ) / ( log ` P ) ) e. RR ) -> ( ( M <_ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) /\ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) <_ ( ( log ` 3 ) / ( log ` P ) ) ) -> M <_ ( ( log ` 3 ) / ( log ` P ) ) ) )
94 78 91 92 93 syl3anc
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( M <_ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) /\ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) <_ ( ( log ` 3 ) / ( log ` P ) ) ) -> M <_ ( ( log ` 3 ) / ( log ` P ) ) ) )
95 1red
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> 1 e. RR )
96 letr
 |-  ( ( M e. RR /\ ( ( log ` 3 ) / ( log ` P ) ) e. RR /\ 1 e. RR ) -> ( ( M <_ ( ( log ` 3 ) / ( log ` P ) ) /\ ( ( log ` 3 ) / ( log ` P ) ) <_ 1 ) -> M <_ 1 ) )
97 78 92 95 96 syl3anc
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( M <_ ( ( log ` 3 ) / ( log ` P ) ) /\ ( ( log ` 3 ) / ( log ` P ) ) <_ 1 ) -> M <_ 1 ) )
98 nnge1
 |-  ( M e. NN -> 1 <_ M )
99 eqcom
 |-  ( M = 1 <-> 1 = M )
100 1red
 |-  ( M e. NN -> 1 e. RR )
101 100 77 letri3d
 |-  ( M e. NN -> ( 1 = M <-> ( 1 <_ M /\ M <_ 1 ) ) )
102 99 101 bitr2id
 |-  ( M e. NN -> ( ( 1 <_ M /\ M <_ 1 ) <-> M = 1 ) )
103 102 biimpd
 |-  ( M e. NN -> ( ( 1 <_ M /\ M <_ 1 ) -> M = 1 ) )
104 98 103 mpand
 |-  ( M e. NN -> ( M <_ 1 -> M = 1 ) )
105 104 3ad2ant2
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( M <_ 1 -> M = 1 ) )
106 97 105 syld
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( M <_ ( ( log ` 3 ) / ( log ` P ) ) /\ ( ( log ` 3 ) / ( log ` P ) ) <_ 1 ) -> M = 1 ) )
107 106 expd
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( M <_ ( ( log ` 3 ) / ( log ` P ) ) -> ( ( ( log ` 3 ) / ( log ` P ) ) <_ 1 -> M = 1 ) ) )
108 94 107 syld
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( M <_ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) /\ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) <_ ( ( log ` 3 ) / ( log ` P ) ) ) -> ( ( ( log ` 3 ) / ( log ` P ) ) <_ 1 -> M = 1 ) ) )
109 76 108 mpan2d
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( M <_ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) -> ( ( ( log ` 3 ) / ( log ` P ) ) <_ 1 -> M = 1 ) ) )
110 74 109 mpid
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( M <_ ( |_ ` ( ( log ` 3 ) / ( log ` P ) ) ) -> M = 1 ) )
111 57 110 sylbid
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( P ^ M ) <_ 3 -> M = 1 ) )
112 46 111 syld
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( 3 = ( P ^ M ) -> M = 1 ) )
113 112 adantl
 |-  ( ( k = 1 /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( 3 = ( P ^ M ) -> M = 1 ) )
114 32 113 sylbid
 |-  ( ( k = 1 /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) -> M = 1 ) )
115 114 ex
 |-  ( k = 1 -> ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) -> M = 1 ) ) )
116 sq1
 |-  ( 1 ^ 2 ) = 1
117 116 eqcomi
 |-  1 = ( 1 ^ 2 )
118 117 oveq2i
 |-  ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( ( ( 2 ^ k ) ^ 2 ) - ( 1 ^ 2 ) )
119 118 eqeq1i
 |-  ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) <-> ( ( ( 2 ^ k ) ^ 2 ) - ( 1 ^ 2 ) ) = ( P ^ M ) )
120 eqcom
 |-  ( ( ( ( 2 ^ k ) ^ 2 ) - ( 1 ^ 2 ) ) = ( P ^ M ) <-> ( P ^ M ) = ( ( ( 2 ^ k ) ^ 2 ) - ( 1 ^ 2 ) ) )
121 9 a1i
 |-  ( k e. ( ZZ>= ` 2 ) -> 2 e. NN0 )
122 eluzge2nn0
 |-  ( k e. ( ZZ>= ` 2 ) -> k e. NN0 )
123 121 122 nn0expcld
 |-  ( k e. ( ZZ>= ` 2 ) -> ( 2 ^ k ) e. NN0 )
124 123 adantr
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( 2 ^ k ) e. NN0 )
125 1nn0
 |-  1 e. NN0
126 125 a1i
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> 1 e. NN0 )
127 1p1e2
 |-  ( 1 + 1 ) = 2
128 22 eqcomi
 |-  2 = ( 2 ^ 1 )
129 127 128 eqtri
 |-  ( 1 + 1 ) = ( 2 ^ 1 )
130 eluz2gt1
 |-  ( k e. ( ZZ>= ` 2 ) -> 1 < k )
131 2re
 |-  2 e. RR
132 131 a1i
 |-  ( k e. ( ZZ>= ` 2 ) -> 2 e. RR )
133 1zzd
 |-  ( k e. ( ZZ>= ` 2 ) -> 1 e. ZZ )
134 eluzelz
 |-  ( k e. ( ZZ>= ` 2 ) -> k e. ZZ )
135 1lt2
 |-  1 < 2
136 135 a1i
 |-  ( k e. ( ZZ>= ` 2 ) -> 1 < 2 )
137 132 133 134 136 ltexp2d
 |-  ( k e. ( ZZ>= ` 2 ) -> ( 1 < k <-> ( 2 ^ 1 ) < ( 2 ^ k ) ) )
138 130 137 mpbid
 |-  ( k e. ( ZZ>= ` 2 ) -> ( 2 ^ 1 ) < ( 2 ^ k ) )
139 129 138 eqbrtrid
 |-  ( k e. ( ZZ>= ` 2 ) -> ( 1 + 1 ) < ( 2 ^ k ) )
140 139 adantr
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( 1 + 1 ) < ( 2 ^ k ) )
141 34 39 anim12i
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN ) -> ( P e. Prime /\ M e. NN0 ) )
142 141 3adant3
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( P e. Prime /\ M e. NN0 ) )
143 142 adantl
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( P e. Prime /\ M e. NN0 ) )
144 difsqpwdvds
 |-  ( ( ( ( 2 ^ k ) e. NN0 /\ 1 e. NN0 /\ ( 1 + 1 ) < ( 2 ^ k ) ) /\ ( P e. Prime /\ M e. NN0 ) ) -> ( ( P ^ M ) = ( ( ( 2 ^ k ) ^ 2 ) - ( 1 ^ 2 ) ) -> P || ( 2 x. 1 ) ) )
145 124 126 140 143 144 syl31anc
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( ( P ^ M ) = ( ( ( 2 ^ k ) ^ 2 ) - ( 1 ^ 2 ) ) -> P || ( 2 x. 1 ) ) )
146 2t1e2
 |-  ( 2 x. 1 ) = 2
147 146 breq2i
 |-  ( P || ( 2 x. 1 ) <-> P || 2 )
148 prmuz2
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
149 34 148 syl
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 2 ) )
150 2prm
 |-  2 e. Prime
151 dvdsprm
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ 2 e. Prime ) -> ( P || 2 <-> P = 2 ) )
152 149 150 151 sylancl
 |-  ( P e. ( Prime \ { 2 } ) -> ( P || 2 <-> P = 2 ) )
153 147 152 syl5bb
 |-  ( P e. ( Prime \ { 2 } ) -> ( P || ( 2 x. 1 ) <-> P = 2 ) )
154 eldifsn
 |-  ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) )
155 eqneqall
 |-  ( P = 2 -> ( P =/= 2 -> M = 1 ) )
156 155 com12
 |-  ( P =/= 2 -> ( P = 2 -> M = 1 ) )
157 154 156 simplbiim
 |-  ( P e. ( Prime \ { 2 } ) -> ( P = 2 -> M = 1 ) )
158 153 157 sylbid
 |-  ( P e. ( Prime \ { 2 } ) -> ( P || ( 2 x. 1 ) -> M = 1 ) )
159 158 3ad2ant1
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( P || ( 2 x. 1 ) -> M = 1 ) )
160 159 adantl
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( P || ( 2 x. 1 ) -> M = 1 ) )
161 145 160 syld
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( ( P ^ M ) = ( ( ( 2 ^ k ) ^ 2 ) - ( 1 ^ 2 ) ) -> M = 1 ) )
162 120 161 syl5bi
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( ( ( ( 2 ^ k ) ^ 2 ) - ( 1 ^ 2 ) ) = ( P ^ M ) -> M = 1 ) )
163 119 162 syl5bi
 |-  ( ( k e. ( ZZ>= ` 2 ) /\ ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) ) -> ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) -> M = 1 ) )
164 163 ex
 |-  ( k e. ( ZZ>= ` 2 ) -> ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) -> M = 1 ) ) )
165 115 164 jaoi
 |-  ( ( k = 1 \/ k e. ( ZZ>= ` 2 ) ) -> ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) -> M = 1 ) ) )
166 18 165 sylbi
 |-  ( k e. NN -> ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) -> M = 1 ) ) )
167 166 impcom
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ k e. NN ) -> ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) -> M = 1 ) )
168 167 adantr
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ k e. NN ) /\ ( 2 x. k ) = N ) -> ( ( ( ( 2 ^ k ) ^ 2 ) - 1 ) = ( P ^ M ) -> M = 1 ) )
169 17 168 sylbid
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ k e. NN ) /\ ( 2 x. k ) = N ) -> ( ( ( 2 ^ N ) - 1 ) = ( P ^ M ) -> M = 1 ) )
170 169 rexlimdva2
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( E. k e. NN ( 2 x. k ) = N -> ( ( ( 2 ^ N ) - 1 ) = ( P ^ M ) -> M = 1 ) ) )
171 2 170 sylbid
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( 2 || N -> ( ( ( 2 ^ N ) - 1 ) = ( P ^ M ) -> M = 1 ) ) )
172 171 3imp
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ 2 || N /\ ( ( 2 ^ N ) - 1 ) = ( P ^ M ) ) -> M = 1 )