Theorem knoppcnlem3

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

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

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem3.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppcnlem3.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppcnlem3.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		knoppcnlem3.1	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
5		knoppcnlem3.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6		knoppcnlem3.3	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
7	2 5 6	knoppcnlem1	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑀 ) = ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) )
8	1 3 4 5 6	knoppcnlem2	⊢ ( 𝜑 → ( ( 𝐶 ↑ 𝑀 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑀 ) · 𝐴 ) ) ) ∈ ℝ )
9	7 8	eqeltrd	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ‘ 𝑀 ) ∈ ℝ )