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