Theorem knoppcn2

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

	Ref	Expression
Hypotheses	knoppcn2.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	knoppcn2.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	knoppcn2.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
	knoppcn2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	knoppcn2.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
Assertion	knoppcn2	⊢ ( 𝜑 → 𝑊 ∈ ( ℝ –cn→ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		knoppcn2.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppcn2.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppcn2.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4		knoppcn2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		knoppcn2.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
6	1 2 3 5 4	knoppf	⊢ ( 𝜑 → 𝑊 : ℝ ⟶ ℝ )
7		ax-resscn	⊢ ℝ ⊆ ℂ
8	7	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
9	5	knoppndvlem3	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
10	9	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
11	9	simprd	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
12	1 2 3 4 10 11	knoppcn	⊢ ( 𝜑 → 𝑊 ∈ ( ℝ –cn→ ℂ ) )
13	8 12	jca	⊢ ( 𝜑 → ( ℝ ⊆ ℂ ∧ 𝑊 ∈ ( ℝ –cn→ ℂ ) ) )
14		cncffvrn	⊢ ( ( ℝ ⊆ ℂ ∧ 𝑊 ∈ ( ℝ –cn→ ℂ ) ) → ( 𝑊 ∈ ( ℝ –cn→ ℝ ) ↔ 𝑊 : ℝ ⟶ ℝ ) )
15	13 14	syl	⊢ ( 𝜑 → ( 𝑊 ∈ ( ℝ –cn→ ℝ ) ↔ 𝑊 : ℝ ⟶ ℝ ) )
16	6 15	mpbird	⊢ ( 𝜑 → 𝑊 ∈ ( ℝ –cn→ ℝ ) )