Proof of Theorem knoppcnlem4
| Step | Hyp | Ref
| Expression |
| 1 | | knoppcnlem4.f |
. . . 4
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
| 2 | | knoppcnlem4.2 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 3 | | knoppcnlem4.3 |
. . . 4
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 4 | 1, 2, 3 | knoppcnlem1 36494 |
. . 3
⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) |
| 5 | 4 | fveq2d 6910 |
. 2
⊢ (𝜑 → (abs‘((𝐹‘𝐴)‘𝑀)) = (abs‘((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))) |
| 6 | | knoppcnlem4.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 7 | 6 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 8 | 7, 3 | expcld 14186 |
. . . . . 6
⊢ (𝜑 → (𝐶↑𝑀) ∈ ℂ) |
| 9 | | knoppcnlem4.t |
. . . . . . . 8
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
| 10 | | 2re 12340 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
| 11 | 10 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) |
| 12 | | knoppcnlem4.n |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 13 | | nnre 12273 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
| 14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 15 | 11, 14 | remulcld 11291 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
| 16 | 15, 3 | reexpcld 14203 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁)↑𝑀) ∈ ℝ) |
| 17 | 16, 2 | remulcld 11291 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁)↑𝑀) · 𝐴) ∈ ℝ) |
| 18 | 9, 17 | dnicld2 36474 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)) ∈ ℝ) |
| 19 | 18 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)) ∈ ℂ) |
| 20 | 8, 19 | absmuld 15493 |
. . . . 5
⊢ (𝜑 → (abs‘((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) = ((abs‘(𝐶↑𝑀)) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))) |
| 21 | 7, 3 | absexpd 15491 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐶↑𝑀)) = ((abs‘𝐶)↑𝑀)) |
| 22 | 21 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((abs‘(𝐶↑𝑀)) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) = (((abs‘𝐶)↑𝑀) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))) |
| 23 | 20, 22 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (abs‘((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) = (((abs‘𝐶)↑𝑀) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))) |
| 24 | 19 | abscld 15475 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ) |
| 25 | | 1red 11262 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
| 26 | 7 | abscld 15475 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
| 27 | 26, 3 | reexpcld 14203 |
. . . . . 6
⊢ (𝜑 → ((abs‘𝐶)↑𝑀) ∈ ℝ) |
| 28 | 7 | absge0d 15483 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (abs‘𝐶)) |
| 29 | 26, 3, 28 | expge0d 14204 |
. . . . . 6
⊢ (𝜑 → 0 ≤ ((abs‘𝐶)↑𝑀)) |
| 30 | 9 | dnival 36472 |
. . . . . . . . . 10
⊢ ((((2
· 𝑁)↑𝑀) · 𝐴) ∈ ℝ → (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)) = (abs‘((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)))) |
| 31 | 17, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)) = (abs‘((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)))) |
| 32 | 31 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) =
(abs‘(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴))))) |
| 33 | | halfre 12480 |
. . . . . . . . . . . . . 14
⊢ (1 / 2)
∈ ℝ |
| 34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
| 35 | 17, 34 | readdcld 11290 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2)) ∈
ℝ) |
| 36 | | reflcl 13836 |
. . . . . . . . . . . 12
⊢ (((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2)) ∈ ℝ →
(⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) ∈
ℝ) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) ∈
ℝ) |
| 38 | 37, 17 | resubcld 11691 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)) ∈ ℝ) |
| 39 | 38 | recnd 11289 |
. . . . . . . . 9
⊢ (𝜑 → ((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)) ∈ ℂ) |
| 40 | | absidm 15362 |
. . . . . . . . 9
⊢
(((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)) ∈ ℂ →
(abs‘(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)))) = (abs‘((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)))) |
| 41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)))) = (abs‘((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)))) |
| 42 | 32, 41 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) = (abs‘((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)))) |
| 43 | 31, 18 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ) |
| 44 | | rddif 15379 |
. . . . . . . . 9
⊢ ((((2
· 𝑁)↑𝑀) · 𝐴) ∈ ℝ →
(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴))) ≤ (1 / 2)) |
| 45 | 17, 44 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴))) ≤ (1 / 2)) |
| 46 | | halflt1 12484 |
. . . . . . . . . 10
⊢ (1 / 2)
< 1 |
| 47 | | 1re 11261 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
| 48 | 33, 47 | ltlei 11383 |
. . . . . . . . . 10
⊢ ((1 / 2)
< 1 → (1 / 2) ≤ 1) |
| 49 | 46, 48 | ax-mp 5 |
. . . . . . . . 9
⊢ (1 / 2)
≤ 1 |
| 50 | 49 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (1 / 2) ≤
1) |
| 51 | 43, 34, 25, 45, 50 | letrd 11418 |
. . . . . . 7
⊢ (𝜑 →
(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴))) ≤ 1) |
| 52 | 42, 51 | eqbrtrd 5165 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ≤ 1) |
| 53 | 24, 25, 27, 29, 52 | lemul2ad 12208 |
. . . . 5
⊢ (𝜑 → (((abs‘𝐶)↑𝑀) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) ≤ (((abs‘𝐶)↑𝑀) · 1)) |
| 54 | | ax-1rid 11225 |
. . . . . 6
⊢
(((abs‘𝐶)↑𝑀) ∈ ℝ → (((abs‘𝐶)↑𝑀) · 1) = ((abs‘𝐶)↑𝑀)) |
| 55 | 27, 54 | syl 17 |
. . . . 5
⊢ (𝜑 → (((abs‘𝐶)↑𝑀) · 1) = ((abs‘𝐶)↑𝑀)) |
| 56 | 53, 55 | breqtrd 5169 |
. . . 4
⊢ (𝜑 → (((abs‘𝐶)↑𝑀) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) ≤ ((abs‘𝐶)↑𝑀)) |
| 57 | 23, 56 | eqbrtrd 5165 |
. . 3
⊢ (𝜑 → (abs‘((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) ≤ ((abs‘𝐶)↑𝑀)) |
| 58 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚)) = (𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))) |
| 59 | | oveq2 7439 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((abs‘𝐶)↑𝑚) = ((abs‘𝐶)↑𝑀)) |
| 60 | 59 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → ((abs‘𝐶)↑𝑚) = ((abs‘𝐶)↑𝑀)) |
| 61 | 58, 60, 3, 27 | fvmptd 7023 |
. . . 4
⊢ (𝜑 → ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑀) = ((abs‘𝐶)↑𝑀)) |
| 62 | 61 | eqcomd 2743 |
. . 3
⊢ (𝜑 → ((abs‘𝐶)↑𝑀) = ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑀)) |
| 63 | 57, 62 | breqtrd 5169 |
. 2
⊢ (𝜑 → (abs‘((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) ≤ ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑀)) |
| 64 | 5, 63 | eqbrtrd 5165 |
1
⊢ (𝜑 → (abs‘((𝐹‘𝐴)‘𝑀)) ≤ ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑀)) |