Theorem knoppcn2

Description: Variant of knoppcn with different codomain. (Contributed by Asger C. Ipsen, 25-Aug-2021)

	Ref	Expression
Hypotheses	knoppcn2.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	knoppcn2.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)$$
	knoppcn2.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
	knoppcn2.n	$$⊢\phi \to N\in \mathbb{N}$$
	knoppcn2.c	$$⊢\phi \to C\in \left(-1,1\right)$$
Assertion	knoppcn2	$$⊢\phi \to W:ℝ\underset{cn}{⟶}ℝ$$

Proof

Step	Hyp	Ref	Expression
1		knoppcn2.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppcn2.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		knoppcn2.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
4		knoppcn2.n	$$⊢\phi \to N\in \mathbb{N}$$
5		knoppcn2.c	$$⊢\phi \to C\in \left(-1,1\right)$$
6	1 2 3 5 4	knoppf	$$⊢\phi \to W:ℝ⟶ℝ$$
7		ax-resscn	$$⊢ℝ\subseteq ℂ$$
8	7	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
9	5	knoppndvlem3	$$⊢\phi \to \left(C\in ℝ\wedge \left|C\right|<1\right)$$
10	9	simpld	$$⊢\phi \to C\in ℝ$$
11	9	simprd	$$⊢\phi \to \left|C\right|<1$$
12	1 2 3 4 10 11	knoppcn	$$⊢\phi \to W:ℝ\underset{cn}{⟶}ℂ$$
13	8 12	jca	$$⊢\phi \to \left(ℝ\subseteq ℂ\wedge W:ℝ\underset{cn}{⟶}ℂ\right)$$
14		cncffvrn	$$⊢\left(ℝ\subseteq ℂ\wedge W:ℝ\underset{cn}{⟶}ℂ\right)\to \left(W:ℝ\underset{cn}{⟶}ℝ\leftrightarrow W:ℝ⟶ℝ\right)$$
15	13 14	syl	$$⊢\phi \to \left(W:ℝ\underset{cn}{⟶}ℝ\leftrightarrow W:ℝ⟶ℝ\right)$$
16	6 15	mpbird	$$⊢\phi \to W:ℝ\underset{cn}{⟶}ℝ$$