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 ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( 𝑃 ↑ ( 𝑃 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) )

Proof

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