# 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 $⊢ T = x ∈ ℝ ⟼ x + 1 2 − x$
knoppndv.f $⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y$
knoppndv.w $⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i$
knoppndv.c $⊢ φ → C ∈ − 1 1$
knoppndv.n $⊢ φ → N ∈ ℕ$
knoppndv.1 $⊢ φ → 1 < N ⁢ C$
Assertion knoppndv $⊢ φ → dom ⁡ W ℝ ′ = ∅$

### Proof

Step Hyp Ref Expression
1 knoppndv.t $⊢ T = x ∈ ℝ ⟼ x + 1 2 − x$
2 knoppndv.f $⊢ F = y ∈ ℝ ⟼ n ∈ ℕ 0 ⟼ C n ⁢ T ⁡ 2 ⋅ N n ⁢ y$
3 knoppndv.w $⊢ W = w ∈ ℝ ⟼ ∑ i ∈ ℕ 0 F ⁡ w ⁡ i$
4 knoppndv.c $⊢ φ → C ∈ − 1 1$
5 knoppndv.n $⊢ φ → N ∈ ℕ$
6 knoppndv.1 $⊢ φ → 1 < N ⁢ C$
7 simpl $⊢ φ ∧ h ∈ dom ⁡ W ℝ ′ → φ$
8 ax-resscn $⊢ ℝ ⊆ ℂ$
9 8 a1i $⊢ φ → ℝ ⊆ ℂ$
10 4 knoppndvlem3 $⊢ φ → C ∈ ℝ ∧ C < 1$
11 10 simpld $⊢ φ → C ∈ ℝ$
12 10 simprd $⊢ φ → C < 1$
13 1 2 3 5 11 12 knoppcn $⊢ φ → W : ℝ ⟶cn ℂ$
14 cncff $⊢ W : ℝ ⟶cn ℂ → W : ℝ ⟶ ℂ$
15 13 14 syl $⊢ φ → W : ℝ ⟶ ℂ$
16 ssidd $⊢ φ → ℝ ⊆ ℝ$
17 9 15 16 dvbss $⊢ φ → dom ⁡ W ℝ ′ ⊆ ℝ$
18 17 adantr $⊢ φ ∧ h ∈ dom ⁡ W ℝ ′ → dom ⁡ W ℝ ′ ⊆ ℝ$
19 simpr $⊢ φ ∧ h ∈ dom ⁡ W ℝ ′ → h ∈ dom ⁡ W ℝ ′$
20 18 19 sseldd $⊢ φ ∧ h ∈ dom ⁡ W ℝ ′ → h ∈ ℝ$
21 7 20 jca $⊢ φ ∧ h ∈ dom ⁡ W ℝ ′ → φ ∧ h ∈ ℝ$
22 ssidd $⊢ φ ∧ h ∈ ℝ → ℝ ⊆ ℝ$
23 15 adantr $⊢ φ ∧ h ∈ ℝ → W : ℝ ⟶ ℂ$
24 4 ad2antrr $⊢ φ ∧ h ∈ ℝ ∧ e ∈ ℝ + ∧ d ∈ ℝ + → C ∈ − 1 1$
25 simprr $⊢ φ ∧ h ∈ ℝ ∧ e ∈ ℝ + ∧ d ∈ ℝ + → d ∈ ℝ +$
26 simprl $⊢ φ ∧ h ∈ ℝ ∧ e ∈ ℝ + ∧ d ∈ ℝ + → e ∈ ℝ +$
27 simplr $⊢ φ ∧ h ∈ ℝ ∧ e ∈ ℝ + ∧ d ∈ ℝ + → h ∈ ℝ$
28 5 ad2antrr $⊢ φ ∧ h ∈ ℝ ∧ e ∈ ℝ + ∧ d ∈ ℝ + → N ∈ ℕ$
29 6 ad2antrr $⊢ φ ∧ h ∈ ℝ ∧ e ∈ ℝ + ∧ d ∈ ℝ + → 1 < N ⁢ C$
30 1 2 3 24 25 26 27 28 29 knoppndvlem22 $⊢ φ ∧ h ∈ ℝ ∧ e ∈ ℝ + ∧ d ∈ ℝ + → ∃ a ∈ ℝ ∃ b ∈ ℝ a ≤ h ∧ h ≤ b ∧ b − a < d ∧ a ≠ b ∧ e ≤ W ⁡ b − W ⁡ a b − a$
31 30 ralrimivva $⊢ φ ∧ h ∈ ℝ → ∀ e ∈ ℝ + ∀ d ∈ ℝ + ∃ a ∈ ℝ ∃ b ∈ ℝ a ≤ h ∧ h ≤ b ∧ b − a < d ∧ a ≠ b ∧ e ≤ W ⁡ b − W ⁡ a b − a$
32 22 23 31 unbdqndv2 $⊢ φ ∧ h ∈ ℝ → ¬ h ∈ dom ⁡ W ℝ ′$
33 21 32 syl $⊢ φ ∧ h ∈ dom ⁡ W ℝ ′ → ¬ h ∈ dom ⁡ W ℝ ′$
34 33 pm2.01da $⊢ φ → ¬ h ∈ dom ⁡ W ℝ ′$
35 34 alrimiv $⊢ φ → ∀ h ¬ h ∈ dom ⁡ W ℝ ′$
36 eq0 $⊢ dom ⁡ W ℝ ′ = ∅ ↔ ∀ h ¬ h ∈ dom ⁡ W ℝ ′$
37 35 36 sylibr $⊢ φ → dom ⁡ W ℝ ′ = ∅$