Theorem cnndv

Description: There exists a continuous nowhere differentiable function. The result follows directly from knoppcn and knoppndv . (Contributed by Asger C. Ipsen, 26-Aug-2021)

	Ref	Expression
Assertion	cnndv	|- E. f ( f e. ( RR -cn-> RR ) /\ dom ( RR _D f ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) ) = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		eqid	|- ( y e. RR |-> ( n e. NN0 |-> ( ( ( 1 / 2 ) ^ n ) x. ( ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) ) ` ( ( ( 2 x. 3 ) ^ n ) x. y ) ) ) ) ) = ( y e. RR |-> ( n e. NN0 |-> ( ( ( 1 / 2 ) ^ n ) x. ( ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) ) ` ( ( ( 2 x. 3 ) ^ n ) x. y ) ) ) ) )
3		eqid	|- ( w e. RR |-> sum_ i e. NN0 ( ( ( y e. RR |-> ( n e. NN0 |-> ( ( ( 1 / 2 ) ^ n ) x. ( ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) ) ` ( ( ( 2 x. 3 ) ^ n ) x. y ) ) ) ) ) ` w ) ` i ) ) = ( w e. RR |-> sum_ i e. NN0 ( ( ( y e. RR |-> ( n e. NN0 |-> ( ( ( 1 / 2 ) ^ n ) x. ( ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) ) ` ( ( ( 2 x. 3 ) ^ n ) x. y ) ) ) ) ) ` w ) ` i ) )
4	1 2 3	cnndvlem2	|- E. f ( f e. ( RR -cn-> RR ) /\ dom ( RR _D f ) = (/) )