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 e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppndv.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppndv.w 
|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
knoppndv.c 
|- ( ph -> C e. ( -u 1 (,) 1 ) )
knoppndv.n 
|- ( ph -> N e. NN )
knoppndv.1 
|- ( ph -> 1 < ( N x. ( abs ` C ) ) )
Assertion knoppndv 
|- ( ph -> dom ( RR _D W ) = (/) )

Proof

Step Hyp Ref Expression
1 knoppndv.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndv.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndv.w 
 |-  W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4 knoppndv.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
5 knoppndv.n 
 |-  ( ph -> N e. NN )
6 knoppndv.1 
 |-  ( ph -> 1 < ( N x. ( abs ` C ) ) )
7 simpl 
 |-  ( ( ph /\ h e. dom ( RR _D W ) ) -> ph )
8 ax-resscn 
 |-  RR C_ CC
9 8 a1i 
 |-  ( ph -> RR C_ CC )
10 4 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
11 10 simpld 
 |-  ( ph -> C e. RR )
12 10 simprd 
 |-  ( ph -> ( abs ` C ) < 1 )
13 1 2 3 5 11 12 knoppcn 
 |-  ( ph -> W e. ( RR -cn-> CC ) )
14 cncff 
 |-  ( W e. ( RR -cn-> CC ) -> W : RR --> CC )
15 13 14 syl 
 |-  ( ph -> W : RR --> CC )
16 ssidd 
 |-  ( ph -> RR C_ RR )
17 9 15 16 dvbss 
 |-  ( ph -> dom ( RR _D W ) C_ RR )
18 17 adantr 
 |-  ( ( ph /\ h e. dom ( RR _D W ) ) -> dom ( RR _D W ) C_ RR )
19 simpr 
 |-  ( ( ph /\ h e. dom ( RR _D W ) ) -> h e. dom ( RR _D W ) )
20 18 19 sseldd 
 |-  ( ( ph /\ h e. dom ( RR _D W ) ) -> h e. RR )
21 7 20 jca 
 |-  ( ( ph /\ h e. dom ( RR _D W ) ) -> ( ph /\ h e. RR ) )
22 ssidd 
 |-  ( ( ph /\ h e. RR ) -> RR C_ RR )
23 15 adantr 
 |-  ( ( ph /\ h e. RR ) -> W : RR --> CC )
24 4 ad2antrr 
 |-  ( ( ( ph /\ h e. RR ) /\ ( e e. RR+ /\ d e. RR+ ) ) -> C e. ( -u 1 (,) 1 ) )
25 simprr 
 |-  ( ( ( ph /\ h e. RR ) /\ ( e e. RR+ /\ d e. RR+ ) ) -> d e. RR+ )
26 simprl 
 |-  ( ( ( ph /\ h e. RR ) /\ ( e e. RR+ /\ d e. RR+ ) ) -> e e. RR+ )
27 simplr 
 |-  ( ( ( ph /\ h e. RR ) /\ ( e e. RR+ /\ d e. RR+ ) ) -> h e. RR )
28 5 ad2antrr 
 |-  ( ( ( ph /\ h e. RR ) /\ ( e e. RR+ /\ d e. RR+ ) ) -> N e. NN )
29 6 ad2antrr 
 |-  ( ( ( ph /\ h e. RR ) /\ ( e e. RR+ /\ d e. RR+ ) ) -> 1 < ( N x. ( abs ` C ) ) )
30 1 2 3 24 25 26 27 28 29 knoppndvlem22 
 |-  ( ( ( ph /\ h e. RR ) /\ ( e e. RR+ /\ d e. RR+ ) ) -> E. a e. RR E. b e. RR ( ( a <_ h /\ h <_ b ) /\ ( ( b - a ) < d /\ a =/= b ) /\ e <_ ( ( abs ` ( ( W ` b ) - ( W ` a ) ) ) / ( b - a ) ) ) )
31 30 ralrimivva 
 |-  ( ( ph /\ h e. RR ) -> A. e e. RR+ A. d e. RR+ E. a e. RR E. b e. RR ( ( a <_ h /\ h <_ b ) /\ ( ( b - a ) < d /\ a =/= b ) /\ e <_ ( ( abs ` ( ( W ` b ) - ( W ` a ) ) ) / ( b - a ) ) ) )
32 22 23 31 unbdqndv2 
 |-  ( ( ph /\ h e. RR ) -> -. h e. dom ( RR _D W ) )
33 21 32 syl 
 |-  ( ( ph /\ h e. dom ( RR _D W ) ) -> -. h e. dom ( RR _D W ) )
34 33 pm2.01da 
 |-  ( ph -> -. h e. dom ( RR _D W ) )
35 34 alrimiv 
 |-  ( ph -> A. h -. h e. dom ( RR _D W ) )
36 eq0 
 |-  ( dom ( RR _D W ) = (/) <-> A. h -. h e. dom ( RR _D W ) )
37 35 36 sylibr 
 |-  ( ph -> dom ( RR _D W ) = (/) )