Step |
Hyp |
Ref |
Expression |
1 |
|
knoppcnlem2.t |
⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) ) |
2 |
|
knoppcnlem2.n |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
3 |
|
knoppcnlem2.1 |
⊢ ( 𝜑 → 𝐶 ∈ ℝ ) |
4 |
|
knoppcnlem2.2 |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
5 |
|
knoppcnlem2.3 |
⊢ ( 𝜑 → 𝑀 ∈ ℕ0 ) |
6 |
3 5
|
reexpcld |
⊢ ( 𝜑 → ( 𝐶 ↑ 𝑀 ) ∈ ℝ ) |
7 |
|
2re |
⊢ 2 ∈ ℝ |
8 |
7
|
a1i |
⊢ ( 𝜑 → 2 ∈ ℝ ) |
9 |
|
nnre |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ ) |
10 |
2 9
|
syl |
⊢ ( 𝜑 → 𝑁 ∈ ℝ ) |
11 |
8 10
|
remulcld |
⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ ) |
12 |
11 5
|
reexpcld |
⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝑀 ) ∈ ℝ ) |
13 |
12 4
|
remulcld |
⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ∈ ℝ ) |
14 |
1 13
|
dnicld2 |
⊢ ( 𝜑 → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ∈ ℝ ) |
15 |
6 14
|
remulcld |
⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ∈ ℝ ) |