Metamath Proof Explorer


Theorem lighneallem2

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

Ref Expression
Assertion lighneallem2 ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 2 ∥ 𝑁 ∧ ( ( 2 ↑ 𝑁 ) − 1 ) = ( 𝑃𝑀 ) ) → 𝑀 = 1 )

Proof

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