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 biimtrid 
 |-  ( ( 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 bitrid 
 |-  ( 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 biimtrid 
 |-  ( ( 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 biimtrid 
 |-  ( ( 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 )