# Metamath Proof Explorer

## Theorem bposlem1

Description: An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014)

Ref Expression
Assertion bposlem1 ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {{P}}^{{P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)}\le 2\cdot {N}$

### Proof

Step Hyp Ref Expression
1 fzfid ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left(1\dots 2\cdot {N}\right)\in \mathrm{Fin}$
2 2nn ${⊢}2\in ℕ$
3 nnmulcl ${⊢}\left(2\in ℕ\wedge {N}\in ℕ\right)\to 2\cdot {N}\in ℕ$
4 2 3 mpan ${⊢}{N}\in ℕ\to 2\cdot {N}\in ℕ$
5 4 ad2antrr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\cdot {N}\in ℕ$
6 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
7 6 ad2antlr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {P}\in ℕ$
8 elfznn ${⊢}{k}\in \left(1\dots 2\cdot {N}\right)\to {k}\in ℕ$
9 8 adantl ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {k}\in ℕ$
10 9 nnnn0d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {k}\in {ℕ}_{0}$
11 7 10 nnexpcld ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {{P}}^{{k}}\in ℕ$
12 nnrp ${⊢}2\cdot {N}\in ℕ\to 2\cdot {N}\in {ℝ}^{+}$
13 nnrp ${⊢}{{P}}^{{k}}\in ℕ\to {{P}}^{{k}}\in {ℝ}^{+}$
14 rpdivcl ${⊢}\left(2\cdot {N}\in {ℝ}^{+}\wedge {{P}}^{{k}}\in {ℝ}^{+}\right)\to \frac{2\cdot {N}}{{{P}}^{{k}}}\in {ℝ}^{+}$
15 12 13 14 syl2an ${⊢}\left(2\cdot {N}\in ℕ\wedge {{P}}^{{k}}\in ℕ\right)\to \frac{2\cdot {N}}{{{P}}^{{k}}}\in {ℝ}^{+}$
16 5 11 15 syl2anc ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \frac{2\cdot {N}}{{{P}}^{{k}}}\in {ℝ}^{+}$
17 16 rpred ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \frac{2\cdot {N}}{{{P}}^{{k}}}\in ℝ$
18 17 flcld ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋\in ℤ$
19 2z ${⊢}2\in ℤ$
20 simpll ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {N}\in ℕ$
21 nnrp ${⊢}{N}\in ℕ\to {N}\in {ℝ}^{+}$
22 rpdivcl ${⊢}\left({N}\in {ℝ}^{+}\wedge {{P}}^{{k}}\in {ℝ}^{+}\right)\to \frac{{N}}{{{P}}^{{k}}}\in {ℝ}^{+}$
23 21 13 22 syl2an ${⊢}\left({N}\in ℕ\wedge {{P}}^{{k}}\in ℕ\right)\to \frac{{N}}{{{P}}^{{k}}}\in {ℝ}^{+}$
24 20 11 23 syl2anc ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \frac{{N}}{{{P}}^{{k}}}\in {ℝ}^{+}$
25 24 rpred ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \frac{{N}}{{{P}}^{{k}}}\in ℝ$
26 25 flcld ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℤ$
27 zmulcl ${⊢}\left(2\in ℤ\wedge ⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℤ\right)\to 2⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℤ$
28 19 26 27 sylancr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℤ$
29 18 28 zsubcld ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℤ$
30 29 zred ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℝ$
31 1re ${⊢}1\in ℝ$
32 0re ${⊢}0\in ℝ$
33 31 32 ifcli ${⊢}if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)\in ℝ$
34 33 a1i ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)\in ℝ$
35 28 zred ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℝ$
36 17 35 resubcld ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{2\cdot {N}}{{{P}}^{{k}}}\right)-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℝ$
37 2re ${⊢}2\in ℝ$
38 37 a1i ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\in ℝ$
39 18 zred ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋\in ℝ$
40 flle ${⊢}\frac{2\cdot {N}}{{{P}}^{{k}}}\in ℝ\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋\le \frac{2\cdot {N}}{{{P}}^{{k}}}$
41 17 40 syl ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋\le \frac{2\cdot {N}}{{{P}}^{{k}}}$
42 39 17 35 41 lesub1dd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le \left(\frac{2\cdot {N}}{{{P}}^{{k}}}\right)-2⌊\frac{{N}}{{{P}}^{{k}}}⌋$
43 resubcl ${⊢}\left(\frac{{N}}{{{P}}^{{k}}}\in ℝ\wedge 1\in ℝ\right)\to \left(\frac{{N}}{{{P}}^{{k}}}\right)-1\in ℝ$
44 25 31 43 sylancl ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{{N}}{{{P}}^{{k}}}\right)-1\in ℝ$
45 remulcl ${⊢}\left(2\in ℝ\wedge \left(\frac{{N}}{{{P}}^{{k}}}\right)-1\in ℝ\right)\to 2\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\right)\in ℝ$
46 37 44 45 sylancr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\right)\in ℝ$
47 flltp1 ${⊢}\frac{{N}}{{{P}}^{{k}}}\in ℝ\to \frac{{N}}{{{P}}^{{k}}}<⌊\frac{{N}}{{{P}}^{{k}}}⌋+1$
48 25 47 syl ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \frac{{N}}{{{P}}^{{k}}}<⌊\frac{{N}}{{{P}}^{{k}}}⌋+1$
49 1red ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 1\in ℝ$
50 26 zred ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℝ$
51 25 49 50 ltsubaddd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1<⌊\frac{{N}}{{{P}}^{{k}}}⌋↔\frac{{N}}{{{P}}^{{k}}}<⌊\frac{{N}}{{{P}}^{{k}}}⌋+1\right)$
52 48 51 mpbird ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{{N}}{{{P}}^{{k}}}\right)-1<⌊\frac{{N}}{{{P}}^{{k}}}⌋$
53 2pos ${⊢}0<2$
54 37 53 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
55 ltmul2 ${⊢}\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\in ℝ\wedge ⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1<⌊\frac{{N}}{{{P}}^{{k}}}⌋↔2\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\right)<2⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)$
56 54 55 mp3an3 ${⊢}\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\in ℝ\wedge ⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℝ\right)\to \left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1<⌊\frac{{N}}{{{P}}^{{k}}}⌋↔2\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\right)<2⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)$
57 44 50 56 syl2anc ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1<⌊\frac{{N}}{{{P}}^{{k}}}⌋↔2\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\right)<2⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)$
58 52 57 mpbid ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\right)<2⌊\frac{{N}}{{{P}}^{{k}}}⌋$
59 46 35 17 58 ltsub2dd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{2\cdot {N}}{{{P}}^{{k}}}\right)-2⌊\frac{{N}}{{{P}}^{{k}}}⌋<\left(\frac{2\cdot {N}}{{{P}}^{{k}}}\right)-2\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\right)$
60 2cnd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\in ℂ$
61 nncn ${⊢}{N}\in ℕ\to {N}\in ℂ$
62 61 ad2antrr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {N}\in ℂ$
63 11 nncnd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {{P}}^{{k}}\in ℂ$
64 11 nnne0d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {{P}}^{{k}}\ne 0$
65 60 62 63 64 divassd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \frac{2\cdot {N}}{{{P}}^{{k}}}=2\left(\frac{{N}}{{{P}}^{{k}}}\right)$
66 25 recnd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \frac{{N}}{{{P}}^{{k}}}\in ℂ$
67 60 66 muls1d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\right)=2\left(\frac{{N}}{{{P}}^{{k}}}\right)-2$
68 65 67 oveq12d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{2\cdot {N}}{{{P}}^{{k}}}\right)-2\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\right)=2\left(\frac{{N}}{{{P}}^{{k}}}\right)-\left(2\left(\frac{{N}}{{{P}}^{{k}}}\right)-2\right)$
69 remulcl ${⊢}\left(2\in ℝ\wedge \frac{{N}}{{{P}}^{{k}}}\in ℝ\right)\to 2\left(\frac{{N}}{{{P}}^{{k}}}\right)\in ℝ$
70 37 25 69 sylancr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\left(\frac{{N}}{{{P}}^{{k}}}\right)\in ℝ$
71 70 recnd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\left(\frac{{N}}{{{P}}^{{k}}}\right)\in ℂ$
72 2cn ${⊢}2\in ℂ$
73 nncan ${⊢}\left(2\left(\frac{{N}}{{{P}}^{{k}}}\right)\in ℂ\wedge 2\in ℂ\right)\to 2\left(\frac{{N}}{{{P}}^{{k}}}\right)-\left(2\left(\frac{{N}}{{{P}}^{{k}}}\right)-2\right)=2$
74 71 72 73 sylancl ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\left(\frac{{N}}{{{P}}^{{k}}}\right)-\left(2\left(\frac{{N}}{{{P}}^{{k}}}\right)-2\right)=2$
75 68 74 eqtrd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{2\cdot {N}}{{{P}}^{{k}}}\right)-2\left(\left(\frac{{N}}{{{P}}^{{k}}}\right)-1\right)=2$
76 59 75 breqtrd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{2\cdot {N}}{{{P}}^{{k}}}\right)-2⌊\frac{{N}}{{{P}}^{{k}}}⌋<2$
77 30 36 38 42 76 lelttrd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋<2$
78 df-2 ${⊢}2=1+1$
79 77 78 breqtrdi ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋<1+1$
80 1z ${⊢}1\in ℤ$
81 zleltp1 ${⊢}\left(⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\in ℤ\wedge 1\in ℤ\right)\to \left(⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le 1↔⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋<1+1\right)$
82 29 80 81 sylancl ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le 1↔⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋<1+1\right)$
83 79 82 mpbird ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le 1$
84 iftrue ${⊢}{k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\to if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)=1$
85 84 breq2d ${⊢}{k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\to \left(⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)↔⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le 1\right)$
86 83 85 syl5ibrcom ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)\right)$
87 9 nnge1d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 1\le {k}$
88 87 biantrurd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left({k}\le ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋↔\left(1\le {k}\wedge {k}\le ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\right)$
89 6 adantl ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {P}\in ℕ$
90 89 nnred ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {P}\in ℝ$
91 prmuz2 ${⊢}{P}\in ℙ\to {P}\in {ℤ}_{\ge 2}$
92 91 adantl ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {P}\in {ℤ}_{\ge 2}$
93 eluz2gt1 ${⊢}{P}\in {ℤ}_{\ge 2}\to 1<{P}$
94 92 93 syl ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 1<{P}$
95 90 94 jca ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left({P}\in ℝ\wedge 1<{P}\right)$
96 95 adantr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left({P}\in ℝ\wedge 1<{P}\right)$
97 elfzelz ${⊢}{k}\in \left(1\dots 2\cdot {N}\right)\to {k}\in ℤ$
98 97 adantl ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {k}\in ℤ$
99 4 adantr ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\cdot {N}\in ℕ$
100 99 nnrpd ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\cdot {N}\in {ℝ}^{+}$
101 100 adantr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\cdot {N}\in {ℝ}^{+}$
102 efexple ${⊢}\left(\left({P}\in ℝ\wedge 1<{P}\right)\wedge {k}\in ℤ\wedge 2\cdot {N}\in {ℝ}^{+}\right)\to \left({{P}}^{{k}}\le 2\cdot {N}↔{k}\le ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)$
103 96 98 101 102 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left({{P}}^{{k}}\le 2\cdot {N}↔{k}\le ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)$
104 9 nnzd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {k}\in ℤ$
105 80 a1i ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 1\in ℤ$
106 99 nnred ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\cdot {N}\in ℝ$
107 1red ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 1\in ℝ$
108 37 a1i ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\in ℝ$
109 1lt2 ${⊢}1<2$
110 109 a1i ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 1<2$
111 2t1e2 ${⊢}2\cdot 1=2$
112 nnre ${⊢}{N}\in ℕ\to {N}\in ℝ$
113 112 adantr ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {N}\in ℝ$
114 0le2 ${⊢}0\le 2$
115 37 114 pm3.2i ${⊢}\left(2\in ℝ\wedge 0\le 2\right)$
116 115 a1i ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left(2\in ℝ\wedge 0\le 2\right)$
117 nnge1 ${⊢}{N}\in ℕ\to 1\le {N}$
118 117 adantr ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 1\le {N}$
119 lemul2a ${⊢}\left(\left(1\in ℝ\wedge {N}\in ℝ\wedge \left(2\in ℝ\wedge 0\le 2\right)\right)\wedge 1\le {N}\right)\to 2\cdot 1\le 2\cdot {N}$
120 107 113 116 118 119 syl31anc ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\cdot 1\le 2\cdot {N}$
121 111 120 eqbrtrrid ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\le 2\cdot {N}$
122 107 108 106 110 121 ltletrd ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 1<2\cdot {N}$
123 106 122 rplogcld ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \mathrm{log}2\cdot {N}\in {ℝ}^{+}$
124 90 94 rplogcld ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \mathrm{log}{P}\in {ℝ}^{+}$
125 123 124 rpdivcld ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}\in {ℝ}^{+}$
126 125 rpred ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}\in ℝ$
127 126 flcld ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\in ℤ$
128 127 adantr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\in ℤ$
129 elfz ${⊢}\left({k}\in ℤ\wedge 1\in ℤ\wedge ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\in ℤ\right)\to \left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)↔\left(1\le {k}\wedge {k}\le ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\right)$
130 104 105 128 129 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)↔\left(1\le {k}\wedge {k}\le ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\right)$
131 88 103 130 3bitr4rd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)↔{{P}}^{{k}}\le 2\cdot {N}\right)$
132 131 notbid ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(¬{k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)↔¬{{P}}^{{k}}\le 2\cdot {N}\right)$
133 106 adantr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 2\cdot {N}\in ℝ$
134 11 nnred ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {{P}}^{{k}}\in ℝ$
135 133 134 ltnled ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(2\cdot {N}<{{P}}^{{k}}↔¬{{P}}^{{k}}\le 2\cdot {N}\right)$
136 132 135 bitr4d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(¬{k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)↔2\cdot {N}<{{P}}^{{k}}\right)$
137 16 rpge0d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 0\le \frac{2\cdot {N}}{{{P}}^{{k}}}$
138 137 adantrr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to 0\le \frac{2\cdot {N}}{{{P}}^{{k}}}$
139 11 nngt0d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 0<{{P}}^{{k}}$
140 ltdivmul ${⊢}\left(2\cdot {N}\in ℝ\wedge 1\in ℝ\wedge \left({{P}}^{{k}}\in ℝ\wedge 0<{{P}}^{{k}}\right)\right)\to \left(\frac{2\cdot {N}}{{{P}}^{{k}}}<1↔2\cdot {N}<{{P}}^{{k}}\cdot 1\right)$
141 133 49 134 139 140 syl112anc ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{2\cdot {N}}{{{P}}^{{k}}}<1↔2\cdot {N}<{{P}}^{{k}}\cdot 1\right)$
142 63 mulid1d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {{P}}^{{k}}\cdot 1={{P}}^{{k}}$
143 142 breq2d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(2\cdot {N}<{{P}}^{{k}}\cdot 1↔2\cdot {N}<{{P}}^{{k}}\right)$
144 141 143 bitrd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{2\cdot {N}}{{{P}}^{{k}}}<1↔2\cdot {N}<{{P}}^{{k}}\right)$
145 144 biimprd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(2\cdot {N}<{{P}}^{{k}}\to \frac{2\cdot {N}}{{{P}}^{{k}}}<1\right)$
146 145 impr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to \frac{2\cdot {N}}{{{P}}^{{k}}}<1$
147 0p1e1 ${⊢}0+1=1$
148 146 147 breqtrrdi ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to \frac{2\cdot {N}}{{{P}}^{{k}}}<0+1$
149 17 adantrr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to \frac{2\cdot {N}}{{{P}}^{{k}}}\in ℝ$
150 0z ${⊢}0\in ℤ$
151 flbi ${⊢}\left(\frac{2\cdot {N}}{{{P}}^{{k}}}\in ℝ\wedge 0\in ℤ\right)\to \left(⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋=0↔\left(0\le \frac{2\cdot {N}}{{{P}}^{{k}}}\wedge \frac{2\cdot {N}}{{{P}}^{{k}}}<0+1\right)\right)$
152 149 150 151 sylancl ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to \left(⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋=0↔\left(0\le \frac{2\cdot {N}}{{{P}}^{{k}}}\wedge \frac{2\cdot {N}}{{{P}}^{{k}}}<0+1\right)\right)$
153 138 148 152 mpbir2and ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋=0$
154 24 rpge0d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to 0\le \frac{{N}}{{{P}}^{{k}}}$
155 154 adantrr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to 0\le \frac{{N}}{{{P}}^{{k}}}$
156 112 21 ltaddrp2d ${⊢}{N}\in ℕ\to {N}<{N}+{N}$
157 61 2timesd ${⊢}{N}\in ℕ\to 2\cdot {N}={N}+{N}$
158 156 157 breqtrrd ${⊢}{N}\in ℕ\to {N}<2\cdot {N}$
159 158 ad2antrr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {N}<2\cdot {N}$
160 112 ad2antrr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to {N}\in ℝ$
161 lttr ${⊢}\left({N}\in ℝ\wedge 2\cdot {N}\in ℝ\wedge {{P}}^{{k}}\in ℝ\right)\to \left(\left({N}<2\cdot {N}\wedge 2\cdot {N}<{{P}}^{{k}}\right)\to {N}<{{P}}^{{k}}\right)$
162 160 133 134 161 syl3anc ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\left({N}<2\cdot {N}\wedge 2\cdot {N}<{{P}}^{{k}}\right)\to {N}<{{P}}^{{k}}\right)$
163 159 162 mpand ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(2\cdot {N}<{{P}}^{{k}}\to {N}<{{P}}^{{k}}\right)$
164 ltdivmul ${⊢}\left({N}\in ℝ\wedge 1\in ℝ\wedge \left({{P}}^{{k}}\in ℝ\wedge 0<{{P}}^{{k}}\right)\right)\to \left(\frac{{N}}{{{P}}^{{k}}}<1↔{N}<{{P}}^{{k}}\cdot 1\right)$
165 160 49 134 139 164 syl112anc ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{{N}}{{{P}}^{{k}}}<1↔{N}<{{P}}^{{k}}\cdot 1\right)$
166 142 breq2d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left({N}<{{P}}^{{k}}\cdot 1↔{N}<{{P}}^{{k}}\right)$
167 165 166 bitrd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(\frac{{N}}{{{P}}^{{k}}}<1↔{N}<{{P}}^{{k}}\right)$
168 163 167 sylibrd ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(2\cdot {N}<{{P}}^{{k}}\to \frac{{N}}{{{P}}^{{k}}}<1\right)$
169 168 impr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to \frac{{N}}{{{P}}^{{k}}}<1$
170 169 147 breqtrrdi ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to \frac{{N}}{{{P}}^{{k}}}<0+1$
171 25 adantrr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to \frac{{N}}{{{P}}^{{k}}}\in ℝ$
172 flbi ${⊢}\left(\frac{{N}}{{{P}}^{{k}}}\in ℝ\wedge 0\in ℤ\right)\to \left(⌊\frac{{N}}{{{P}}^{{k}}}⌋=0↔\left(0\le \frac{{N}}{{{P}}^{{k}}}\wedge \frac{{N}}{{{P}}^{{k}}}<0+1\right)\right)$
173 171 150 172 sylancl ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to \left(⌊\frac{{N}}{{{P}}^{{k}}}⌋=0↔\left(0\le \frac{{N}}{{{P}}^{{k}}}\wedge \frac{{N}}{{{P}}^{{k}}}<0+1\right)\right)$
174 155 170 173 mpbir2and ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to ⌊\frac{{N}}{{{P}}^{{k}}}⌋=0$
175 174 oveq2d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to 2⌊\frac{{N}}{{{P}}^{{k}}}⌋=2\cdot 0$
176 2t0e0 ${⊢}2\cdot 0=0$
177 175 176 syl6eq ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to 2⌊\frac{{N}}{{{P}}^{{k}}}⌋=0$
178 153 177 oveq12d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋=0-0$
179 0m0e0 ${⊢}0-0=0$
180 178 179 syl6eq ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋=0$
181 0le0 ${⊢}0\le 0$
182 180 181 eqbrtrdi ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge \left({k}\in \left(1\dots 2\cdot {N}\right)\wedge 2\cdot {N}<{{P}}^{{k}}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le 0$
183 182 expr ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(2\cdot {N}<{{P}}^{{k}}\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le 0\right)$
184 136 183 sylbid ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(¬{k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le 0\right)$
185 iffalse ${⊢}¬{k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\to if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)=0$
186 185 eqcomd ${⊢}¬{k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\to 0=if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)$
187 186 breq2d ${⊢}¬{k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\to \left(⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le 0↔⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)\right)$
188 184 187 mpbidi ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to \left(¬{k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)\right)$
189 86 188 pm2.61d ${⊢}\left(\left({N}\in ℕ\wedge {P}\in ℙ\right)\wedge {k}\in \left(1\dots 2\cdot {N}\right)\right)\to ⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\le if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)$
190 1 30 34 189 fsumle ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \sum _{{k}=1}^{2\cdot {N}}\left(⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)\le \sum _{{k}=1}^{2\cdot {N}}if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)$
191 pcbcctr ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)=\sum _{{k}=1}^{2\cdot {N}}\left(⌊\frac{2\cdot {N}}{{{P}}^{{k}}}⌋-2⌊\frac{{N}}{{{P}}^{{k}}}⌋\right)$
192 127 zred ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\in ℝ$
193 flle ${⊢}\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}\in ℝ\to ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\le \frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}$
194 126 193 syl ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\le \frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}$
195 99 nnnn0d ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\cdot {N}\in {ℕ}_{0}$
196 89 195 nnexpcld ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {{P}}^{2\cdot {N}}\in ℕ$
197 196 nnred ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {{P}}^{2\cdot {N}}\in ℝ$
198 bernneq3 ${⊢}\left({P}\in {ℤ}_{\ge 2}\wedge 2\cdot {N}\in {ℕ}_{0}\right)\to 2\cdot {N}<{{P}}^{2\cdot {N}}$
199 92 195 198 syl2anc ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\cdot {N}<{{P}}^{2\cdot {N}}$
200 106 197 199 ltled ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\cdot {N}\le {{P}}^{2\cdot {N}}$
201 100 reeflogd ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {\mathrm{e}}^{\mathrm{log}2\cdot {N}}=2\cdot {N}$
202 89 nnrpd ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {P}\in {ℝ}^{+}$
203 99 nnzd ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\cdot {N}\in ℤ$
204 reexplog ${⊢}\left({P}\in {ℝ}^{+}\wedge 2\cdot {N}\in ℤ\right)\to {{P}}^{2\cdot {N}}={\mathrm{e}}^{2\cdot {N}\mathrm{log}{P}}$
205 202 203 204 syl2anc ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {{P}}^{2\cdot {N}}={\mathrm{e}}^{2\cdot {N}\mathrm{log}{P}}$
206 205 eqcomd ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {\mathrm{e}}^{2\cdot {N}\mathrm{log}{P}}={{P}}^{2\cdot {N}}$
207 200 201 206 3brtr4d ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {\mathrm{e}}^{\mathrm{log}2\cdot {N}}\le {\mathrm{e}}^{2\cdot {N}\mathrm{log}{P}}$
208 100 relogcld ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \mathrm{log}2\cdot {N}\in ℝ$
209 124 rpred ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \mathrm{log}{P}\in ℝ$
210 106 209 remulcld ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\cdot {N}\mathrm{log}{P}\in ℝ$
211 efle ${⊢}\left(\mathrm{log}2\cdot {N}\in ℝ\wedge 2\cdot {N}\mathrm{log}{P}\in ℝ\right)\to \left(\mathrm{log}2\cdot {N}\le 2\cdot {N}\mathrm{log}{P}↔{\mathrm{e}}^{\mathrm{log}2\cdot {N}}\le {\mathrm{e}}^{2\cdot {N}\mathrm{log}{P}}\right)$
212 208 210 211 syl2anc ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left(\mathrm{log}2\cdot {N}\le 2\cdot {N}\mathrm{log}{P}↔{\mathrm{e}}^{\mathrm{log}2\cdot {N}}\le {\mathrm{e}}^{2\cdot {N}\mathrm{log}{P}}\right)$
213 207 212 mpbird ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \mathrm{log}2\cdot {N}\le 2\cdot {N}\mathrm{log}{P}$
214 208 106 124 ledivmul2d ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left(\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}\le 2\cdot {N}↔\mathrm{log}2\cdot {N}\le 2\cdot {N}\mathrm{log}{P}\right)$
215 213 214 mpbird ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}\le 2\cdot {N}$
216 192 126 106 194 215 letrd ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\le 2\cdot {N}$
217 eluz ${⊢}\left(⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\in ℤ\wedge 2\cdot {N}\in ℤ\right)\to \left(2\cdot {N}\in {ℤ}_{\ge ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋}↔⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\le 2\cdot {N}\right)$
218 127 203 217 syl2anc ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left(2\cdot {N}\in {ℤ}_{\ge ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋}↔⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\le 2\cdot {N}\right)$
219 216 218 mpbird ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to 2\cdot {N}\in {ℤ}_{\ge ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋}$
220 fzss2 ${⊢}2\cdot {N}\in {ℤ}_{\ge ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋}\to \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\subseteq \left(1\dots 2\cdot {N}\right)$
221 219 220 syl ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\subseteq \left(1\dots 2\cdot {N}\right)$
222 sumhash ${⊢}\left(\left(1\dots 2\cdot {N}\right)\in \mathrm{Fin}\wedge \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\subseteq \left(1\dots 2\cdot {N}\right)\right)\to \sum _{{k}=1}^{2\cdot {N}}if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)=\left|\left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\right|$
223 1 221 222 syl2anc ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \sum _{{k}=1}^{2\cdot {N}}if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)=\left|\left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\right|$
224 125 rprege0d ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left(\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}\in ℝ\wedge 0\le \frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}\right)$
225 flge0nn0 ${⊢}\left(\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}\in ℝ\wedge 0\le \frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}\right)\to ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\in {ℕ}_{0}$
226 hashfz1 ${⊢}⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\in {ℕ}_{0}\to \left|\left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\right|=⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋$
227 224 225 226 3syl ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left|\left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)\right|=⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋$
228 223 227 eqtr2d ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋=\sum _{{k}=1}^{2\cdot {N}}if\left({k}\in \left(1\dots ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right),1,0\right)$
229 190 191 228 3brtr4d ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)\le ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋$
230 simpr ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {P}\in ℙ$
231 nnnn0 ${⊢}{N}\in ℕ\to {N}\in {ℕ}_{0}$
232 fzctr ${⊢}{N}\in {ℕ}_{0}\to {N}\in \left(0\dots 2\cdot {N}\right)$
233 bccl2 ${⊢}{N}\in \left(0\dots 2\cdot {N}\right)\to \left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)\in ℕ$
234 231 232 233 3syl ${⊢}{N}\in ℕ\to \left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)\in ℕ$
235 234 adantr ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)\in ℕ$
236 230 235 pccld ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)\in {ℕ}_{0}$
237 236 nn0zd ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)\in ℤ$
238 efexple ${⊢}\left(\left({P}\in ℝ\wedge 1<{P}\right)\wedge {P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)\in ℤ\wedge 2\cdot {N}\in {ℝ}^{+}\right)\to \left({{P}}^{{P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)}\le 2\cdot {N}↔{P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)\le ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)$
239 90 94 237 100 238 syl211anc ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to \left({{P}}^{{P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)}\le 2\cdot {N}↔{P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)\le ⌊\frac{\mathrm{log}2\cdot {N}}{\mathrm{log}{P}}⌋\right)$
240 229 239 mpbird ${⊢}\left({N}\in ℕ\wedge {P}\in ℙ\right)\to {{P}}^{{P}\mathrm{pCnt}\left(\genfrac{}{}{0}{}{2\cdot {N}}{{N}}\right)}\le 2\cdot {N}$