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 ‘ 𝐶 ) ↑ 𝑚 ) ) ‘ 𝑀 ) )