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 biimtrid ⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 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 bitrid ⊢ ( 𝑃 ∈ ( ℙ ∖ { 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 biimtrid ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( ( ( ( 2 ↑ 𝑘 ) ↑ 2 ) − ( 1 ↑ 2 ) ) = ( 𝑃 ↑ 𝑀 ) → 𝑀 = 1 ) )
163 119 162 biimtrid ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 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 )