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 · 𝑁 ) )