Theorem knoppcn

Description: The continuous nowhere differentiable function W ( Knopp, K. (1918). Math. Z. 2, 1-26 ) is, in fact, continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		knoppcn.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppcn.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppcn.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4		knoppcn.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
5		knoppcn.1	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
6		knoppcn.2	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
7		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
8		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
9	1 2 4 5	knoppcnlem11	⊢ ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) : ℕ0 ⟶ ( ℝ –cn→ ℂ ) )
10	1 2 3 4 5 6	knoppcnlem9	⊢ ( 𝜑 → seq 0 ( ∘f + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑧 ∈ ℝ ↦ ( ( 𝐹 ‘ 𝑧 ) ‘ 𝑚 ) ) ) ) ( ⇝𝑢 ‘ ℝ ) 𝑊 )
11	7 8 9 10	ulmcn	⊢ ( 𝜑 → 𝑊 ∈ ( ℝ –cn→ ℂ ) )