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	$$⊢\exists f\left(f:ℝ\underset{cn}{⟶}ℝ\wedge \mathrm{dom}{f}_{ℝ}^{\prime }=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		eqid	$$⊢\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{2}\right)}^n\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)\left({2\cdot 3}^{n}y\right)\right)\right)=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{2}\right)}^n\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)\left({2\cdot 3}^{n}y\right)\right)\right)$$
3		eqid	$$⊢\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{2}\right)}^n\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)\left({2\cdot 3}^{n}y\right)\right)\right)\left(w\right)\left(i\right)\right)=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼{\left(\frac{1}{2}\right)}^n\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)\left({2\cdot 3}^{n}y\right)\right)\right)\left(w\right)\left(i\right)\right)$$
4	1 2 3	cnndvlem2	$$⊢\exists f\left(f:ℝ\underset{cn}{⟶}ℝ\wedge \mathrm{dom}{f}_{ℝ}^{\prime }=\varnothing \right)$$