knoppndv

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

	Ref	Expression
Hypotheses	knoppndv.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
	knoppndv.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
	knoppndv.w	$⊢ W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
	knoppndv.c	$⊢ φ \to C \in (- 1, 1)$
	knoppndv.n	$⊢ φ \to N \in ℕ$
	knoppndv.1	$⊢ φ \to 1 < N \|C\|$
Assertion	knoppndv	$⊢ φ \to dom W_{ℝ}^{'} = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		knoppndv.t	$⊢ T = (x \in ℝ ⟼ \|⌊x + (\frac{1}{2})⌋ - x\|)$
2		knoppndv.f	$⊢ F = (y \in ℝ ⟼ (n \in ℕ_{0} ⟼ C^{n} T ({2 \cdot N}^{n} y)))$
3		knoppndv.w	$⊢ W = (w \in ℝ ⟼ \sum_{i \in ℕ_{0}} F (w) (i))$
4		knoppndv.c	$⊢ φ \to C \in (- 1, 1)$
5		knoppndv.n	$⊢ φ \to N \in ℕ$
6		knoppndv.1	$⊢ φ \to 1 < N \|C\|$
7		simpl	$⊢ (φ \land h \in dom W_{ℝ}^{'}) \to φ$
8		ax-resscn	$⊢ ℝ \subseteq ℂ$
9	8	a1i	$⊢ φ \to ℝ \subseteq ℂ$
10	4	knoppndvlem3	$⊢ φ \to (C \in ℝ \land \|C\| < 1)$
11	10	simpld	$⊢ φ \to C \in ℝ$
12	10	simprd	$⊢ φ \to \|C\| < 1$
13	1 2 3 5 11 12	knoppcn	$⊢ φ \to W : ℝ \underset{cn}{⟶} ℂ$
14		cncff	$⊢ W : ℝ \underset{cn}{⟶} ℂ \to W : ℝ ⟶ ℂ$
15	13 14	syl	$⊢ φ \to W : ℝ ⟶ ℂ$
16		ssidd	$⊢ φ \to ℝ \subseteq ℝ$
17	9 15 16	dvbss	$⊢ φ \to dom W_{ℝ}^{'} \subseteq ℝ$
18	17	adantr	$⊢ (φ \land h \in dom W_{ℝ}^{'}) \to dom W_{ℝ}^{'} \subseteq ℝ$
19		simpr	$⊢ (φ \land h \in dom W_{ℝ}^{'}) \to h \in dom W_{ℝ}^{'}$
20	18 19	sseldd	$⊢ (φ \land h \in dom W_{ℝ}^{'}) \to h \in ℝ$
21	7 20	jca	$⊢ (φ \land h \in dom W_{ℝ}^{'}) \to (φ \land h \in ℝ)$
22		ssidd	$⊢ (φ \land h \in ℝ) \to ℝ \subseteq ℝ$
23	15	adantr	$⊢ (φ \land h \in ℝ) \to W : ℝ ⟶ ℂ$
24	4	ad2antrr	$⊢ ((φ \land h \in ℝ) \land (e \in ℝ^{+} \land d \in ℝ^{+})) \to C \in (- 1, 1)$
25		simprr	$⊢ ((φ \land h \in ℝ) \land (e \in ℝ^{+} \land d \in ℝ^{+})) \to d \in ℝ^{+}$
26		simprl	$⊢ ((φ \land h \in ℝ) \land (e \in ℝ^{+} \land d \in ℝ^{+})) \to e \in ℝ^{+}$
27		simplr	$⊢ ((φ \land h \in ℝ) \land (e \in ℝ^{+} \land d \in ℝ^{+})) \to h \in ℝ$
28	5	ad2antrr	$⊢ ((φ \land h \in ℝ) \land (e \in ℝ^{+} \land d \in ℝ^{+})) \to N \in ℕ$
29	6	ad2antrr	$⊢ ((φ \land h \in ℝ) \land (e \in ℝ^{+} \land d \in ℝ^{+})) \to 1 < N \|C\|$
30	1 2 3 24 25 26 27 28 29	knoppndvlem22	$⊢ ((φ \land h \in ℝ) \land (e \in ℝ^{+} \land d \in ℝ^{+})) \to \exists a \in ℝ \exists b \in ℝ ((a \leq h \land h \leq b) \land (b - a < d \land a \neq b) \land e \leq \frac{\|W (b) - W (a)\|}{b - a})$
31	30	ralrimivva	$⊢ (φ \land h \in ℝ) \to \forall e \in ℝ^{+} \forall d \in ℝ^{+} \exists a \in ℝ \exists b \in ℝ ((a \leq h \land h \leq b) \land (b - a < d \land a \neq b) \land e \leq \frac{\|W (b) - W (a)\|}{b - a})$
32	22 23 31	unbdqndv2	$⊢ (φ \land h \in ℝ) \to \neg h \in dom W_{ℝ}^{'}$
33	21 32	syl	$⊢ (φ \land h \in dom W_{ℝ}^{'}) \to \neg h \in dom W_{ℝ}^{'}$
34	33	pm2.01da	$⊢ φ \to \neg h \in dom W_{ℝ}^{'}$
35	34	alrimiv	$⊢ φ \to \forall h \neg h \in dom W_{ℝ}^{'}$
36		eq0	$⊢ dom W_{ℝ}^{'} = \emptyset \leftrightarrow \forall h \neg h \in dom W_{ℝ}^{'}$
37	35 36	sylibr	$⊢ φ \to dom W_{ℝ}^{'} = \emptyset$

Metamath Proof Explorer

Theorem knoppndv

Proof