Metamath Proof Explorer

Theorem chebbnd1lem1

Description: Lemma for chebbnd1 : show a lower bound on ppi ( x ) at even integers using similar techniques to those used to prove bpos . (Note that the expression K is actually equal to 2 x. N , but proving that is not necessary for the proof, and it's too much work.) The key to the proof is bposlem1 , which shows that each term in the expansion ( ( 2 x. N )C N ) = prod p e. Prime ( p ^ ( p pCnt ( ( 2 x. N )C N ) ) ) is at most 2 x. N , so that the sum really only has nonzero elements up to 2 x. N , and since each term is at most 2 x. N , after taking logs we get the inequality ppi ( 2 x. N ) x. log ( 2 x. N ) < log ( ( 2 x. N ) _C N ) , and bclbnd finishes the proof. (Contributed by Mario Carneiro, 22-Sep-2014) (Revised by Mario Carneiro, 15-Apr-2016)

Ref Expression
Hypothesis chebbnd1lem1.1 ⊢ 𝐾 = if ( ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) , ( 2 · 𝑁 ) , ( ( 2 · 𝑁 ) C 𝑁 ) )
Assertion chebbnd1lem1 ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( ( 4 ↑ 𝑁 ) / 𝑁 ) ) < ( ( π ‘ ( 2 · 𝑁 ) ) · ( log ‘ ( 2 · 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 chebbnd1lem1.1 ⊢ 𝐾 = if ( ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) , ( 2 · 𝑁 ) , ( ( 2 · 𝑁 ) C 𝑁 ) )
2 4nn ⊢ 4 ∈ ℕ
3 eluznn ⊢ ( ( 4 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 4 ) ) → 𝑁 ∈ ℕ )
4 2 3 mpan ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ℕ )
5 4 nnnn0d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ℕ0 )
6 nnexpcl ⊢ ( ( 4 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 4 ↑ 𝑁 ) ∈ ℕ )
7 2 5 6 sylancr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 4 ↑ 𝑁 ) ∈ ℕ )
8 7 nnrpd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 4 ↑ 𝑁 ) ∈ ℝ+ )
9 4 nnrpd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ℝ+ )
10 8 9 rpdivcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 4 ↑ 𝑁 ) / 𝑁 ) ∈ ℝ+ )
11 10 relogcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( ( 4 ↑ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
12 fzctr ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) )
13 5 12 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) )
14 bccl2 ⊢ ( 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
15 13 14 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
16 15 nnrpd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ+ )
17 16 relogcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℝ )
18 2z ⊢ 2 ∈ ℤ
19 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ℤ )
20 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 · 𝑁 ) ∈ ℤ )
21 18 19 20 sylancr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 · 𝑁 ) ∈ ℤ )
22 21 zred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 · 𝑁 ) ∈ ℝ )
23 ppicl ⊢ ( ( 2 · 𝑁 ) ∈ ℝ → ( π ‘ ( 2 · 𝑁 ) ) ∈ ℕ0 )
24 22 23 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( π ‘ ( 2 · 𝑁 ) ) ∈ ℕ0 )
25 24 nn0red ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( π ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
26 2nn ⊢ 2 ∈ ℕ
27 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ )
28 26 4 27 sylancr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 · 𝑁 ) ∈ ℕ )
29 28 nnrpd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 · 𝑁 ) ∈ ℝ+ )
30 29 relogcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
31 25 30 remulcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( π ‘ ( 2 · 𝑁 ) ) · ( log ‘ ( 2 · 𝑁 ) ) ) ∈ ℝ )
32 bclbnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( 2 · 𝑁 ) C 𝑁 ) )
33 logltb ⊢ ( ( ( ( 4 ↑ 𝑁 ) / 𝑁 ) ∈ ℝ+ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ+ ) → ( ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( 2 · 𝑁 ) C 𝑁 ) ↔ ( log ‘ ( ( 4 ↑ 𝑁 ) / 𝑁 ) ) < ( log ‘ ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
34 10 16 33 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( ( 4 ↑ 𝑁 ) / 𝑁 ) < ( ( 2 · 𝑁 ) C 𝑁 ) ↔ ( log ‘ ( ( 4 ↑ 𝑁 ) / 𝑁 ) ) < ( log ‘ ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
35 32 34 mpbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( ( 4 ↑ 𝑁 ) / 𝑁 ) ) < ( log ‘ ( ( 2 · 𝑁 ) C 𝑁 ) ) )
36 28 15 ifcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → if ( ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) , ( 2 · 𝑁 ) , ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ )
37 1 36 eqeltrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝐾 ∈ ℕ )
38 37 nnred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝐾 ∈ ℝ )
39 ppicl ⊢ ( 𝐾 ∈ ℝ → ( π ‘ 𝐾 ) ∈ ℕ0 )
40 38 39 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( π ‘ 𝐾 ) ∈ ℕ0 )
41 40 nn0red ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( π ‘ 𝐾 ) ∈ ℝ )
42 41 30 remulcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( π ‘ 𝐾 ) · ( log ‘ ( 2 · 𝑁 ) ) ) ∈ ℝ )
43 fzfid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 1 ... 𝐾 ) ∈ Fin )
44 inss1 ⊢ ( ( 1 ... 𝐾 ) ∩ ℙ ) ⊆ ( 1 ... 𝐾 )
45 ssfi ⊢ ( ( ( 1 ... 𝐾 ) ∈ Fin ∧ ( ( 1 ... 𝐾 ) ∩ ℙ ) ⊆ ( 1 ... 𝐾 ) ) → ( ( 1 ... 𝐾 ) ∩ ℙ ) ∈ Fin )
46 43 44 45 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 1 ... 𝐾 ) ∩ ℙ ) ∈ Fin )
47 37 nnzd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝐾 ∈ ℤ )
48 15 nnzd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℤ )
49 15 nnred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ )
50 min2 ⊢ ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ ) → if ( ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) , ( 2 · 𝑁 ) , ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
51 22 49 50 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → if ( ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) , ( 2 · 𝑁 ) , ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
52 1 51 eqbrtrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝐾 ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
53 eluz2 ⊢ ( ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ( ℤ≥ ‘ 𝐾 ) ↔ ( 𝐾 ∈ ℤ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℤ ∧ 𝐾 ≤ ( ( 2 · 𝑁 ) C 𝑁 ) ) )
54 47 48 52 53 syl3anbrc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ( ℤ≥ ‘ 𝐾 ) )
55 fzss2 ⊢ ( ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ( ℤ≥ ‘ 𝐾 ) → ( 1 ... 𝐾 ) ⊆ ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) )
56 54 55 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 1 ... 𝐾 ) ⊆ ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) )
57 56 ssrind ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 1 ... 𝐾 ) ∩ ℙ ) ⊆ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) )
58 57 sselda ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) )
59 simpr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) )
60 59 elin1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → 𝑘 ∈ ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) )
61 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) → 𝑘 ∈ ℕ )
62 60 61 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → 𝑘 ∈ ℕ )
63 59 elin2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → 𝑘 ∈ ℙ )
64 15 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ )
65 63 64 pccld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
66 62 65 nnexpcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ ℕ )
67 66 nnrpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ ℝ+ )
68 67 relogcld ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ∈ ℝ )
69 58 68 syldan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ∈ ℝ )
70 30 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( log ‘ ( 2 · 𝑁 ) ) ∈ ℝ )
71 elinel2 ⊢ ( 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) → 𝑘 ∈ ℙ )
72 bposlem1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℙ ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) )
73 4 71 72 syl2an ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) )
74 58 67 syldan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ ℝ+ )
75 74 reeflogd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ) = ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
76 29 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( 2 · 𝑁 ) ∈ ℝ+ )
77 76 reeflogd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ ( 2 · 𝑁 ) ) ) = ( 2 · 𝑁 ) )
78 73 75 77 3brtr4d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( exp ‘ ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ) ≤ ( exp ‘ ( log ‘ ( 2 · 𝑁 ) ) ) )
79 efle ⊢ ( ( ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ∈ ℝ ∧ ( log ‘ ( 2 · 𝑁 ) ) ∈ ℝ ) → ( ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ≤ ( log ‘ ( 2 · 𝑁 ) ) ↔ ( exp ‘ ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ) ≤ ( exp ‘ ( log ‘ ( 2 · 𝑁 ) ) ) ) )
80 69 70 79 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ≤ ( log ‘ ( 2 · 𝑁 ) ) ↔ ( exp ‘ ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ) ≤ ( exp ‘ ( log ‘ ( 2 · 𝑁 ) ) ) ) )
81 78 80 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ≤ ( log ‘ ( 2 · 𝑁 ) ) )
82 46 69 70 81 fsumle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → Σ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ≤ Σ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ( log ‘ ( 2 · 𝑁 ) ) )
83 68 recnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ∈ ℂ )
84 58 83 syldan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) ∈ ℂ )
85 eldifn ⊢ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) → ¬ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) )
86 85 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ¬ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) )
87 simpr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) )
88 87 eldifad ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) )
89 88 elin1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → 𝑘 ∈ ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) )
90 89 61 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → 𝑘 ∈ ℕ )
91 90 adantrr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ∈ ℕ )
92 91 nnred ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ∈ ℝ )
93 88 66 syldan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ ℕ )
94 93 nnred ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ ℝ )
95 94 adantrr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ ℝ )
96 22 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → ( 2 · 𝑁 ) ∈ ℝ )
97 91 nncnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ∈ ℂ )
98 97 exp1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → ( 𝑘 ↑ 1 ) = 𝑘 )
99 91 nnge1d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 1 ≤ 𝑘 )
100 simprr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ )
101 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
102 100 101 eleqtrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ( ℤ≥ ‘ 1 ) )
103 92 99 102 leexp2ad ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → ( 𝑘 ↑ 1 ) ≤ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
104 98 103 eqbrtrrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ≤ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
105 4 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑁 ∈ ℕ )
106 88 elin2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → 𝑘 ∈ ℙ )
107 106 adantrr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ∈ ℙ )
108 105 107 72 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) )
109 92 95 96 104 108 letrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ≤ ( 2 · 𝑁 ) )
110 elfzle2 ⊢ ( 𝑘 ∈ ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) → 𝑘 ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
111 89 110 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → 𝑘 ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
112 111 adantrr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
113 49 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ )
114 lemin ⊢ ( ( 𝑘 ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ ) → ( 𝑘 ≤ if ( ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) , ( 2 · 𝑁 ) , ( ( 2 · 𝑁 ) C 𝑁 ) ) ↔ ( 𝑘 ≤ ( 2 · 𝑁 ) ∧ 𝑘 ≤ ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
115 92 96 113 114 syl3anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → ( 𝑘 ≤ if ( ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) , ( 2 · 𝑁 ) , ( ( 2 · 𝑁 ) C 𝑁 ) ) ↔ ( 𝑘 ≤ ( 2 · 𝑁 ) ∧ 𝑘 ≤ ( ( 2 · 𝑁 ) C 𝑁 ) ) ) )
116 109 112 115 mpbir2and ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ≤ if ( ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) , ( 2 · 𝑁 ) , ( ( 2 · 𝑁 ) C 𝑁 ) ) )
117 116 1 breqtrrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ≤ 𝐾 )
118 37 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝐾 ∈ ℕ )
119 118 nnzd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝐾 ∈ ℤ )
120 fznn ⊢ ( 𝐾 ∈ ℤ → ( 𝑘 ∈ ( 1 ... 𝐾 ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾 ) ) )
121 119 120 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → ( 𝑘 ∈ ( 1 ... 𝐾 ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾 ) ) )
122 91 117 121 mpbir2and ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ∈ ( 1 ... 𝐾 ) )
123 122 107 elind ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ ( 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ) ) → 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) )
124 123 expr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ → 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) )
125 86 124 mtod ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ¬ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ )
126 88 65 syldan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 )
127 elnn0 ⊢ ( ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 ↔ ( ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ∨ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ) )
128 126 127 sylib ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ ∨ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ) )
129 128 ord ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( ¬ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ → ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 ) )
130 125 129 mpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = 0 )
131 130 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) = ( 𝑘 ↑ 0 ) )
132 90 nncnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → 𝑘 ∈ ℂ )
133 132 exp0d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( 𝑘 ↑ 0 ) = 1 )
134 131 133 eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) = 1 )
135 134 fveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) = ( log ‘ 1 ) )
136 log1 ⊢ ( log ‘ 1 ) = 0
137 135 136 eqtrdi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∖ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) ) → ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) = 0 )
138 fzfid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ Fin )
139 inss1 ⊢ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) )
140 ssfi ⊢ ( ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ Fin ∧ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ) → ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∈ Fin )
141 138 139 140 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ∈ Fin )
142 57 84 137 141 fsumss ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → Σ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) = Σ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) )
143 62 nnrpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → 𝑘 ∈ ℝ+ )
144 65 nn0zd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℤ )
145 relogexp ⊢ ( ( 𝑘 ∈ ℝ+ ∧ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℤ ) → ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) = ( ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) · ( log ‘ 𝑘 ) ) )
146 143 144 145 syl2anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) ∧ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ) → ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) = ( ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) · ( log ‘ 𝑘 ) ) )
147 146 sumeq2dv ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → Σ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) = Σ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ( ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) · ( log ‘ 𝑘 ) ) )
148 pclogsum ⊢ ( ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ → Σ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ( ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) · ( log ‘ 𝑘 ) ) = ( log ‘ ( ( 2 · 𝑁 ) C 𝑁 ) ) )
149 15 148 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → Σ 𝑘 ∈ ( ( 1 ... ( ( 2 · 𝑁 ) C 𝑁 ) ) ∩ ℙ ) ( ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) · ( log ‘ 𝑘 ) ) = ( log ‘ ( ( 2 · 𝑁 ) C 𝑁 ) ) )
150 142 147 149 3eqtrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → Σ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ( log ‘ ( 𝑘 ↑ ( 𝑘 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) = ( log ‘ ( ( 2 · 𝑁 ) C 𝑁 ) ) )
151 30 recnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( 2 · 𝑁 ) ) ∈ ℂ )
152 fsumconst ⊢ ( ( ( ( 1 ... 𝐾 ) ∩ ℙ ) ∈ Fin ∧ ( log ‘ ( 2 · 𝑁 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ( log ‘ ( 2 · 𝑁 ) ) = ( ( ♯ ‘ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) · ( log ‘ ( 2 · 𝑁 ) ) ) )
153 46 151 152 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → Σ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ( log ‘ ( 2 · 𝑁 ) ) = ( ( ♯ ‘ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) · ( log ‘ ( 2 · 𝑁 ) ) ) )
154 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
155 ppival2g ⊢ ( ( 𝐾 ∈ ℤ ∧ 2 ∈ ( ℤ≥ ‘ 1 ) ) → ( π ‘ 𝐾 ) = ( ♯ ‘ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) )
156 47 154 155 sylancl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( π ‘ 𝐾 ) = ( ♯ ‘ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) )
157 156 oveq1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( π ‘ 𝐾 ) · ( log ‘ ( 2 · 𝑁 ) ) ) = ( ( ♯ ‘ ( ( 1 ... 𝐾 ) ∩ ℙ ) ) · ( log ‘ ( 2 · 𝑁 ) ) ) )
158 153 157 eqtr4d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → Σ 𝑘 ∈ ( ( 1 ... 𝐾 ) ∩ ℙ ) ( log ‘ ( 2 · 𝑁 ) ) = ( ( π ‘ 𝐾 ) · ( log ‘ ( 2 · 𝑁 ) ) ) )
159 82 150 158 3brtr3d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( ( π ‘ 𝐾 ) · ( log ‘ ( 2 · 𝑁 ) ) ) )
160 min1 ⊢ ( ( ( 2 · 𝑁 ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ ) → if ( ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) , ( 2 · 𝑁 ) , ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( 2 · 𝑁 ) )
161 22 49 160 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → if ( ( 2 · 𝑁 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) , ( 2 · 𝑁 ) , ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( 2 · 𝑁 ) )
162 1 161 eqbrtrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝐾 ≤ ( 2 · 𝑁 ) )
163 ppiwordi ⊢ ( ( 𝐾 ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℝ ∧ 𝐾 ≤ ( 2 · 𝑁 ) ) → ( π ‘ 𝐾 ) ≤ ( π ‘ ( 2 · 𝑁 ) ) )
164 38 22 162 163 syl3anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( π ‘ 𝐾 ) ≤ ( π ‘ ( 2 · 𝑁 ) ) )
165 1red ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 1 ∈ ℝ )
166 2re ⊢ 2 ∈ ℝ
167 166 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 2 ∈ ℝ )
168 1lt2 ⊢ 1 < 2
169 168 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 1 < 2 )
170 2t1e2 ⊢ ( 2 · 1 ) = 2
171 4 nnge1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 1 ≤ 𝑁 )
172 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 𝑁 ∈ ℝ )
173 2pos ⊢ 0 < 2
174 166 173 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
175 174 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
176 lemul2 ⊢ ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) )
177 165 172 175 176 syl3anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) )
178 171 177 mpbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( 2 · 1 ) ≤ ( 2 · 𝑁 ) )
179 170 178 eqbrtrrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 2 ≤ ( 2 · 𝑁 ) )
180 165 167 22 169 179 ltletrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → 1 < ( 2 · 𝑁 ) )
181 22 180 rplogcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( 2 · 𝑁 ) ) ∈ ℝ+ )
182 41 25 181 lemul1d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( π ‘ 𝐾 ) ≤ ( π ‘ ( 2 · 𝑁 ) ) ↔ ( ( π ‘ 𝐾 ) · ( log ‘ ( 2 · 𝑁 ) ) ) ≤ ( ( π ‘ ( 2 · 𝑁 ) ) · ( log ‘ ( 2 · 𝑁 ) ) ) ) )
183 164 182 mpbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( ( π ‘ 𝐾 ) · ( log ‘ ( 2 · 𝑁 ) ) ) ≤ ( ( π ‘ ( 2 · 𝑁 ) ) · ( log ‘ ( 2 · 𝑁 ) ) ) )
184 17 42 31 159 183 letrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( ( 2 · 𝑁 ) C 𝑁 ) ) ≤ ( ( π ‘ ( 2 · 𝑁 ) ) · ( log ‘ ( 2 · 𝑁 ) ) ) )
185 11 17 31 35 184 ltletrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 4 ) → ( log ‘ ( ( 4 ↑ 𝑁 ) / 𝑁 ) ) < ( ( π ‘ ( 2 · 𝑁 ) ) · ( log ‘ ( 2 · 𝑁 ) ) ) )