| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | evennn2n 16389 | . . . 4
⊢ (𝑁 ∈ ℕ → (2
∥ 𝑁 ↔
∃𝑘 ∈ ℕ (2
· 𝑘) = 𝑁)) | 
| 2 | 1 | 3ad2ant3 1135 | . . 3
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (2 ∥ 𝑁 ↔
∃𝑘 ∈ ℕ (2
· 𝑘) = 𝑁)) | 
| 3 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑁 = (2 · 𝑘) → (2↑𝑁) = (2↑(2 · 𝑘))) | 
| 4 | 3 | eqcoms 2744 | . . . . . . . 8
⊢ ((2
· 𝑘) = 𝑁 → (2↑𝑁) = (2↑(2 · 𝑘))) | 
| 5 |  | 2cnd 12345 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 2 ∈
ℂ) | 
| 6 |  | nncn 12275 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) | 
| 7 | 5, 6 | mulcomd 11283 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (2
· 𝑘) = (𝑘 · 2)) | 
| 8 | 7 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ →
(2↑(2 · 𝑘)) =
(2↑(𝑘 ·
2))) | 
| 9 |  | 2nn0 12545 | . . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 | 
| 10 | 9 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 2 ∈
ℕ0) | 
| 11 |  | nnnn0 12535 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) | 
| 12 | 5, 10, 11 | expmuld 14190 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ →
(2↑(𝑘 · 2)) =
((2↑𝑘)↑2)) | 
| 13 | 8, 12 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ →
(2↑(2 · 𝑘)) =
((2↑𝑘)↑2)) | 
| 14 | 13 | adantl 481 | . . . . . . . 8
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ ℕ)
→ (2↑(2 · 𝑘)) = ((2↑𝑘)↑2)) | 
| 15 | 4, 14 | sylan9eqr 2798 | . . . . . . 7
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ ℕ)
∧ (2 · 𝑘) =
𝑁) → (2↑𝑁) = ((2↑𝑘)↑2)) | 
| 16 | 15 | oveq1d 7447 | . . . . . 6
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ ℕ)
∧ (2 · 𝑘) =
𝑁) → ((2↑𝑁) − 1) = (((2↑𝑘)↑2) −
1)) | 
| 17 | 16 | eqeq1d 2738 | . . . . 5
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ ℕ)
∧ (2 · 𝑘) =
𝑁) → (((2↑𝑁) − 1) = (𝑃↑𝑀) ↔ (((2↑𝑘)↑2) − 1) = (𝑃↑𝑀))) | 
| 18 |  | elnn1uz2 12968 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ ↔ (𝑘 = 1 ∨ 𝑘 ∈
(ℤ≥‘2))) | 
| 19 |  | oveq2 7440 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → (2↑𝑘) = (2↑1)) | 
| 20 |  | 2cn 12342 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℂ | 
| 21 |  | exp1 14109 | . . . . . . . . . . . . . . . . . 18
⊢ (2 ∈
ℂ → (2↑1) = 2) | 
| 22 | 20, 21 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢
(2↑1) = 2 | 
| 23 | 19, 22 | eqtrdi 2792 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 1 → (2↑𝑘) = 2) | 
| 24 | 23 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → ((2↑𝑘)↑2) =
(2↑2)) | 
| 25 | 24 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → (((2↑𝑘)↑2) − 1) =
((2↑2) − 1)) | 
| 26 |  | sq2 14237 | . . . . . . . . . . . . . . . 16
⊢
(2↑2) = 4 | 
| 27 | 26 | oveq1i 7442 | . . . . . . . . . . . . . . 15
⊢
((2↑2) − 1) = (4 − 1) | 
| 28 |  | 4m1e3 12396 | . . . . . . . . . . . . . . 15
⊢ (4
− 1) = 3 | 
| 29 | 27, 28 | eqtri 2764 | . . . . . . . . . . . . . 14
⊢
((2↑2) − 1) = 3 | 
| 30 | 25, 29 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑘 = 1 → (((2↑𝑘)↑2) − 1) =
3) | 
| 31 | 30 | eqeq1d 2738 | . . . . . . . . . . . 12
⊢ (𝑘 = 1 → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) ↔ 3 = (𝑃↑𝑀))) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑘 = 1 ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) →
((((2↑𝑘)↑2)
− 1) = (𝑃↑𝑀) ↔ 3 = (𝑃↑𝑀))) | 
| 33 |  | eqcom 2743 | . . . . . . . . . . . . . 14
⊢ (3 =
(𝑃↑𝑀) ↔ (𝑃↑𝑀) = 3) | 
| 34 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℙ) | 
| 35 |  | prmnn 16712 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 36 |  | nnre 12274 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) | 
| 37 | 34, 35, 36 | 3syl 18 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℝ) | 
| 38 | 37 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ 𝑃 ∈
ℝ) | 
| 39 |  | nnnn0 12535 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) | 
| 40 | 39 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ 𝑀 ∈
ℕ0) | 
| 41 | 38, 40 | reexpcld 14204 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑃↑𝑀) ∈
ℝ) | 
| 42 | 41 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ (𝑃↑𝑀) = 3) → (𝑃↑𝑀) ∈ ℝ) | 
| 43 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ (𝑃↑𝑀) = 3) → (𝑃↑𝑀) = 3) | 
| 44 | 42, 43 | eqled 11365 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ (𝑃↑𝑀) = 3) → (𝑃↑𝑀) ≤ 3) | 
| 45 | 44 | ex 412 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((𝑃↑𝑀) = 3 → (𝑃↑𝑀) ≤ 3)) | 
| 46 | 33, 45 | biimtrid 242 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (3 = (𝑃↑𝑀) → (𝑃↑𝑀) ≤ 3)) | 
| 47 | 35 | nnred 12282 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ) | 
| 48 |  | prmgt1 16735 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℙ → 1 <
𝑃) | 
| 49 | 47, 48 | jca 511 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ℝ ∧ 1 <
𝑃)) | 
| 50 | 34, 49 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∈ ℝ
∧ 1 < 𝑃)) | 
| 51 | 50 | 3ad2ant1 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑃 ∈ ℝ
∧ 1 < 𝑃)) | 
| 52 |  | nnz 12636 | . . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) | 
| 53 | 52 | 3ad2ant2 1134 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ 𝑀 ∈
ℤ) | 
| 54 |  | 3rp 13041 | . . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ+ | 
| 55 | 54 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ 3 ∈ ℝ+) | 
| 56 |  | efexple 27326 | . . . . . . . . . . . . . . 15
⊢ (((𝑃 ∈ ℝ ∧ 1 <
𝑃) ∧ 𝑀 ∈ ℤ ∧ 3 ∈
ℝ+) → ((𝑃↑𝑀) ≤ 3 ↔ 𝑀 ≤ (⌊‘((log‘3) /
(log‘𝑃))))) | 
| 57 | 51, 53, 55, 56 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((𝑃↑𝑀) ≤ 3 ↔ 𝑀 ≤
(⌊‘((log‘3) / (log‘𝑃))))) | 
| 58 |  | oddprmge3 16738 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
(ℤ≥‘3)) | 
| 59 |  | eluzle 12892 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈
(ℤ≥‘3) → 3 ≤ 𝑃) | 
| 60 | 58, 59 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 3 ≤ 𝑃) | 
| 61 | 54 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 3 ∈ ℝ+) | 
| 62 |  | nnrp 13047 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ+) | 
| 63 | 34, 35, 62 | 3syl 18 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
ℝ+) | 
| 64 | 61, 63 | logled 26670 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (3 ≤ 𝑃 ↔
(log‘3) ≤ (log‘𝑃))) | 
| 65 | 60, 64 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (log‘3) ≤ (log‘𝑃)) | 
| 66 | 65 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (log‘3) ≤ (log‘𝑃)) | 
| 67 |  | relogcl 26618 | . . . . . . . . . . . . . . . . . 18
⊢ (3 ∈
ℝ+ → (log‘3) ∈ ℝ) | 
| 68 | 54, 67 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢
(log‘3) ∈ ℝ | 
| 69 |  | rplogcl 26647 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℝ ∧ 1 <
𝑃) → (log‘𝑃) ∈
ℝ+) | 
| 70 | 34, 49, 69 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (log‘𝑃) ∈
ℝ+) | 
| 71 | 70 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (log‘𝑃) ∈
ℝ+) | 
| 72 |  | divle1le 13106 | . . . . . . . . . . . . . . . . 17
⊢
(((log‘3) ∈ ℝ ∧ (log‘𝑃) ∈ ℝ+) →
(((log‘3) / (log‘𝑃)) ≤ 1 ↔ (log‘3) ≤
(log‘𝑃))) | 
| 73 | 68, 71, 72 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (((log‘3) / (log‘𝑃)) ≤ 1 ↔ (log‘3) ≤
(log‘𝑃))) | 
| 74 | 66, 73 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((log‘3) / (log‘𝑃)) ≤ 1) | 
| 75 |  | fldivle 13872 | . . . . . . . . . . . . . . . . 17
⊢
(((log‘3) ∈ ℝ ∧ (log‘𝑃) ∈ ℝ+) →
(⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃))) | 
| 76 | 68, 71, 75 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (⌊‘((log‘3) / (log‘𝑃))) ≤ ((log‘3) / (log‘𝑃))) | 
| 77 |  | nnre 12274 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) | 
| 78 | 77 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ 𝑀 ∈
ℝ) | 
| 79 | 68 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (log‘3) ∈ ℝ) | 
| 80 | 62 | relogcld 26666 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℕ →
(log‘𝑃) ∈
ℝ) | 
| 81 | 34, 35, 80 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (log‘𝑃) ∈
ℝ) | 
| 82 | 35 | nnrpd 13076 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℝ+) | 
| 83 |  | 1red 11263 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑃 ∈ ℙ → 1 ∈
ℝ) | 
| 84 | 83, 48 | gtned 11397 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℙ → 𝑃 ≠ 1) | 
| 85 | 82, 84 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ ℝ+
∧ 𝑃 ≠
1)) | 
| 86 |  | logne0 26622 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℝ+
∧ 𝑃 ≠ 1) →
(log‘𝑃) ≠
0) | 
| 87 | 34, 85, 86 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (log‘𝑃) ≠
0) | 
| 88 | 79, 81, 87 | redivcld 12096 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ ((log‘3) / (log‘𝑃)) ∈ ℝ) | 
| 89 | 88 | flcld 13839 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (⌊‘((log‘3) / (log‘𝑃))) ∈ ℤ) | 
| 90 | 89 | zred 12724 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (⌊‘((log‘3) / (log‘𝑃))) ∈ ℝ) | 
| 91 | 90 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (⌊‘((log‘3) / (log‘𝑃))) ∈ ℝ) | 
| 92 | 88 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((log‘3) / (log‘𝑃)) ∈ ℝ) | 
| 93 |  | letr 11356 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℝ ∧
(⌊‘((log‘3) / (log‘𝑃))) ∈ ℝ ∧ ((log‘3) /
(log‘𝑃)) ∈
ℝ) → ((𝑀 ≤
(⌊‘((log‘3) / (log‘𝑃))) ∧ (⌊‘((log‘3) /
(log‘𝑃))) ≤
((log‘3) / (log‘𝑃))) → 𝑀 ≤ ((log‘3) / (log‘𝑃)))) | 
| 94 | 78, 91, 92, 93 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((𝑀 ≤
(⌊‘((log‘3) / (log‘𝑃))) ∧ (⌊‘((log‘3) /
(log‘𝑃))) ≤
((log‘3) / (log‘𝑃))) → 𝑀 ≤ ((log‘3) / (log‘𝑃)))) | 
| 95 |  | 1red 11263 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ 1 ∈ ℝ) | 
| 96 |  | letr 11356 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℝ ∧
((log‘3) / (log‘𝑃)) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝑀 ≤
((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 ≤ 1)) | 
| 97 | 78, 92, 95, 96 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((𝑀 ≤
((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 ≤ 1)) | 
| 98 |  | nnge1 12295 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ → 1 ≤
𝑀) | 
| 99 |  | eqcom 2743 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 = 1 ↔ 1 = 𝑀) | 
| 100 |  | 1red 11263 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 ∈ ℕ → 1 ∈
ℝ) | 
| 101 | 100, 77 | letri3d 11404 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ → (1 =
𝑀 ↔ (1 ≤ 𝑀 ∧ 𝑀 ≤ 1))) | 
| 102 | 99, 101 | bitr2id 284 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℕ → ((1 ≤
𝑀 ∧ 𝑀 ≤ 1) ↔ 𝑀 = 1)) | 
| 103 | 102 | biimpd 229 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ → ((1 ≤
𝑀 ∧ 𝑀 ≤ 1) → 𝑀 = 1)) | 
| 104 | 98, 103 | mpand 695 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ → (𝑀 ≤ 1 → 𝑀 = 1)) | 
| 105 | 104 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑀 ≤ 1 →
𝑀 = 1)) | 
| 106 | 97, 105 | syld 47 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((𝑀 ≤
((log‘3) / (log‘𝑃)) ∧ ((log‘3) / (log‘𝑃)) ≤ 1) → 𝑀 = 1)) | 
| 107 | 106 | expd 415 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑀 ≤
((log‘3) / (log‘𝑃)) → (((log‘3) / (log‘𝑃)) ≤ 1 → 𝑀 = 1))) | 
| 108 | 94, 107 | syld 47 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((𝑀 ≤
(⌊‘((log‘3) / (log‘𝑃))) ∧ (⌊‘((log‘3) /
(log‘𝑃))) ≤
((log‘3) / (log‘𝑃))) → (((log‘3) /
(log‘𝑃)) ≤ 1
→ 𝑀 =
1))) | 
| 109 | 76, 108 | mpan2d 694 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑀 ≤
(⌊‘((log‘3) / (log‘𝑃))) → (((log‘3) /
(log‘𝑃)) ≤ 1
→ 𝑀 =
1))) | 
| 110 | 74, 109 | mpid 44 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑀 ≤
(⌊‘((log‘3) / (log‘𝑃))) → 𝑀 = 1)) | 
| 111 | 57, 110 | sylbid 240 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((𝑃↑𝑀) ≤ 3 → 𝑀 = 1)) | 
| 112 | 46, 111 | syld 47 | . . . . . . . . . . . 12
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (3 = (𝑃↑𝑀) → 𝑀 = 1)) | 
| 113 | 112 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑘 = 1 ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (3 =
(𝑃↑𝑀) → 𝑀 = 1)) | 
| 114 | 32, 113 | sylbid 240 | . . . . . . . . . 10
⊢ ((𝑘 = 1 ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) →
((((2↑𝑘)↑2)
− 1) = (𝑃↑𝑀) → 𝑀 = 1)) | 
| 115 | 114 | ex 412 | . . . . . . . . 9
⊢ (𝑘 = 1 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
((((2↑𝑘)↑2)
− 1) = (𝑃↑𝑀) → 𝑀 = 1))) | 
| 116 |  | sq1 14235 | . . . . . . . . . . . . . 14
⊢
(1↑2) = 1 | 
| 117 | 116 | eqcomi 2745 | . . . . . . . . . . . . 13
⊢ 1 =
(1↑2) | 
| 118 | 117 | oveq2i 7443 | . . . . . . . . . . . 12
⊢
(((2↑𝑘)↑2)
− 1) = (((2↑𝑘)↑2) −
(1↑2)) | 
| 119 | 118 | eqeq1i 2741 | . . . . . . . . . . 11
⊢
((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) ↔ (((2↑𝑘)↑2) − (1↑2)) = (𝑃↑𝑀)) | 
| 120 |  | eqcom 2743 | . . . . . . . . . . . 12
⊢
((((2↑𝑘)↑2) − (1↑2)) = (𝑃↑𝑀) ↔ (𝑃↑𝑀) = (((2↑𝑘)↑2) −
(1↑2))) | 
| 121 | 9 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(ℤ≥‘2) → 2 ∈
ℕ0) | 
| 122 |  | eluzge2nn0 12930 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(ℤ≥‘2) → 𝑘 ∈ ℕ0) | 
| 123 | 121, 122 | nn0expcld 14286 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
(ℤ≥‘2) → (2↑𝑘) ∈
ℕ0) | 
| 124 | 123 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) →
(2↑𝑘) ∈
ℕ0) | 
| 125 |  | 1nn0 12544 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ0 | 
| 126 | 125 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → 1
∈ ℕ0) | 
| 127 |  | 1p1e2 12392 | . . . . . . . . . . . . . . . . 17
⊢ (1 + 1) =
2 | 
| 128 | 22 | eqcomi 2745 | . . . . . . . . . . . . . . . . 17
⊢ 2 =
(2↑1) | 
| 129 | 127, 128 | eqtri 2764 | . . . . . . . . . . . . . . . 16
⊢ (1 + 1) =
(2↑1) | 
| 130 |  | eluz2gt1 12963 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘2) → 1 < 𝑘) | 
| 131 |  | 2re 12341 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ | 
| 132 | 131 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
(ℤ≥‘2) → 2 ∈ ℝ) | 
| 133 |  | 1zzd 12650 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
(ℤ≥‘2) → 1 ∈ ℤ) | 
| 134 |  | eluzelz 12889 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
(ℤ≥‘2) → 𝑘 ∈ ℤ) | 
| 135 |  | 1lt2 12438 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 <
2 | 
| 136 | 135 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
(ℤ≥‘2) → 1 < 2) | 
| 137 | 132, 133,
134, 136 | ltexp2d 14291 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘2) → (1 < 𝑘 ↔ (2↑1) < (2↑𝑘))) | 
| 138 | 130, 137 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(ℤ≥‘2) → (2↑1) < (2↑𝑘)) | 
| 139 | 129, 138 | eqbrtrid 5177 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈
(ℤ≥‘2) → (1 + 1) < (2↑𝑘)) | 
| 140 | 139 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (1 + 1)
< (2↑𝑘)) | 
| 141 | 34, 39 | anim12i 613 | . . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ)
→ (𝑃 ∈ ℙ
∧ 𝑀 ∈
ℕ0)) | 
| 142 | 141 | 3adant3 1132 | . . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑃 ∈ ℙ
∧ 𝑀 ∈
ℕ0)) | 
| 143 | 142 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃 ∈ ℙ ∧ 𝑀 ∈
ℕ0)) | 
| 144 |  | difsqpwdvds 16926 | . . . . . . . . . . . . . 14
⊢
((((2↑𝑘) ∈
ℕ0 ∧ 1 ∈ ℕ0 ∧ (1 + 1) <
(2↑𝑘)) ∧ (𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ0))
→ ((𝑃↑𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑃 ∥ (2 ·
1))) | 
| 145 | 124, 126,
140, 143, 144 | syl31anc 1374 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃↑𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑃 ∥ (2 ·
1))) | 
| 146 |  | 2t1e2 12430 | . . . . . . . . . . . . . . . . . 18
⊢ (2
· 1) = 2 | 
| 147 | 146 | breq2i 5150 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∥ (2 · 1) ↔
𝑃 ∥
2) | 
| 148 |  | prmuz2 16734 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) | 
| 149 | 34, 148 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ 𝑃 ∈
(ℤ≥‘2)) | 
| 150 |  | 2prm 16730 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℙ | 
| 151 |  | dvdsprm 16741 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 2 ∈ ℙ) → (𝑃 ∥ 2 ↔ 𝑃 = 2)) | 
| 152 | 149, 150,
151 | sylancl 586 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∥ 2 ↔
𝑃 = 2)) | 
| 153 | 147, 152 | bitrid 283 | . . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∥ (2
· 1) ↔ 𝑃 =
2)) | 
| 154 |  | eldifsn 4785 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ (ℙ ∖ {2})
↔ (𝑃 ∈ ℙ
∧ 𝑃 ≠
2)) | 
| 155 |  | eqneqall 2950 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑃 = 2 → (𝑃 ≠ 2 → 𝑀 = 1)) | 
| 156 | 155 | com12 32 | . . . . . . . . . . . . . . . . 17
⊢ (𝑃 ≠ 2 → (𝑃 = 2 → 𝑀 = 1)) | 
| 157 | 154, 156 | simplbiim 504 | . . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 = 2 → 𝑀 = 1)) | 
| 158 | 153, 157 | sylbid 240 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ (ℙ ∖ {2})
→ (𝑃 ∥ (2
· 1) → 𝑀 =
1)) | 
| 159 | 158 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (𝑃 ∥ (2
· 1) → 𝑀 =
1)) | 
| 160 | 159 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → (𝑃 ∥ (2 · 1) →
𝑀 = 1)) | 
| 161 | 145, 160 | syld 47 | . . . . . . . . . . . 12
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃↑𝑀) = (((2↑𝑘)↑2) − (1↑2)) → 𝑀 = 1)) | 
| 162 | 120, 161 | biimtrid 242 | . . . . . . . . . . 11
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) →
((((2↑𝑘)↑2)
− (1↑2)) = (𝑃↑𝑀) → 𝑀 = 1)) | 
| 163 | 119, 162 | biimtrid 242 | . . . . . . . . . 10
⊢ ((𝑘 ∈
(ℤ≥‘2) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) →
((((2↑𝑘)↑2)
− 1) = (𝑃↑𝑀) → 𝑀 = 1)) | 
| 164 | 163 | ex 412 | . . . . . . . . 9
⊢ (𝑘 ∈
(ℤ≥‘2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
((((2↑𝑘)↑2)
− 1) = (𝑃↑𝑀) → 𝑀 = 1))) | 
| 165 | 115, 164 | jaoi 857 | . . . . . . . 8
⊢ ((𝑘 = 1 ∨ 𝑘 ∈ (ℤ≥‘2))
→ ((𝑃 ∈ (ℙ
∖ {2}) ∧ 𝑀 ∈
ℕ ∧ 𝑁 ∈
ℕ) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1))) | 
| 166 | 18, 165 | sylbi 217 | . . . . . . 7
⊢ (𝑘 ∈ ℕ → ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1))) | 
| 167 | 166 | impcom 407 | . . . . . 6
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ ℕ)
→ ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1)) | 
| 168 | 167 | adantr 480 | . . . . 5
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ ℕ)
∧ (2 · 𝑘) =
𝑁) → ((((2↑𝑘)↑2) − 1) = (𝑃↑𝑀) → 𝑀 = 1)) | 
| 169 | 17, 168 | sylbid 240 | . . . 4
⊢ ((((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 𝑘 ∈ ℕ)
∧ (2 · 𝑘) =
𝑁) → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1)) | 
| 170 | 169 | rexlimdva2 3156 | . . 3
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (∃𝑘 ∈
ℕ (2 · 𝑘) =
𝑁 → (((2↑𝑁) − 1) = (𝑃↑𝑀) → 𝑀 = 1))) | 
| 171 | 2, 170 | sylbid 240 | . 2
⊢ ((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
→ (2 ∥ 𝑁 →
(((2↑𝑁) − 1) =
(𝑃↑𝑀) → 𝑀 = 1))) | 
| 172 | 171 | 3imp 1110 | 1
⊢ (((𝑃 ∈ (ℙ ∖ {2})
∧ 𝑀 ∈ ℕ
∧ 𝑁 ∈ ℕ)
∧ 2 ∥ 𝑁 ∧
((2↑𝑁) − 1) =
(𝑃↑𝑀)) → 𝑀 = 1) |