Theorem knoppcn

Description: The continuous nowhere differentiable function W ( Knopp, K. (1918). Math. Z. 2, 1-26 ) is, in fact, continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

	Ref	Expression
Hypotheses	knoppcn.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
	knoppcn.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
	knoppcn.w	|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
	knoppcn.n	|- ( ph -> N e. NN )
	knoppcn.1	|- ( ph -> C e. RR )
	knoppcn.2	|- ( ph -> ( abs ` C ) < 1 )
Assertion	knoppcn	|- ( ph -> W e. ( RR -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		knoppcn.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		knoppcn.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3		knoppcn.w	|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4		knoppcn.n	|- ( ph -> N e. NN )
5		knoppcn.1	|- ( ph -> C e. RR )
6		knoppcn.2	|- ( ph -> ( abs ` C ) < 1 )
7		nn0uz	|- NN0 = ( ZZ>= ` 0 )
8		0zd	|- ( ph -> 0 e. ZZ )
9	1 2 4 5	knoppcnlem11	|- ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) : NN0 --> ( RR -cn-> CC ) )
10	1 2 3 4 5 6	knoppcnlem9	|- ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) W )
11	7 8 9 10	ulmcn	|- ( ph -> W e. ( RR -cn-> CC ) )