Step |
Hyp |
Ref |
Expression |
1 |
|
bpos.1 |
⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 5 ) ) |
2 |
|
bpos.2 |
⊢ ( 𝜑 → ¬ ∃ 𝑝 ∈ ℙ ( 𝑁 < 𝑝 ∧ 𝑝 ≤ ( 2 · 𝑁 ) ) ) |
3 |
|
bpos.3 |
⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) ) |
4 |
|
bpos.4 |
⊢ 𝐾 = ( ⌊ ‘ ( ( 2 · 𝑁 ) / 3 ) ) |
5 |
|
bpos.5 |
⊢ 𝑀 = ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) |
6 |
|
id |
⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ℙ ) |
7 |
|
5nn |
⊢ 5 ∈ ℕ |
8 |
|
eluznn |
⊢ ( ( 5 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 5 ) ) → 𝑁 ∈ ℕ ) |
9 |
7 1 8
|
sylancr |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
10 |
9
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
11 |
|
fzctr |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) |
12 |
|
bccl2 |
⊢ ( 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ ) |
13 |
10 11 12
|
3syl |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ ) |
14 |
|
pccl |
⊢ ( ( 𝑛 ∈ ℙ ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 ) |
15 |
6 13 14
|
syl2anr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℙ ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 ) |
16 |
15
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑛 ∈ ℙ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ∈ ℕ0 ) |
17 |
3 16
|
pcmptcl |
⊢ ( 𝜑 → ( 𝐹 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ) ) |
18 |
17
|
simprd |
⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ) |
19 |
|
3nn |
⊢ 3 ∈ ℕ |
20 |
|
2z |
⊢ 2 ∈ ℤ |
21 |
9
|
nnzd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
22 |
|
zmulcl |
⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 · 𝑁 ) ∈ ℤ ) |
23 |
20 21 22
|
sylancr |
⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℤ ) |
24 |
23
|
zred |
⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ ) |
25 |
|
2nn |
⊢ 2 ∈ ℕ |
26 |
|
nnmulcl |
⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ ) |
27 |
25 9 26
|
sylancr |
⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ ) |
28 |
27
|
nnrpd |
⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ+ ) |
29 |
28
|
rpge0d |
⊢ ( 𝜑 → 0 ≤ ( 2 · 𝑁 ) ) |
30 |
24 29
|
resqrtcld |
⊢ ( 𝜑 → ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ) |
31 |
30
|
flcld |
⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℤ ) |
32 |
|
sqrt9 |
⊢ ( √ ‘ 9 ) = 3 |
33 |
|
9re |
⊢ 9 ∈ ℝ |
34 |
33
|
a1i |
⊢ ( 𝜑 → 9 ∈ ℝ ) |
35 |
|
10re |
⊢ ; 1 0 ∈ ℝ |
36 |
35
|
a1i |
⊢ ( 𝜑 → ; 1 0 ∈ ℝ ) |
37 |
|
lep1 |
⊢ ( 9 ∈ ℝ → 9 ≤ ( 9 + 1 ) ) |
38 |
33 37
|
ax-mp |
⊢ 9 ≤ ( 9 + 1 ) |
39 |
|
9p1e10 |
⊢ ( 9 + 1 ) = ; 1 0 |
40 |
38 39
|
breqtri |
⊢ 9 ≤ ; 1 0 |
41 |
40
|
a1i |
⊢ ( 𝜑 → 9 ≤ ; 1 0 ) |
42 |
|
5cn |
⊢ 5 ∈ ℂ |
43 |
|
2cn |
⊢ 2 ∈ ℂ |
44 |
|
5t2e10 |
⊢ ( 5 · 2 ) = ; 1 0 |
45 |
42 43 44
|
mulcomli |
⊢ ( 2 · 5 ) = ; 1 0 |
46 |
|
eluzle |
⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → 5 ≤ 𝑁 ) |
47 |
1 46
|
syl |
⊢ ( 𝜑 → 5 ≤ 𝑁 ) |
48 |
9
|
nnred |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
49 |
|
5re |
⊢ 5 ∈ ℝ |
50 |
|
2re |
⊢ 2 ∈ ℝ |
51 |
|
2pos |
⊢ 0 < 2 |
52 |
50 51
|
pm3.2i |
⊢ ( 2 ∈ ℝ ∧ 0 < 2 ) |
53 |
|
lemul2 |
⊢ ( ( 5 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) ) |
54 |
49 52 53
|
mp3an13 |
⊢ ( 𝑁 ∈ ℝ → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) ) |
55 |
48 54
|
syl |
⊢ ( 𝜑 → ( 5 ≤ 𝑁 ↔ ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) ) |
56 |
47 55
|
mpbid |
⊢ ( 𝜑 → ( 2 · 5 ) ≤ ( 2 · 𝑁 ) ) |
57 |
45 56
|
eqbrtrrid |
⊢ ( 𝜑 → ; 1 0 ≤ ( 2 · 𝑁 ) ) |
58 |
34 36 24 41 57
|
letrd |
⊢ ( 𝜑 → 9 ≤ ( 2 · 𝑁 ) ) |
59 |
|
0re |
⊢ 0 ∈ ℝ |
60 |
|
9pos |
⊢ 0 < 9 |
61 |
59 33 60
|
ltleii |
⊢ 0 ≤ 9 |
62 |
33 61
|
pm3.2i |
⊢ ( 9 ∈ ℝ ∧ 0 ≤ 9 ) |
63 |
24 29
|
jca |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) ) |
64 |
|
sqrtle |
⊢ ( ( ( 9 ∈ ℝ ∧ 0 ≤ 9 ) ∧ ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 · 𝑁 ) ) ) → ( 9 ≤ ( 2 · 𝑁 ) ↔ ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) ) |
65 |
62 63 64
|
sylancr |
⊢ ( 𝜑 → ( 9 ≤ ( 2 · 𝑁 ) ↔ ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) ) |
66 |
58 65
|
mpbid |
⊢ ( 𝜑 → ( √ ‘ 9 ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) |
67 |
32 66
|
eqbrtrrid |
⊢ ( 𝜑 → 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) |
68 |
|
3z |
⊢ 3 ∈ ℤ |
69 |
|
flge |
⊢ ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 3 ∈ ℤ ) → ( 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) |
70 |
30 68 69
|
sylancl |
⊢ ( 𝜑 → ( 3 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) |
71 |
67 70
|
mpbid |
⊢ ( 𝜑 → 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) |
72 |
68
|
eluz1i |
⊢ ( ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( ℤ≥ ‘ 3 ) ↔ ( ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ℤ ∧ 3 ≤ ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ) ) |
73 |
31 71 72
|
sylanbrc |
⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ∈ ( ℤ≥ ‘ 3 ) ) |
74 |
5 73
|
eqeltrid |
⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 3 ) ) |
75 |
|
eluznn |
⊢ ( ( 3 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑀 ∈ ℕ ) |
76 |
19 74 75
|
sylancr |
⊢ ( 𝜑 → 𝑀 ∈ ℕ ) |
77 |
18 76
|
ffvelrnd |
⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℕ ) |
78 |
77
|
nnred |
⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℝ ) |
79 |
76
|
nnred |
⊢ ( 𝜑 → 𝑀 ∈ ℝ ) |
80 |
|
ppicl |
⊢ ( 𝑀 ∈ ℝ → ( π ‘ 𝑀 ) ∈ ℕ0 ) |
81 |
79 80
|
syl |
⊢ ( 𝜑 → ( π ‘ 𝑀 ) ∈ ℕ0 ) |
82 |
27 81
|
nnexpcld |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ∈ ℕ ) |
83 |
82
|
nnred |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ∈ ℝ ) |
84 |
|
nndivre |
⊢ ( ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ 3 ∈ ℕ ) → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ ) |
85 |
30 19 84
|
sylancl |
⊢ ( 𝜑 → ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ ) |
86 |
|
readdcl |
⊢ ( ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℝ ) |
87 |
85 50 86
|
sylancl |
⊢ ( 𝜑 → ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ∈ ℝ ) |
88 |
24 29 87
|
recxpcld |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ∈ ℝ ) |
89 |
|
fveq2 |
⊢ ( 𝑥 = 1 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 1 ) ) |
90 |
|
fveq2 |
⊢ ( 𝑥 = 1 → ( π ‘ 𝑥 ) = ( π ‘ 1 ) ) |
91 |
|
ppi1 |
⊢ ( π ‘ 1 ) = 0 |
92 |
90 91
|
eqtrdi |
⊢ ( 𝑥 = 1 → ( π ‘ 𝑥 ) = 0 ) |
93 |
92
|
oveq2d |
⊢ ( 𝑥 = 1 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ 0 ) ) |
94 |
89 93
|
breq12d |
⊢ ( 𝑥 = 1 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ ( ( 2 · 𝑁 ) ↑ 0 ) ) ) |
95 |
94
|
imbi2d |
⊢ ( 𝑥 = 1 → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ ( ( 2 · 𝑁 ) ↑ 0 ) ) ) ) |
96 |
|
fveq2 |
⊢ ( 𝑥 = 𝑘 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) |
97 |
|
fveq2 |
⊢ ( 𝑥 = 𝑘 → ( π ‘ 𝑥 ) = ( π ‘ 𝑘 ) ) |
98 |
97
|
oveq2d |
⊢ ( 𝑥 = 𝑘 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ) |
99 |
96 98
|
breq12d |
⊢ ( 𝑥 = 𝑘 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ) ) |
100 |
99
|
imbi2d |
⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ) ) ) |
101 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ) |
102 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( π ‘ 𝑥 ) = ( π ‘ ( 𝑘 + 1 ) ) ) |
103 |
102
|
oveq2d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) |
104 |
101 103
|
breq12d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) |
105 |
104
|
imbi2d |
⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) ) |
106 |
|
fveq2 |
⊢ ( 𝑥 = 𝑀 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) |
107 |
|
fveq2 |
⊢ ( 𝑥 = 𝑀 → ( π ‘ 𝑥 ) = ( π ‘ 𝑀 ) ) |
108 |
107
|
oveq2d |
⊢ ( 𝑥 = 𝑀 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ) |
109 |
106 108
|
breq12d |
⊢ ( 𝑥 = 𝑀 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ) ) |
110 |
109
|
imbi2d |
⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑥 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ) ) ) |
111 |
|
1z |
⊢ 1 ∈ ℤ |
112 |
|
seq1 |
⊢ ( 1 ∈ ℤ → ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) ) |
113 |
111 112
|
ax-mp |
⊢ ( seq 1 ( · , 𝐹 ) ‘ 1 ) = ( 𝐹 ‘ 1 ) |
114 |
|
1nn |
⊢ 1 ∈ ℕ |
115 |
|
1nprm |
⊢ ¬ 1 ∈ ℙ |
116 |
|
eleq1 |
⊢ ( 𝑛 = 1 → ( 𝑛 ∈ ℙ ↔ 1 ∈ ℙ ) ) |
117 |
115 116
|
mtbiri |
⊢ ( 𝑛 = 1 → ¬ 𝑛 ∈ ℙ ) |
118 |
117
|
iffalsed |
⊢ ( 𝑛 = 1 → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = 1 ) |
119 |
|
1ex |
⊢ 1 ∈ V |
120 |
118 3 119
|
fvmpt |
⊢ ( 1 ∈ ℕ → ( 𝐹 ‘ 1 ) = 1 ) |
121 |
114 120
|
ax-mp |
⊢ ( 𝐹 ‘ 1 ) = 1 |
122 |
113 121
|
eqtri |
⊢ ( seq 1 ( · , 𝐹 ) ‘ 1 ) = 1 |
123 |
|
1le1 |
⊢ 1 ≤ 1 |
124 |
122 123
|
eqbrtri |
⊢ ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ 1 |
125 |
23
|
zcnd |
⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℂ ) |
126 |
125
|
exp0d |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 0 ) = 1 ) |
127 |
124 126
|
breqtrrid |
⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 1 ) ≤ ( ( 2 · 𝑁 ) ↑ 0 ) ) |
128 |
18
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ ) |
129 |
128
|
nnred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ) |
130 |
129
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ) |
131 |
27
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℕ ) |
132 |
|
nnre |
⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ ) |
133 |
132
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → 𝑘 ∈ ℝ ) |
134 |
|
ppicl |
⊢ ( 𝑘 ∈ ℝ → ( π ‘ 𝑘 ) ∈ ℕ0 ) |
135 |
133 134
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ 𝑘 ) ∈ ℕ0 ) |
136 |
131 135
|
nnexpcld |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ∈ ℕ ) |
137 |
136
|
nnred |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ∈ ℝ ) |
138 |
|
nnre |
⊢ ( ( 2 · 𝑁 ) ∈ ℕ → ( 2 · 𝑁 ) ∈ ℝ ) |
139 |
|
nngt0 |
⊢ ( ( 2 · 𝑁 ) ∈ ℕ → 0 < ( 2 · 𝑁 ) ) |
140 |
138 139
|
jca |
⊢ ( ( 2 · 𝑁 ) ∈ ℕ → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) ) |
141 |
27 140
|
syl |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) ) |
142 |
141
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) ) |
143 |
|
lemul1 |
⊢ ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) ∈ ℝ ∧ 0 < ( 2 · 𝑁 ) ) ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) · ( 2 · 𝑁 ) ) ) ) |
144 |
130 137 142 143
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) · ( 2 · 𝑁 ) ) ) ) |
145 |
|
nnz |
⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ ) |
146 |
145
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℤ ) |
147 |
|
ppiprm |
⊢ ( ( 𝑘 ∈ ℤ ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( ( π ‘ 𝑘 ) + 1 ) ) |
148 |
146 147
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( ( π ‘ 𝑘 ) + 1 ) ) |
149 |
148
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) = ( ( 2 · 𝑁 ) ↑ ( ( π ‘ 𝑘 ) + 1 ) ) ) |
150 |
125
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℂ ) |
151 |
150 135
|
expp1d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( ( π ‘ 𝑘 ) + 1 ) ) = ( ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) · ( 2 · 𝑁 ) ) ) |
152 |
149 151
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) = ( ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) · ( 2 · 𝑁 ) ) ) |
153 |
152
|
breq2d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) · ( 2 · 𝑁 ) ) ) ) |
154 |
144 153
|
bitr4d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) |
155 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ ) |
156 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
157 |
155 156
|
eleqtrdi |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) |
158 |
|
seqp1 |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) |
159 |
157 158
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) |
160 |
159
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) |
161 |
|
peano2nn |
⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ ) |
162 |
161
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ ) |
163 |
|
eleq1 |
⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 ∈ ℙ ↔ ( 𝑘 + 1 ) ∈ ℙ ) ) |
164 |
|
id |
⊢ ( 𝑛 = ( 𝑘 + 1 ) → 𝑛 = ( 𝑘 + 1 ) ) |
165 |
|
oveq1 |
⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) = ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) |
166 |
164 165
|
oveq12d |
⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) = ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) |
167 |
163 166
|
ifbieq1d |
⊢ ( 𝑛 = ( 𝑘 + 1 ) → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) ) |
168 |
|
ovex |
⊢ ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ∈ V |
169 |
168 119
|
ifex |
⊢ if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) ∈ V |
170 |
167 3 169
|
fvmpt |
⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) ) |
171 |
162 170
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) ) |
172 |
|
iftrue |
⊢ ( ( 𝑘 + 1 ) ∈ ℙ → if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) |
173 |
171 172
|
sylan9eq |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ) |
174 |
9
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑁 ∈ ℕ ) |
175 |
|
bposlem1 |
⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) ) |
176 |
174 175
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) ≤ ( 2 · 𝑁 ) ) |
177 |
173 176
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 2 · 𝑁 ) ) |
178 |
17
|
simpld |
⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℕ ) |
179 |
|
ffvelrn |
⊢ ( ( 𝐹 : ℕ ⟶ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℕ ) |
180 |
178 161 179
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℕ ) |
181 |
180
|
nnred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) |
182 |
181
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) |
183 |
24
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( 2 · 𝑁 ) ∈ ℝ ) |
184 |
|
nnre |
⊢ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ) |
185 |
|
nngt0 |
⊢ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ → 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) |
186 |
184 185
|
jca |
⊢ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) ) |
187 |
128 186
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) ) |
188 |
187
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) ) |
189 |
|
lemul2 |
⊢ ( ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( 2 · 𝑁 ) ∈ ℝ ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℝ ∧ 0 < ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 2 · 𝑁 ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ) ) |
190 |
182 183 188 189
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 2 · 𝑁 ) ↔ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ) ) |
191 |
177 190
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ) |
192 |
160 191
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ) |
193 |
|
ffvelrn |
⊢ ( ( seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℕ ) |
194 |
18 161 193
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℕ ) |
195 |
194
|
nnred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ ) |
196 |
27
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑁 ) ∈ ℕ ) |
197 |
128 196
|
nnmulcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∈ ℕ ) |
198 |
197
|
nnred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∈ ℝ ) |
199 |
162
|
nnred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℝ ) |
200 |
|
ppicl |
⊢ ( ( 𝑘 + 1 ) ∈ ℝ → ( π ‘ ( 𝑘 + 1 ) ) ∈ ℕ0 ) |
201 |
199 200
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( π ‘ ( 𝑘 + 1 ) ) ∈ ℕ0 ) |
202 |
196 201
|
nnexpcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ∈ ℕ ) |
203 |
202
|
nnred |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ ) |
204 |
|
letr |
⊢ ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ∈ ℝ ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∈ ℝ ∧ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ∈ ℝ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) |
205 |
195 198 203 204
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) |
206 |
205
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) |
207 |
192 206
|
mpand |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 2 · 𝑁 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) |
208 |
154 207
|
sylbid |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) |
209 |
159
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) |
210 |
|
iffalse |
⊢ ( ¬ ( 𝑘 + 1 ) ∈ ℙ → if ( ( 𝑘 + 1 ) ∈ ℙ , ( ( 𝑘 + 1 ) ↑ ( ( 𝑘 + 1 ) pCnt ( ( 2 · 𝑁 ) C 𝑁 ) ) ) , 1 ) = 1 ) |
211 |
171 210
|
sylan9eq |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = 1 ) |
212 |
211
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) = ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · 1 ) ) |
213 |
128
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℕ ) |
214 |
213
|
nncnd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ∈ ℂ ) |
215 |
214
|
mulid1d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) · 1 ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) |
216 |
209 212 215
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) = ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ) |
217 |
|
ppinprm |
⊢ ( ( 𝑘 ∈ ℤ ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( π ‘ 𝑘 ) ) |
218 |
146 217
|
sylan |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( π ‘ ( 𝑘 + 1 ) ) = ( π ‘ 𝑘 ) ) |
219 |
218
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ) |
220 |
216 219
|
breq12d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ↔ ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ) ) |
221 |
220
|
biimprd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ¬ ( 𝑘 + 1 ) ∈ ℙ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) |
222 |
208 221
|
pm2.61dan |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) |
223 |
222
|
expcom |
⊢ ( 𝑘 ∈ ℕ → ( 𝜑 → ( ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) ) |
224 |
223
|
a2d |
⊢ ( 𝑘 ∈ ℕ → ( ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑘 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑘 ) ) ) → ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ ( 𝑘 + 1 ) ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ ( 𝑘 + 1 ) ) ) ) ) ) |
225 |
95 100 105 110 127 224
|
nnind |
⊢ ( 𝑀 ∈ ℕ → ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ) ) |
226 |
76 225
|
mpcom |
⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ) |
227 |
|
cxpexp |
⊢ ( ( ( 2 · 𝑁 ) ∈ ℂ ∧ ( π ‘ 𝑀 ) ∈ ℕ0 ) → ( ( 2 · 𝑁 ) ↑𝑐 ( π ‘ 𝑀 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ) |
228 |
125 81 227
|
syl2anc |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( π ‘ 𝑀 ) ) = ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ) |
229 |
81
|
nn0red |
⊢ ( 𝜑 → ( π ‘ 𝑀 ) ∈ ℝ ) |
230 |
|
nndivre |
⊢ ( ( 𝑀 ∈ ℝ ∧ 3 ∈ ℕ ) → ( 𝑀 / 3 ) ∈ ℝ ) |
231 |
79 19 230
|
sylancl |
⊢ ( 𝜑 → ( 𝑀 / 3 ) ∈ ℝ ) |
232 |
|
readdcl |
⊢ ( ( ( 𝑀 / 3 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( 𝑀 / 3 ) + 2 ) ∈ ℝ ) |
233 |
231 50 232
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑀 / 3 ) + 2 ) ∈ ℝ ) |
234 |
76
|
nnnn0d |
⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) |
235 |
234
|
nn0ge0d |
⊢ ( 𝜑 → 0 ≤ 𝑀 ) |
236 |
|
ppiub |
⊢ ( ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) → ( π ‘ 𝑀 ) ≤ ( ( 𝑀 / 3 ) + 2 ) ) |
237 |
79 235 236
|
syl2anc |
⊢ ( 𝜑 → ( π ‘ 𝑀 ) ≤ ( ( 𝑀 / 3 ) + 2 ) ) |
238 |
50
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℝ ) |
239 |
|
flle |
⊢ ( ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) |
240 |
30 239
|
syl |
⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ ( 2 · 𝑁 ) ) ) ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) |
241 |
5 240
|
eqbrtrid |
⊢ ( 𝜑 → 𝑀 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ) |
242 |
|
3re |
⊢ 3 ∈ ℝ |
243 |
|
3pos |
⊢ 0 < 3 |
244 |
242 243
|
pm3.2i |
⊢ ( 3 ∈ ℝ ∧ 0 < 3 ) |
245 |
244
|
a1i |
⊢ ( 𝜑 → ( 3 ∈ ℝ ∧ 0 < 3 ) ) |
246 |
|
lediv1 |
⊢ ( ( 𝑀 ∈ ℝ ∧ ( √ ‘ ( 2 · 𝑁 ) ) ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( 𝑀 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ ( 𝑀 / 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ) ) |
247 |
79 30 245 246
|
syl3anc |
⊢ ( 𝜑 → ( 𝑀 ≤ ( √ ‘ ( 2 · 𝑁 ) ) ↔ ( 𝑀 / 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ) ) |
248 |
241 247
|
mpbid |
⊢ ( 𝜑 → ( 𝑀 / 3 ) ≤ ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) ) |
249 |
231 85 238 248
|
leadd1dd |
⊢ ( 𝜑 → ( ( 𝑀 / 3 ) + 2 ) ≤ ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) |
250 |
229 233 87 237 249
|
letrd |
⊢ ( 𝜑 → ( π ‘ 𝑀 ) ≤ ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) |
251 |
|
2t1e2 |
⊢ ( 2 · 1 ) = 2 |
252 |
9
|
nnge1d |
⊢ ( 𝜑 → 1 ≤ 𝑁 ) |
253 |
|
1re |
⊢ 1 ∈ ℝ |
254 |
|
lemul2 |
⊢ ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) ) |
255 |
253 52 254
|
mp3an13 |
⊢ ( 𝑁 ∈ ℝ → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) ) |
256 |
48 255
|
syl |
⊢ ( 𝜑 → ( 1 ≤ 𝑁 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) ) |
257 |
252 256
|
mpbid |
⊢ ( 𝜑 → ( 2 · 1 ) ≤ ( 2 · 𝑁 ) ) |
258 |
251 257
|
eqbrtrrid |
⊢ ( 𝜑 → 2 ≤ ( 2 · 𝑁 ) ) |
259 |
20
|
eluz1i |
⊢ ( ( 2 · 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( 2 · 𝑁 ) ∈ ℤ ∧ 2 ≤ ( 2 · 𝑁 ) ) ) |
260 |
23 258 259
|
sylanbrc |
⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) ) |
261 |
|
eluz2gt1 |
⊢ ( ( 2 · 𝑁 ) ∈ ( ℤ≥ ‘ 2 ) → 1 < ( 2 · 𝑁 ) ) |
262 |
260 261
|
syl |
⊢ ( 𝜑 → 1 < ( 2 · 𝑁 ) ) |
263 |
24 262 229 87
|
cxpled |
⊢ ( 𝜑 → ( ( π ‘ 𝑀 ) ≤ ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ↔ ( ( 2 · 𝑁 ) ↑𝑐 ( π ‘ 𝑀 ) ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ) ) |
264 |
250 263
|
mpbid |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑𝑐 ( π ‘ 𝑀 ) ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ) |
265 |
228 264
|
eqbrtrrd |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ ( π ‘ 𝑀 ) ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ) |
266 |
78 83 88 226 265
|
letrd |
⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≤ ( ( 2 · 𝑁 ) ↑𝑐 ( ( ( √ ‘ ( 2 · 𝑁 ) ) / 3 ) + 2 ) ) ) |