Theorem knoppcld

Description: Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		knoppcld.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		knoppcld.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3		knoppcld.w	|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4		knoppcld.a	|- ( ph -> A e. RR )
5		knoppcld.n	|- ( ph -> N e. NN )
6		knoppcld.1	|- ( ph -> C e. RR )
7		knoppcld.2	|- ( ph -> ( abs ` C ) < 1 )
8	1 2 3 5 6 7	knoppcn	|- ( ph -> W e. ( RR -cn-> CC ) )
9		cncff	|- ( W e. ( RR -cn-> CC ) -> W : RR --> CC )
10	8 9	syl	|- ( ph -> W : RR --> CC )
11	10 4	ffvelrnd	|- ( ph -> ( W ` A ) e. CC )