Metamath Proof Explorer

Theorem knoppcnlem4

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppcnlem4.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
knoppcnlem4.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
knoppcnlem4.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
knoppcnlem4.1 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
knoppcnlem4.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
knoppcnlem4.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
Assertion knoppcnlem4 ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑀 ) ) ≤ ( ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 knoppcnlem4.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 knoppcnlem4.f ⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3 knoppcnlem4.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 knoppcnlem4.1 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5 knoppcnlem4.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6 knoppcnlem4.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
7 2 5 6 knoppcnlem1 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑀 ) = ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )
8 7 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑀 ) ) = ( abs ‘ ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) )
9 4 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
10 9 6 expcld ⊢ ( 𝜑 → ( 𝐶 ↑ 𝑀 ) ∈ ℂ )
11 2re ⊢ 2 ∈ ℝ
12 11 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
13 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
14 3 13 syl ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
15 12 14 remulcld ⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℝ )
16 15 6 reexpcld ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 𝑀 ) ∈ ℝ )
17 16 5 remulcld ⊢ ( 𝜑 → ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ∈ ℝ )
18 1 17 dnicld2 ⊢ ( 𝜑 → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ∈ ℝ )
19 18 recnd ⊢ ( 𝜑 → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ∈ ℂ )
20 10 19 absmuld ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) = ( ( abs ‘ ( 𝐶 ↑ 𝑀 ) ) · ( abs ‘ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) )
21 9 6 absexpd ⊢ ( 𝜑 → ( abs ‘ ( 𝐶 ↑ 𝑀 ) ) = ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) )
22 21 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐶 ↑ 𝑀 ) ) · ( abs ‘ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) · ( abs ‘ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) )
23 20 22 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) = ( ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) · ( abs ‘ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) )
24 19 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ∈ ℝ )
25 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
26 9 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
27 26 6 reexpcld ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) ∈ ℝ )
28 9 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝐶 ) )
29 26 6 28 expge0d ⊢ ( 𝜑 → 0 ≤ ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) )
30 1 dnival ⊢ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ∈ ℝ → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) = ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )
31 17 30 syl ⊢ ( 𝜑 → ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) = ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )
32 31 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) = ( abs ‘ ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) )
33 halfre ⊢ ( 1 / 2 ) ∈ ℝ
34 33 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
35 17 34 readdcld ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ∈ ℝ )
36 reflcl ⊢ ( ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) ∈ ℝ )
37 35 36 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) ∈ ℝ )
38 37 17 resubcld ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ∈ ℝ )
39 38 recnd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ∈ ℂ )
40 absidm ⊢ ( ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ∈ ℂ → ( abs ‘ ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) = ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )
41 39 40 syl ⊢ ( 𝜑 → ( abs ‘ ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) = ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )
42 32 41 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) = ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )
43 31 18 eqeltrrd ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ∈ ℝ )
44 rddif ⊢ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ∈ ℝ → ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ≤ ( 1 / 2 ) )
45 17 44 syl ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ≤ ( 1 / 2 ) )
46 halflt1 ⊢ ( 1 / 2 ) < 1
47 1re ⊢ 1 ∈ ℝ
48 33 47 ltlei ⊢ ( ( 1 / 2 ) < 1 → ( 1 / 2 ) ≤ 1 )
49 46 48 ax-mp ⊢ ( 1 / 2 ) ≤ 1
50 49 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ≤ 1 )
51 43 34 25 45 50 letrd ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) + ( 1 / 2 ) ) ) − ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ≤ 1 )
52 42 51 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ≤ 1 )
53 24 25 27 29 52 lemul2ad ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) · ( abs ‘ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) ≤ ( ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) · 1 ) )
54 ax-1rid ⊢ ( ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) ∈ ℝ → ( ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) · 1 ) = ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) )
55 27 54 syl ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) · 1 ) = ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) )
56 53 55 breqtrd ⊢ ( 𝜑 → ( ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) · ( abs ‘ ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) ≤ ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) )
57 23 56 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) ≤ ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) )
58 eqidd ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) = ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) )
59 oveq2 ⊢ ( 𝑚 = 𝑀 → ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) = ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) )
60 59 adantl ⊢ ( ( 𝜑 ∧ 𝑚 = 𝑀 ) → ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) = ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) )
61 58 60 6 27 fvmptd ⊢ ( 𝜑 → ( ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ‘ 𝑀 ) = ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) )
62 61 eqcomd ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) ↑ 𝑀 ) = ( ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ‘ 𝑀 ) )
63 57 62 breqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ) ≤ ( ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ‘ 𝑀 ) )
64 8 63 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑀 ) ) ≤ ( ( 𝑚 ∈ ℕ0 ↦ ( ( abs ‘ 𝐶 ) ↑ 𝑚 ) ) ‘ 𝑀 ) )