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