| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzfid 14014 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (1...(2
· 𝑁)) ∈
Fin) | 
| 2 |  | 2nn 12339 | . . . . . . . . . . 11
⊢ 2 ∈
ℕ | 
| 3 |  | nnmulcl 12290 | . . . . . . . . . . 11
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) | 
| 4 | 2, 3 | mpan 690 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) ∈
ℕ) | 
| 5 | 4 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · 𝑁) ∈
ℕ) | 
| 6 |  | prmnn 16711 | . . . . . . . . . . 11
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 7 | 6 | ad2antlr 727 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑃 ∈ ℕ) | 
| 8 |  | elfznn 13593 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(2 · 𝑁)) → 𝑘 ∈ ℕ) | 
| 9 | 8 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑘 ∈ ℕ) | 
| 10 | 9 | nnnn0d 12587 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑘 ∈ ℕ0) | 
| 11 | 7, 10 | nnexpcld 14284 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑃↑𝑘) ∈ ℕ) | 
| 12 |  | nnrp 13046 | . . . . . . . . . 10
⊢ ((2
· 𝑁) ∈ ℕ
→ (2 · 𝑁)
∈ ℝ+) | 
| 13 |  | nnrp 13046 | . . . . . . . . . 10
⊢ ((𝑃↑𝑘) ∈ ℕ → (𝑃↑𝑘) ∈
ℝ+) | 
| 14 |  | rpdivcl 13060 | . . . . . . . . . 10
⊢ (((2
· 𝑁) ∈
ℝ+ ∧ (𝑃↑𝑘) ∈ ℝ+) → ((2
· 𝑁) / (𝑃↑𝑘)) ∈
ℝ+) | 
| 15 | 12, 13, 14 | syl2an 596 | . . . . . . . . 9
⊢ (((2
· 𝑁) ∈ ℕ
∧ (𝑃↑𝑘) ∈ ℕ) → ((2
· 𝑁) / (𝑃↑𝑘)) ∈
ℝ+) | 
| 16 | 5, 11, 15 | syl2anc 584 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) / (𝑃↑𝑘)) ∈
ℝ+) | 
| 17 | 16 | rpred 13077 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) / (𝑃↑𝑘)) ∈ ℝ) | 
| 18 | 17 | flcld 13838 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘((2
· 𝑁) / (𝑃↑𝑘))) ∈ ℤ) | 
| 19 |  | 2z 12649 | . . . . . . 7
⊢ 2 ∈
ℤ | 
| 20 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑁 ∈ ℕ) | 
| 21 |  | nnrp 13046 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) | 
| 22 |  | rpdivcl 13060 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ+
∧ (𝑃↑𝑘) ∈ ℝ+)
→ (𝑁 / (𝑃↑𝑘)) ∈
ℝ+) | 
| 23 | 21, 13, 22 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ (𝑃↑𝑘) ∈ ℕ) → (𝑁 / (𝑃↑𝑘)) ∈
ℝ+) | 
| 24 | 20, 11, 23 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑁 / (𝑃↑𝑘)) ∈
ℝ+) | 
| 25 | 24 | rpred 13077 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑁 / (𝑃↑𝑘)) ∈ ℝ) | 
| 26 | 25 | flcld 13838 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘(𝑁 / (𝑃↑𝑘))) ∈ ℤ) | 
| 27 |  | zmulcl 12666 | . . . . . . 7
⊢ ((2
∈ ℤ ∧ (⌊‘(𝑁 / (𝑃↑𝑘))) ∈ ℤ) → (2 ·
(⌊‘(𝑁 / (𝑃↑𝑘)))) ∈ ℤ) | 
| 28 | 19, 26, 27 | sylancr 587 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 ·
(⌊‘(𝑁 / (𝑃↑𝑘)))) ∈ ℤ) | 
| 29 | 18, 28 | zsubcld 12727 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ∈ ℤ) | 
| 30 | 29 | zred 12722 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ∈ ℝ) | 
| 31 |  | 1re 11261 | . . . . . 6
⊢ 1 ∈
ℝ | 
| 32 |  | 0re 11263 | . . . . . 6
⊢ 0 ∈
ℝ | 
| 33 | 31, 32 | ifcli 4573 | . . . . 5
⊢ if(𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0) ∈ ℝ | 
| 34 | 33 | a1i 11 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1, 0)
∈ ℝ) | 
| 35 | 28 | zred 12722 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 ·
(⌊‘(𝑁 / (𝑃↑𝑘)))) ∈ ℝ) | 
| 36 | 17, 35 | resubcld 11691 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃↑𝑘)) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ∈ ℝ) | 
| 37 |  | 2re 12340 | . . . . . . . . . 10
⊢ 2 ∈
ℝ | 
| 38 | 37 | a1i 11 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 2 ∈
ℝ) | 
| 39 | 18 | zred 12722 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘((2
· 𝑁) / (𝑃↑𝑘))) ∈ ℝ) | 
| 40 |  | flle 13839 | . . . . . . . . . . 11
⊢ (((2
· 𝑁) / (𝑃↑𝑘)) ∈ ℝ → (⌊‘((2
· 𝑁) / (𝑃↑𝑘))) ≤ ((2 · 𝑁) / (𝑃↑𝑘))) | 
| 41 | 17, 40 | syl 17 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘((2
· 𝑁) / (𝑃↑𝑘))) ≤ ((2 · 𝑁) / (𝑃↑𝑘))) | 
| 42 | 39, 17, 35, 41 | lesub1dd 11879 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ (((2 · 𝑁) / (𝑃↑𝑘)) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))))) | 
| 43 |  | resubcl 11573 | . . . . . . . . . . . . 13
⊢ (((𝑁 / (𝑃↑𝑘)) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((𝑁 / (𝑃↑𝑘)) − 1) ∈
ℝ) | 
| 44 | 25, 31, 43 | sylancl 586 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑁 / (𝑃↑𝑘)) − 1) ∈
ℝ) | 
| 45 |  | remulcl 11240 | . . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ ((𝑁 /
(𝑃↑𝑘)) − 1) ∈ ℝ) → (2
· ((𝑁 / (𝑃↑𝑘)) − 1)) ∈
ℝ) | 
| 46 | 37, 44, 45 | sylancr 587 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · ((𝑁 / (𝑃↑𝑘)) − 1)) ∈
ℝ) | 
| 47 |  | flltp1 13840 | . . . . . . . . . . . . . 14
⊢ ((𝑁 / (𝑃↑𝑘)) ∈ ℝ → (𝑁 / (𝑃↑𝑘)) < ((⌊‘(𝑁 / (𝑃↑𝑘))) + 1)) | 
| 48 | 25, 47 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑁 / (𝑃↑𝑘)) < ((⌊‘(𝑁 / (𝑃↑𝑘))) + 1)) | 
| 49 |  | 1red 11262 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 1 ∈
ℝ) | 
| 50 | 26 | zred 12722 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (⌊‘(𝑁 / (𝑃↑𝑘))) ∈ ℝ) | 
| 51 | 25, 49, 50 | ltsubaddd 11859 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((𝑁 / (𝑃↑𝑘)) − 1) < (⌊‘(𝑁 / (𝑃↑𝑘))) ↔ (𝑁 / (𝑃↑𝑘)) < ((⌊‘(𝑁 / (𝑃↑𝑘))) + 1))) | 
| 52 | 48, 51 | mpbird 257 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑁 / (𝑃↑𝑘)) − 1) < (⌊‘(𝑁 / (𝑃↑𝑘)))) | 
| 53 |  | 2pos 12369 | . . . . . . . . . . . . . . 15
⊢ 0 <
2 | 
| 54 | 37, 53 | pm3.2i 470 | . . . . . . . . . . . . . 14
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 55 |  | ltmul2 12118 | . . . . . . . . . . . . . 14
⊢ ((((𝑁 / (𝑃↑𝑘)) − 1) ∈ ℝ ∧
(⌊‘(𝑁 / (𝑃↑𝑘))) ∈ ℝ ∧ (2 ∈ ℝ
∧ 0 < 2)) → (((𝑁 / (𝑃↑𝑘)) − 1) < (⌊‘(𝑁 / (𝑃↑𝑘))) ↔ (2 · ((𝑁 / (𝑃↑𝑘)) − 1)) < (2 ·
(⌊‘(𝑁 / (𝑃↑𝑘)))))) | 
| 56 | 54, 55 | mp3an3 1452 | . . . . . . . . . . . . 13
⊢ ((((𝑁 / (𝑃↑𝑘)) − 1) ∈ ℝ ∧
(⌊‘(𝑁 / (𝑃↑𝑘))) ∈ ℝ) → (((𝑁 / (𝑃↑𝑘)) − 1) < (⌊‘(𝑁 / (𝑃↑𝑘))) ↔ (2 · ((𝑁 / (𝑃↑𝑘)) − 1)) < (2 ·
(⌊‘(𝑁 / (𝑃↑𝑘)))))) | 
| 57 | 44, 50, 56 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((𝑁 / (𝑃↑𝑘)) − 1) < (⌊‘(𝑁 / (𝑃↑𝑘))) ↔ (2 · ((𝑁 / (𝑃↑𝑘)) − 1)) < (2 ·
(⌊‘(𝑁 / (𝑃↑𝑘)))))) | 
| 58 | 52, 57 | mpbid 232 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · ((𝑁 / (𝑃↑𝑘)) − 1)) < (2 ·
(⌊‘(𝑁 / (𝑃↑𝑘))))) | 
| 59 | 46, 35, 17, 58 | ltsub2dd 11876 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃↑𝑘)) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) < (((2 · 𝑁) / (𝑃↑𝑘)) − (2 · ((𝑁 / (𝑃↑𝑘)) − 1)))) | 
| 60 |  | 2cnd 12344 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 2 ∈
ℂ) | 
| 61 |  | nncn 12274 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 62 | 61 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑁 ∈ ℂ) | 
| 63 | 11 | nncnd 12282 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑃↑𝑘) ∈ ℂ) | 
| 64 | 11 | nnne0d 12316 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑃↑𝑘) ≠ 0) | 
| 65 | 60, 62, 63, 64 | divassd 12078 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) / (𝑃↑𝑘)) = (2 · (𝑁 / (𝑃↑𝑘)))) | 
| 66 | 25 | recnd 11289 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑁 / (𝑃↑𝑘)) ∈ ℂ) | 
| 67 | 60, 66 | muls1d 11723 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · ((𝑁 / (𝑃↑𝑘)) − 1)) = ((2 · (𝑁 / (𝑃↑𝑘))) − 2)) | 
| 68 | 65, 67 | oveq12d 7449 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃↑𝑘)) − (2 · ((𝑁 / (𝑃↑𝑘)) − 1))) = ((2 · (𝑁 / (𝑃↑𝑘))) − ((2 · (𝑁 / (𝑃↑𝑘))) − 2))) | 
| 69 |  | remulcl 11240 | . . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ (𝑁 /
(𝑃↑𝑘)) ∈ ℝ) → (2 · (𝑁 / (𝑃↑𝑘))) ∈ ℝ) | 
| 70 | 37, 25, 69 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · (𝑁 / (𝑃↑𝑘))) ∈ ℝ) | 
| 71 | 70 | recnd 11289 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · (𝑁 / (𝑃↑𝑘))) ∈ ℂ) | 
| 72 |  | 2cn 12341 | . . . . . . . . . . . 12
⊢ 2 ∈
ℂ | 
| 73 |  | nncan 11538 | . . . . . . . . . . . 12
⊢ (((2
· (𝑁 / (𝑃↑𝑘))) ∈ ℂ ∧ 2 ∈ ℂ)
→ ((2 · (𝑁 /
(𝑃↑𝑘))) − ((2 · (𝑁 / (𝑃↑𝑘))) − 2)) = 2) | 
| 74 | 71, 72, 73 | sylancl 586 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · (𝑁 / (𝑃↑𝑘))) − ((2 · (𝑁 / (𝑃↑𝑘))) − 2)) = 2) | 
| 75 | 68, 74 | eqtrd 2777 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃↑𝑘)) − (2 · ((𝑁 / (𝑃↑𝑘)) − 1))) = 2) | 
| 76 | 59, 75 | breqtrd 5169 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃↑𝑘)) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) < 2) | 
| 77 | 30, 36, 38, 42, 76 | lelttrd 11419 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) < 2) | 
| 78 |  | df-2 12329 | . . . . . . . 8
⊢ 2 = (1 +
1) | 
| 79 | 77, 78 | breqtrdi 5184 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) < (1 + 1)) | 
| 80 |  | 1z 12647 | . . . . . . . 8
⊢ 1 ∈
ℤ | 
| 81 |  | zleltp1 12668 | . . . . . . . 8
⊢
((((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ∈ ℤ ∧ 1 ∈ ℤ)
→ (((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ 1 ↔ ((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) < (1 + 1))) | 
| 82 | 29, 80, 81 | sylancl 586 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ 1 ↔ ((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) < (1 + 1))) | 
| 83 | 79, 82 | mpbird 257 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ 1) | 
| 84 |  | iftrue 4531 | . . . . . . 7
⊢ (𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1, 0) =
1) | 
| 85 | 84 | breq2d 5155 | . . . . . 6
⊢ (𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → (((⌊‘((2 ·
𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1, 0)
↔ ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ 1)) | 
| 86 | 83, 85 | syl5ibrcom 247 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))) →
((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1,
0))) | 
| 87 | 9 | nnge1d 12314 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 1 ≤ 𝑘) | 
| 88 | 87 | biantrurd 532 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑘 ≤ (⌊‘((log‘(2 ·
𝑁)) / (log‘𝑃))) ↔ (1 ≤ 𝑘 ∧ 𝑘 ≤ (⌊‘((log‘(2 ·
𝑁)) / (log‘𝑃)))))) | 
| 89 | 6 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈
ℕ) | 
| 90 | 89 | nnred 12281 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈
ℝ) | 
| 91 |  | prmuz2 16733 | . . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) | 
| 92 | 91 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈
(ℤ≥‘2)) | 
| 93 |  | eluz2gt1 12962 | . . . . . . . . . . . . . 14
⊢ (𝑃 ∈
(ℤ≥‘2) → 1 < 𝑃) | 
| 94 | 92, 93 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 <
𝑃) | 
| 95 | 90, 94 | jca 511 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 ∈ ℝ ∧ 1 <
𝑃)) | 
| 96 | 95 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑃 ∈ ℝ ∧ 1 < 𝑃)) | 
| 97 |  | elfzelz 13564 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...(2 · 𝑁)) → 𝑘 ∈ ℤ) | 
| 98 | 97 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑘 ∈ ℤ) | 
| 99 | 4 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2
· 𝑁) ∈
ℕ) | 
| 100 | 99 | nnrpd 13075 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2
· 𝑁) ∈
ℝ+) | 
| 101 | 100 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · 𝑁) ∈
ℝ+) | 
| 102 |  | efexple 27325 | . . . . . . . . . . 11
⊢ (((𝑃 ∈ ℝ ∧ 1 <
𝑃) ∧ 𝑘 ∈ ℤ ∧ (2 · 𝑁) ∈ ℝ+)
→ ((𝑃↑𝑘) ≤ (2 · 𝑁) ↔ 𝑘 ≤ (⌊‘((log‘(2 ·
𝑁)) / (log‘𝑃))))) | 
| 103 | 96, 98, 101, 102 | syl3anc 1373 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑃↑𝑘) ≤ (2 · 𝑁) ↔ 𝑘 ≤ (⌊‘((log‘(2 ·
𝑁)) / (log‘𝑃))))) | 
| 104 | 9 | nnzd 12640 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑘 ∈ ℤ) | 
| 105 | 80 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 1 ∈
ℤ) | 
| 106 | 99 | nnred 12281 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2
· 𝑁) ∈
ℝ) | 
| 107 |  | 1red 11262 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 ∈
ℝ) | 
| 108 | 37 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 2 ∈
ℝ) | 
| 109 |  | 1lt2 12437 | . . . . . . . . . . . . . . . . . 18
⊢ 1 <
2 | 
| 110 | 109 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 <
2) | 
| 111 |  | 2t1e2 12429 | . . . . . . . . . . . . . . . . . 18
⊢ (2
· 1) = 2 | 
| 112 |  | nnre 12273 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 113 | 112 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑁 ∈
ℝ) | 
| 114 |  | 0le2 12368 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ≤
2 | 
| 115 | 37, 114 | pm3.2i 470 | . . . . . . . . . . . . . . . . . . . 20
⊢ (2 ∈
ℝ ∧ 0 ≤ 2) | 
| 116 | 115 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2
∈ ℝ ∧ 0 ≤ 2)) | 
| 117 |  | nnge1 12294 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 1 ≤
𝑁) | 
| 118 | 117 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 ≤
𝑁) | 
| 119 |  | lemul2a 12122 | . . . . . . . . . . . . . . . . . . 19
⊢ (((1
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 ≤ 2)) ∧ 1 ≤ 𝑁) → (2 · 1) ≤ (2
· 𝑁)) | 
| 120 | 107, 113,
116, 118, 119 | syl31anc 1375 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2
· 1) ≤ (2 · 𝑁)) | 
| 121 | 111, 120 | eqbrtrrid 5179 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 2 ≤
(2 · 𝑁)) | 
| 122 | 107, 108,
106, 110, 121 | ltletrd 11421 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 1 <
(2 · 𝑁)) | 
| 123 | 106, 122 | rplogcld 26671 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(log‘(2 · 𝑁))
∈ ℝ+) | 
| 124 | 90, 94 | rplogcld 26671 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(log‘𝑃) ∈
ℝ+) | 
| 125 | 123, 124 | rpdivcld 13094 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
((log‘(2 · 𝑁))
/ (log‘𝑃)) ∈
ℝ+) | 
| 126 | 125 | rpred 13077 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
((log‘(2 · 𝑁))
/ (log‘𝑃)) ∈
ℝ) | 
| 127 | 126 | flcld 13838 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℤ) | 
| 128 | 127 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) →
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℤ) | 
| 129 |  | elfz 13553 | . . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 1 ∈
ℤ ∧ (⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℤ) → (𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔ (1 ≤ 𝑘 ∧ 𝑘 ≤ (⌊‘((log‘(2 ·
𝑁)) / (log‘𝑃)))))) | 
| 130 | 104, 105,
128, 129 | syl3anc 1373 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))) ↔ (1
≤ 𝑘 ∧ 𝑘 ≤
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))))) | 
| 131 | 88, 103, 130 | 3bitr4rd 312 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))) ↔
(𝑃↑𝑘) ≤ (2 · 𝑁))) | 
| 132 | 131 | notbid 318 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (¬ 𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔ ¬ (𝑃↑𝑘) ≤ (2 · 𝑁))) | 
| 133 | 106 | adantr 480 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (2 · 𝑁) ∈
ℝ) | 
| 134 | 11 | nnred 12281 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑃↑𝑘) ∈ ℝ) | 
| 135 | 133, 134 | ltnled 11408 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < (𝑃↑𝑘) ↔ ¬ (𝑃↑𝑘) ≤ (2 · 𝑁))) | 
| 136 | 132, 135 | bitr4d 282 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (¬ 𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔ (2 · 𝑁) < (𝑃↑𝑘))) | 
| 137 | 16 | rpge0d 13081 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 0 ≤ ((2 ·
𝑁) / (𝑃↑𝑘))) | 
| 138 | 137 | adantrr 717 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → 0 ≤ ((2 · 𝑁) / (𝑃↑𝑘))) | 
| 139 | 11 | nngt0d 12315 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 0 < (𝑃↑𝑘)) | 
| 140 |  | ltdivmul 12143 | . . . . . . . . . . . . . . . . 17
⊢ (((2
· 𝑁) ∈ ℝ
∧ 1 ∈ ℝ ∧ ((𝑃↑𝑘) ∈ ℝ ∧ 0 < (𝑃↑𝑘))) → (((2 · 𝑁) / (𝑃↑𝑘)) < 1 ↔ (2 · 𝑁) < ((𝑃↑𝑘) · 1))) | 
| 141 | 133, 49, 134, 139, 140 | syl112anc 1376 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃↑𝑘)) < 1 ↔ (2 · 𝑁) < ((𝑃↑𝑘) · 1))) | 
| 142 | 63 | mulridd 11278 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑃↑𝑘) · 1) = (𝑃↑𝑘)) | 
| 143 | 142 | breq2d 5155 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < ((𝑃↑𝑘) · 1) ↔ (2 · 𝑁) < (𝑃↑𝑘))) | 
| 144 | 141, 143 | bitrd 279 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (((2 · 𝑁) / (𝑃↑𝑘)) < 1 ↔ (2 · 𝑁) < (𝑃↑𝑘))) | 
| 145 | 144 | biimprd 248 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < (𝑃↑𝑘) → ((2 · 𝑁) / (𝑃↑𝑘)) < 1)) | 
| 146 | 145 | impr 454 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → ((2 · 𝑁) / (𝑃↑𝑘)) < 1) | 
| 147 |  | 0p1e1 12388 | . . . . . . . . . . . . 13
⊢ (0 + 1) =
1 | 
| 148 | 146, 147 | breqtrrdi 5185 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → ((2 · 𝑁) / (𝑃↑𝑘)) < (0 + 1)) | 
| 149 | 17 | adantrr 717 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → ((2 · 𝑁) / (𝑃↑𝑘)) ∈ ℝ) | 
| 150 |  | 0z 12624 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℤ | 
| 151 |  | flbi 13856 | . . . . . . . . . . . . 13
⊢ ((((2
· 𝑁) / (𝑃↑𝑘)) ∈ ℝ ∧ 0 ∈ ℤ)
→ ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) = 0 ↔ (0 ≤ ((2 · 𝑁) / (𝑃↑𝑘)) ∧ ((2 · 𝑁) / (𝑃↑𝑘)) < (0 + 1)))) | 
| 152 | 149, 150,
151 | sylancl 586 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) = 0 ↔ (0 ≤ ((2 · 𝑁) / (𝑃↑𝑘)) ∧ ((2 · 𝑁) / (𝑃↑𝑘)) < (0 + 1)))) | 
| 153 | 138, 148,
152 | mpbir2and 713 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → (⌊‘((2 · 𝑁) / (𝑃↑𝑘))) = 0) | 
| 154 | 24 | rpge0d 13081 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 0 ≤ (𝑁 / (𝑃↑𝑘))) | 
| 155 | 154 | adantrr 717 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → 0 ≤ (𝑁 / (𝑃↑𝑘))) | 
| 156 | 112, 21 | ltaddrp2d 13111 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 𝑁)) | 
| 157 | 61 | 2timesd 12509 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → (2
· 𝑁) = (𝑁 + 𝑁)) | 
| 158 | 156, 157 | breqtrrd 5171 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 < (2 · 𝑁)) | 
| 159 | 158 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑁 < (2 · 𝑁)) | 
| 160 | 112 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → 𝑁 ∈ ℝ) | 
| 161 |  | lttr 11337 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℝ ∧ (2
· 𝑁) ∈ ℝ
∧ (𝑃↑𝑘) ∈ ℝ) → ((𝑁 < (2 · 𝑁) ∧ (2 · 𝑁) < (𝑃↑𝑘)) → 𝑁 < (𝑃↑𝑘))) | 
| 162 | 160, 133,
134, 161 | syl3anc 1373 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑁 < (2 · 𝑁) ∧ (2 · 𝑁) < (𝑃↑𝑘)) → 𝑁 < (𝑃↑𝑘))) | 
| 163 | 159, 162 | mpand 695 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < (𝑃↑𝑘) → 𝑁 < (𝑃↑𝑘))) | 
| 164 |  | ltdivmul 12143 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℝ ∧ 1 ∈
ℝ ∧ ((𝑃↑𝑘) ∈ ℝ ∧ 0 < (𝑃↑𝑘))) → ((𝑁 / (𝑃↑𝑘)) < 1 ↔ 𝑁 < ((𝑃↑𝑘) · 1))) | 
| 165 | 160, 49, 134, 139, 164 | syl112anc 1376 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑁 / (𝑃↑𝑘)) < 1 ↔ 𝑁 < ((𝑃↑𝑘) · 1))) | 
| 166 | 142 | breq2d 5155 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (𝑁 < ((𝑃↑𝑘) · 1) ↔ 𝑁 < (𝑃↑𝑘))) | 
| 167 | 165, 166 | bitrd 279 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((𝑁 / (𝑃↑𝑘)) < 1 ↔ 𝑁 < (𝑃↑𝑘))) | 
| 168 | 163, 167 | sylibrd 259 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < (𝑃↑𝑘) → (𝑁 / (𝑃↑𝑘)) < 1)) | 
| 169 | 168 | impr 454 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → (𝑁 / (𝑃↑𝑘)) < 1) | 
| 170 | 169, 147 | breqtrrdi 5185 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → (𝑁 / (𝑃↑𝑘)) < (0 + 1)) | 
| 171 | 25 | adantrr 717 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → (𝑁 / (𝑃↑𝑘)) ∈ ℝ) | 
| 172 |  | flbi 13856 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 / (𝑃↑𝑘)) ∈ ℝ ∧ 0 ∈ ℤ)
→ ((⌊‘(𝑁 /
(𝑃↑𝑘))) = 0 ↔ (0 ≤ (𝑁 / (𝑃↑𝑘)) ∧ (𝑁 / (𝑃↑𝑘)) < (0 + 1)))) | 
| 173 | 171, 150,
172 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → ((⌊‘(𝑁 / (𝑃↑𝑘))) = 0 ↔ (0 ≤ (𝑁 / (𝑃↑𝑘)) ∧ (𝑁 / (𝑃↑𝑘)) < (0 + 1)))) | 
| 174 | 155, 170,
173 | mpbir2and 713 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → (⌊‘(𝑁 / (𝑃↑𝑘))) = 0) | 
| 175 | 174 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))) = (2 · 0)) | 
| 176 |  | 2t0e0 12435 | . . . . . . . . . . . 12
⊢ (2
· 0) = 0 | 
| 177 | 175, 176 | eqtrdi 2793 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))) = 0) | 
| 178 | 153, 177 | oveq12d 7449 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = (0 − 0)) | 
| 179 |  | 0m0e0 12386 | . . . . . . . . . 10
⊢ (0
− 0) = 0 | 
| 180 | 178, 179 | eqtrdi 2793 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) = 0) | 
| 181 |  | 0le0 12367 | . . . . . . . . 9
⊢ 0 ≤
0 | 
| 182 | 180, 181 | eqbrtrdi 5182 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ (𝑘 ∈ (1...(2 · 𝑁)) ∧ (2 · 𝑁) < (𝑃↑𝑘))) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ 0) | 
| 183 | 182 | expr 456 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((2 · 𝑁) < (𝑃↑𝑘) → ((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ 0)) | 
| 184 | 136, 183 | sylbid 240 | . . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (¬ 𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → ((⌊‘((2 ·
𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ 0)) | 
| 185 |  | iffalse 4534 | . . . . . . . 8
⊢ (¬
𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1, 0) =
0) | 
| 186 | 185 | eqcomd 2743 | . . . . . . 7
⊢ (¬
𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → 0 = if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1,
0)) | 
| 187 | 186 | breq2d 5155 | . . . . . 6
⊢ (¬
𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → (((⌊‘((2 ·
𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ 0 ↔ ((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1,
0))) | 
| 188 | 184, 187 | mpbidi 241 | . . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → (¬ 𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) → ((⌊‘((2 ·
𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1,
0))) | 
| 189 | 86, 188 | pm2.61d 179 | . . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) ∧ 𝑘 ∈ (1...(2 · 𝑁))) → ((⌊‘((2
· 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1,
0)) | 
| 190 | 1, 30, 34, 189 | fsumle 15835 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
Σ𝑘 ∈ (1...(2
· 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘))))) ≤ Σ𝑘 ∈ (1...(2 · 𝑁))if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1,
0)) | 
| 191 |  | pcbcctr 27320 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) = Σ𝑘 ∈ (1...(2 · 𝑁))((⌊‘((2 · 𝑁) / (𝑃↑𝑘))) − (2 · (⌊‘(𝑁 / (𝑃↑𝑘)))))) | 
| 192 | 127 | zred 12722 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℝ) | 
| 193 |  | flle 13839 | . . . . . . . . 9
⊢
(((log‘(2 · 𝑁)) / (log‘𝑃)) ∈ ℝ →
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ≤ ((log‘(2 · 𝑁)) / (log‘𝑃))) | 
| 194 | 126, 193 | syl 17 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ≤ ((log‘(2 · 𝑁)) / (log‘𝑃))) | 
| 195 | 99 | nnnn0d 12587 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2
· 𝑁) ∈
ℕ0) | 
| 196 | 89, 195 | nnexpcld 14284 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(2 · 𝑁)) ∈
ℕ) | 
| 197 | 196 | nnred 12281 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(2 · 𝑁)) ∈
ℝ) | 
| 198 |  | bernneq3 14270 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ (2 · 𝑁) ∈ ℕ0) → (2
· 𝑁) < (𝑃↑(2 · 𝑁))) | 
| 199 | 92, 195, 198 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2
· 𝑁) < (𝑃↑(2 · 𝑁))) | 
| 200 | 106, 197,
199 | ltled 11409 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2
· 𝑁) ≤ (𝑃↑(2 · 𝑁))) | 
| 201 | 100 | reeflogd 26666 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(exp‘(log‘(2 · 𝑁))) = (2 · 𝑁)) | 
| 202 | 89 | nnrpd 13075 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈
ℝ+) | 
| 203 | 99 | nnzd 12640 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2
· 𝑁) ∈
ℤ) | 
| 204 |  | reexplog 26637 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℝ+
∧ (2 · 𝑁) ∈
ℤ) → (𝑃↑(2
· 𝑁)) =
(exp‘((2 · 𝑁)
· (log‘𝑃)))) | 
| 205 | 202, 203,
204 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(2 · 𝑁)) = (exp‘((2 ·
𝑁) ·
(log‘𝑃)))) | 
| 206 | 205 | eqcomd 2743 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(exp‘((2 · 𝑁)
· (log‘𝑃))) =
(𝑃↑(2 · 𝑁))) | 
| 207 | 200, 201,
206 | 3brtr4d 5175 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(exp‘(log‘(2 · 𝑁))) ≤ (exp‘((2 · 𝑁) · (log‘𝑃)))) | 
| 208 | 100 | relogcld 26665 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(log‘(2 · 𝑁))
∈ ℝ) | 
| 209 | 124 | rpred 13077 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(log‘𝑃) ∈
ℝ) | 
| 210 | 106, 209 | remulcld 11291 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((2
· 𝑁) ·
(log‘𝑃)) ∈
ℝ) | 
| 211 |  | efle 16154 | . . . . . . . . . . 11
⊢
(((log‘(2 · 𝑁)) ∈ ℝ ∧ ((2 · 𝑁) · (log‘𝑃)) ∈ ℝ) →
((log‘(2 · 𝑁))
≤ ((2 · 𝑁)
· (log‘𝑃))
↔ (exp‘(log‘(2 · 𝑁))) ≤ (exp‘((2 · 𝑁) · (log‘𝑃))))) | 
| 212 | 208, 210,
211 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
((log‘(2 · 𝑁))
≤ ((2 · 𝑁)
· (log‘𝑃))
↔ (exp‘(log‘(2 · 𝑁))) ≤ (exp‘((2 · 𝑁) · (log‘𝑃))))) | 
| 213 | 207, 212 | mpbird 257 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(log‘(2 · 𝑁))
≤ ((2 · 𝑁)
· (log‘𝑃))) | 
| 214 | 208, 106,
124 | ledivmul2d 13131 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(((log‘(2 · 𝑁)) / (log‘𝑃)) ≤ (2 · 𝑁) ↔ (log‘(2 · 𝑁)) ≤ ((2 · 𝑁) · (log‘𝑃)))) | 
| 215 | 213, 214 | mpbird 257 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
((log‘(2 · 𝑁))
/ (log‘𝑃)) ≤ (2
· 𝑁)) | 
| 216 | 192, 126,
106, 194, 215 | letrd 11418 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ≤ (2 · 𝑁)) | 
| 217 |  | eluz 12892 | . . . . . . . 8
⊢
(((⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℤ ∧ (2 · 𝑁) ∈ ℤ) → ((2
· 𝑁) ∈
(ℤ≥‘(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ≤ (2 · 𝑁))) | 
| 218 | 127, 203,
217 | syl2anc 584 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((2
· 𝑁) ∈
(ℤ≥‘(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ↔
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ≤ (2 · 𝑁))) | 
| 219 | 216, 218 | mpbird 257 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (2
· 𝑁) ∈
(ℤ≥‘(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))) | 
| 220 |  | fzss2 13604 | . . . . . 6
⊢ ((2
· 𝑁) ∈
(ℤ≥‘(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) →
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ⊆ (1...(2 · 𝑁))) | 
| 221 | 219, 220 | syl 17 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ⊆ (1...(2 · 𝑁))) | 
| 222 |  | sumhash 16934 | . . . . 5
⊢ (((1...(2
· 𝑁)) ∈ Fin
∧ (1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))) ⊆ (1...(2 · 𝑁))) → Σ𝑘 ∈ (1...(2 · 𝑁))if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1, 0) =
(♯‘(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))))) | 
| 223 | 1, 221, 222 | syl2anc 584 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
Σ𝑘 ∈ (1...(2
· 𝑁))if(𝑘 ∈
(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))), 1, 0) =
(♯‘(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃)))))) | 
| 224 | 125 | rprege0d 13084 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(((log‘(2 · 𝑁)) / (log‘𝑃)) ∈ ℝ ∧ 0 ≤
((log‘(2 · 𝑁))
/ (log‘𝑃)))) | 
| 225 |  | flge0nn0 13860 | . . . . 5
⊢
((((log‘(2 · 𝑁)) / (log‘𝑃)) ∈ ℝ ∧ 0 ≤
((log‘(2 · 𝑁))
/ (log‘𝑃))) →
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈
ℕ0) | 
| 226 |  | hashfz1 14385 | . . . . 5
⊢
((⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) ∈ ℕ0 →
(♯‘(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))) = (⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))) | 
| 227 | 224, 225,
226 | 3syl 18 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(♯‘(1...(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))))) = (⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))) | 
| 228 | 223, 227 | eqtr2d 2778 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) →
(⌊‘((log‘(2 · 𝑁)) / (log‘𝑃))) = Σ𝑘 ∈ (1...(2 · 𝑁))if(𝑘 ∈ (1...(⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))), 1,
0)) | 
| 229 | 190, 191,
228 | 3brtr4d 5175 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) ≤ (⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃)))) | 
| 230 |  | simpr 484 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → 𝑃 ∈
ℙ) | 
| 231 |  | nnnn0 12533 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 232 |  | fzctr 13680 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0...(2
· 𝑁))) | 
| 233 |  | bccl2 14362 | . . . . . . 7
⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ) | 
| 234 | 231, 232,
233 | 3syl 18 | . . . . . 6
⊢ (𝑁 ∈ ℕ → ((2
· 𝑁)C𝑁) ∈
ℕ) | 
| 235 | 234 | adantr 480 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((2
· 𝑁)C𝑁) ∈
ℕ) | 
| 236 | 230, 235 | pccld 16888 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) | 
| 237 | 236 | nn0zd 12639 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ) | 
| 238 |  | efexple 27325 | . . 3
⊢ (((𝑃 ∈ ℝ ∧ 1 <
𝑃) ∧ (𝑃 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ ∧ (2 · 𝑁) ∈ ℝ+)
→ ((𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ↔ (𝑃 pCnt ((2 · 𝑁)C𝑁)) ≤ (⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃))))) | 
| 239 | 90, 94, 237, 100, 238 | syl211anc 1378 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ↔ (𝑃 pCnt ((2 · 𝑁)C𝑁)) ≤ (⌊‘((log‘(2
· 𝑁)) /
(log‘𝑃))))) | 
| 240 | 229, 239 | mpbird 257 | 1
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → (𝑃↑(𝑃 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |