Theorem knoppcld

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

	Ref	Expression
Hypotheses	knoppcld.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	knoppcld.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
	knoppcld.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
	knoppcld.a	$$⊢\phi \to A\in ℝ$$
	knoppcld.n	$$⊢\phi \to N\in \mathbb{N}$$
	knoppcld.1	$$⊢\phi \to C\in ℝ$$
	knoppcld.2	$$⊢\phi \to \left|C\right|<1$$
Assertion	knoppcld	$$⊢\phi \to W\left(A\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		knoppcld.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppcld.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
3		knoppcld.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
4		knoppcld.a	$$⊢\phi \to A\in ℝ$$
5		knoppcld.n	$$⊢\phi \to N\in \mathbb{N}$$
6		knoppcld.1	$$⊢\phi \to C\in ℝ$$
7		knoppcld.2	$$⊢\phi \to \left|C\right|<1$$
8	1 2 3 5 6 7	knoppcn	$$⊢\phi \to W:ℝ\underset{cn}{⟶}ℂ$$
9		cncff	$$⊢W:ℝ\underset{cn}{⟶}ℂ\to W:ℝ⟶ℂ$$
10	8 9	syl	$$⊢\phi \to W:ℝ⟶ℂ$$
11	10 4	ffvelrnd	$$⊢\phi \to W\left(A\right)\in ℂ$$