Metamath Proof Explorer


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 𝑊 ) = ∅ )