Theorem cnndv

Description: There exists a continuous nowhere differentiable function. The result follows directly from knoppcn and knoppndv . (Contributed by Asger C. Ipsen, 26-Aug-2021)

	Ref	Expression
Assertion	cnndv	⊢ ∃ 𝑓 ( 𝑓 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑓 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		eqid	⊢ ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 1 / 2 ) ↑ 𝑛 ) · ( ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) ) ‘ ( ( ( 2 · 3 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) ) = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 1 / 2 ) ↑ 𝑛 ) · ( ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) ) ‘ ( ( ( 2 · 3 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		eqid	⊢ ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 1 / 2 ) ↑ 𝑛 ) · ( ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) ) ‘ ( ( ( 2 · 3 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) ) ‘ 𝑤 ) ‘ 𝑖 ) ) = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( ( 1 / 2 ) ↑ 𝑛 ) · ( ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) ) ‘ ( ( ( 2 · 3 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) ) ‘ 𝑤 ) ‘ 𝑖 ) )
4	1 2 3	cnndvlem2	⊢ ∃ 𝑓 ( 𝑓 ∈ ( ℝ –cn→ ℝ ) ∧ dom ( ℝ D 𝑓 ) = ∅ )