Theorem knoppcld

Description: Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021)

	Ref	Expression
Hypotheses	knoppcld.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	knoppcld.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	knoppcld.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
	knoppcld.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	knoppcld.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	knoppcld.1	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	knoppcld.2	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
Assertion	knoppcld	⊢ ( 𝜑 → ( 𝑊 ‘ 𝐴 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		knoppcld.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppcld.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppcld.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4		knoppcld.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5		knoppcld.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		knoppcld.1	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
7		knoppcld.2	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
8	1 2 3 5 6 7	knoppcn	⊢ ( 𝜑 → 𝑊 ∈ ( ℝ –cn→ ℂ ) )
9		cncff	⊢ ( 𝑊 ∈ ( ℝ –cn→ ℂ ) → 𝑊 : ℝ ⟶ ℂ )
10	8 9	syl	⊢ ( 𝜑 → 𝑊 : ℝ ⟶ ℂ )
11	10 4	ffvelrnd	⊢ ( 𝜑 → ( 𝑊 ‘ 𝐴 ) ∈ ℂ )