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 34410 |
. . 3
⊢ (𝜑 → ((𝐹‘𝐴)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) |
5 | 4 | fveq2d 6721 |
. 2
⊢ (𝜑 → (abs‘((𝐹‘𝐴)‘𝑀)) = (abs‘((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))) |
6 | | knoppcnlem4.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) |
7 | 6 | recnd 10861 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℂ) |
8 | 7, 3 | expcld 13716 |
. . . . . 6
⊢ (𝜑 → (𝐶↑𝑀) ∈ ℂ) |
9 | | knoppcnlem4.t |
. . . . . . . 8
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
10 | | 2re 11904 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
11 | 10 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) |
12 | | knoppcnlem4.n |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
13 | | nnre 11837 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) |
15 | 11, 14 | remulcld 10863 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
16 | 15, 3 | reexpcld 13733 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁)↑𝑀) ∈ ℝ) |
17 | 16, 2 | remulcld 10863 |
. . . . . . . 8
⊢ (𝜑 → (((2 · 𝑁)↑𝑀) · 𝐴) ∈ ℝ) |
18 | 9, 17 | dnicld2 34390 |
. . . . . . 7
⊢ (𝜑 → (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)) ∈ ℝ) |
19 | 18 | recnd 10861 |
. . . . . 6
⊢ (𝜑 → (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)) ∈ ℂ) |
20 | 8, 19 | absmuld 15018 |
. . . . 5
⊢ (𝜑 → (abs‘((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) = ((abs‘(𝐶↑𝑀)) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))) |
21 | 7, 3 | absexpd 15016 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝐶↑𝑀)) = ((abs‘𝐶)↑𝑀)) |
22 | 21 | oveq1d 7228 |
. . . . 5
⊢ (𝜑 → ((abs‘(𝐶↑𝑀)) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) = (((abs‘𝐶)↑𝑀) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))) |
23 | 20, 22 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (abs‘((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) = (((abs‘𝐶)↑𝑀) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))))) |
24 | 19 | abscld 15000 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ) |
25 | | 1red 10834 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
26 | 7 | abscld 15000 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
27 | 26, 3 | reexpcld 13733 |
. . . . . 6
⊢ (𝜑 → ((abs‘𝐶)↑𝑀) ∈ ℝ) |
28 | 7 | absge0d 15008 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (abs‘𝐶)) |
29 | 26, 3, 28 | expge0d 13734 |
. . . . . 6
⊢ (𝜑 → 0 ≤ ((abs‘𝐶)↑𝑀)) |
30 | 9 | dnival 34388 |
. . . . . . . . . 10
⊢ ((((2
· 𝑁)↑𝑀) · 𝐴) ∈ ℝ → (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)) = (abs‘((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)))) |
31 | 17, 30 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)) = (abs‘((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)))) |
32 | 31 | fveq2d 6721 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) =
(abs‘(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴))))) |
33 | | halfre 12044 |
. . . . . . . . . . . . . 14
⊢ (1 / 2)
∈ ℝ |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
35 | 17, 34 | readdcld 10862 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2)) ∈
ℝ) |
36 | | reflcl 13371 |
. . . . . . . . . . . 12
⊢ (((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2)) ∈ ℝ →
(⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) ∈
ℝ) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) ∈
ℝ) |
38 | 37, 17 | resubcld 11260 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)) ∈ ℝ) |
39 | 38 | recnd 10861 |
. . . . . . . . 9
⊢ (𝜑 → ((⌊‘((((2
· 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴)) ∈ ℂ) |
40 | | absidm 14887 |
. . . . . . . . 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 2839 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴))) ∈ ℝ) |
44 | | rddif 14904 |
. . . . . . . . 9
⊢ ((((2
· 𝑁)↑𝑀) · 𝐴) ∈ ℝ →
(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴))) ≤ (1 / 2)) |
45 | 17, 44 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴))) ≤ (1 / 2)) |
46 | | halflt1 12048 |
. . . . . . . . . 10
⊢ (1 / 2)
< 1 |
47 | | 1re 10833 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
48 | 33, 47 | ltlei 10954 |
. . . . . . . . . 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 10989 |
. . . . . . 7
⊢ (𝜑 →
(abs‘((⌊‘((((2 · 𝑁)↑𝑀) · 𝐴) + (1 / 2))) − (((2 · 𝑁)↑𝑀) · 𝐴))) ≤ 1) |
52 | 42, 51 | eqbrtrd 5075 |
. . . . . 6
⊢ (𝜑 → (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴))) ≤ 1) |
53 | 24, 25, 27, 29, 52 | lemul2ad 11772 |
. . . . 5
⊢ (𝜑 → (((abs‘𝐶)↑𝑀) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) ≤ (((abs‘𝐶)↑𝑀) · 1)) |
54 | | ax-1rid 10799 |
. . . . . 6
⊢
(((abs‘𝐶)↑𝑀) ∈ ℝ → (((abs‘𝐶)↑𝑀) · 1) = ((abs‘𝐶)↑𝑀)) |
55 | 27, 54 | syl 17 |
. . . . 5
⊢ (𝜑 → (((abs‘𝐶)↑𝑀) · 1) = ((abs‘𝐶)↑𝑀)) |
56 | 53, 55 | breqtrd 5079 |
. . . 4
⊢ (𝜑 → (((abs‘𝐶)↑𝑀) · (abs‘(𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) ≤ ((abs‘𝐶)↑𝑀)) |
57 | 23, 56 | eqbrtrd 5075 |
. . 3
⊢ (𝜑 → (abs‘((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) ≤ ((abs‘𝐶)↑𝑀)) |
58 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚)) = (𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))) |
59 | | oveq2 7221 |
. . . . . 6
⊢ (𝑚 = 𝑀 → ((abs‘𝐶)↑𝑚) = ((abs‘𝐶)↑𝑀)) |
60 | 59 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 = 𝑀) → ((abs‘𝐶)↑𝑚) = ((abs‘𝐶)↑𝑀)) |
61 | 58, 60, 3, 27 | fvmptd 6825 |
. . . 4
⊢ (𝜑 → ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑀) = ((abs‘𝐶)↑𝑀)) |
62 | 61 | eqcomd 2743 |
. . 3
⊢ (𝜑 → ((abs‘𝐶)↑𝑀) = ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑀)) |
63 | 57, 62 | breqtrd 5079 |
. 2
⊢ (𝜑 → (abs‘((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝐴)))) ≤ ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑀)) |
64 | 5, 63 | eqbrtrd 5075 |
1
⊢ (𝜑 → (abs‘((𝐹‘𝐴)‘𝑀)) ≤ ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑀)) |