Theorem 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	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
	knoppndv.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
	knoppndv.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
	knoppndv.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
	knoppndv.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	knoppndv.1	⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
Assertion	knoppndv	⊢ ( 𝜑 → dom ( ℝ D 𝑊 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		knoppndv.t	⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2		knoppndv.f	⊢ 𝐹 = ( 𝑦 ∈ ℝ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐶 ↑ 𝑛 ) · ( 𝑇 ‘ ( ( ( 2 · 𝑁 ) ↑ 𝑛 ) · 𝑦 ) ) ) ) )
3		knoppndv.w	⊢ 𝑊 = ( 𝑤 ∈ ℝ ↦ Σ 𝑖 ∈ ℕ0 ( ( 𝐹 ‘ 𝑤 ) ‘ 𝑖 ) )
4		knoppndv.c	⊢ ( 𝜑 → 𝐶 ∈ ( - 1 (,) 1 ) )
5		knoppndv.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		knoppndv.1	⊢ ( 𝜑 → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
7		simpl	⊢ ( ( 𝜑 ∧ ℎ ∈ dom ( ℝ D 𝑊 ) ) → 𝜑 )
8		ax-resscn	⊢ ℝ ⊆ ℂ
9	8	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
10	4	knoppndvlem3	⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ( abs ‘ 𝐶 ) < 1 ) )
11	10	simpld	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
12	10	simprd	⊢ ( 𝜑 → ( abs ‘ 𝐶 ) < 1 )
13	1 2 3 5 11 12	knoppcn	⊢ ( 𝜑 → 𝑊 ∈ ( ℝ –cn→ ℂ ) )
14		cncff	⊢ ( 𝑊 ∈ ( ℝ –cn→ ℂ ) → 𝑊 : ℝ ⟶ ℂ )
15	13 14	syl	⊢ ( 𝜑 → 𝑊 : ℝ ⟶ ℂ )
16		ssidd	⊢ ( 𝜑 → ℝ ⊆ ℝ )
17	9 15 16	dvbss	⊢ ( 𝜑 → dom ( ℝ D 𝑊 ) ⊆ ℝ )
18	17	adantr	⊢ ( ( 𝜑 ∧ ℎ ∈ dom ( ℝ D 𝑊 ) ) → dom ( ℝ D 𝑊 ) ⊆ ℝ )
19		simpr	⊢ ( ( 𝜑 ∧ ℎ ∈ dom ( ℝ D 𝑊 ) ) → ℎ ∈ dom ( ℝ D 𝑊 ) )
20	18 19	sseldd	⊢ ( ( 𝜑 ∧ ℎ ∈ dom ( ℝ D 𝑊 ) ) → ℎ ∈ ℝ )
21	7 20	jca	⊢ ( ( 𝜑 ∧ ℎ ∈ dom ( ℝ D 𝑊 ) ) → ( 𝜑 ∧ ℎ ∈ ℝ ) )
22		ssidd	⊢ ( ( 𝜑 ∧ ℎ ∈ ℝ ) → ℝ ⊆ ℝ )
23	15	adantr	⊢ ( ( 𝜑 ∧ ℎ ∈ ℝ ) → 𝑊 : ℝ ⟶ ℂ )
24	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ℎ ∈ ℝ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 𝐶 ∈ ( - 1 (,) 1 ) )
25		simprr	⊢ ( ( ( 𝜑 ∧ ℎ ∈ ℝ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 𝑑 ∈ ℝ+ )
26		simprl	⊢ ( ( ( 𝜑 ∧ ℎ ∈ ℝ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 𝑒 ∈ ℝ+ )
27		simplr	⊢ ( ( ( 𝜑 ∧ ℎ ∈ ℝ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → ℎ ∈ ℝ )
28	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ℎ ∈ ℝ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 𝑁 ∈ ℕ )
29	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ℎ ∈ ℝ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 1 < ( 𝑁 · ( abs ‘ 𝐶 ) ) )
30	1 2 3 24 25 26 27 28 29	knoppndvlem22	⊢ ( ( ( 𝜑 ∧ ℎ ∈ ℝ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ( 𝑎 ≤ ℎ ∧ ℎ ≤ 𝑏 ) ∧ ( ( 𝑏 − 𝑎 ) < 𝑑 ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑒 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ) )
31	30	ralrimivva	⊢ ( ( 𝜑 ∧ ℎ ∈ ℝ ) → ∀ 𝑒 ∈ ℝ+ ∀ 𝑑 ∈ ℝ+ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ ( ( 𝑎 ≤ ℎ ∧ ℎ ≤ 𝑏 ) ∧ ( ( 𝑏 − 𝑎 ) < 𝑑 ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑒 ≤ ( ( abs ‘ ( ( 𝑊 ‘ 𝑏 ) − ( 𝑊 ‘ 𝑎 ) ) ) / ( 𝑏 − 𝑎 ) ) ) )
32	22 23 31	unbdqndv2	⊢ ( ( 𝜑 ∧ ℎ ∈ ℝ ) → ¬ ℎ ∈ dom ( ℝ D 𝑊 ) )
33	21 32	syl	⊢ ( ( 𝜑 ∧ ℎ ∈ dom ( ℝ D 𝑊 ) ) → ¬ ℎ ∈ dom ( ℝ D 𝑊 ) )
34	33	pm2.01da	⊢ ( 𝜑 → ¬ ℎ ∈ dom ( ℝ D 𝑊 ) )
35	34	alrimiv	⊢ ( 𝜑 → ∀ ℎ ¬ ℎ ∈ dom ( ℝ D 𝑊 ) )
36		eq0	⊢ ( dom ( ℝ D 𝑊 ) = ∅ ↔ ∀ ℎ ¬ ℎ ∈ dom ( ℝ D 𝑊 ) )
37	35 36	sylibr	⊢ ( 𝜑 → dom ( ℝ D 𝑊 ) = ∅ )