Theorem knoppcn2

Description: Variant of knoppcn with different codomain. (Contributed by Asger C. Ipsen, 25-Aug-2021)

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

Proof

Step	Hyp	Ref	Expression
1		knoppcn2.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		knoppcn2.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3		knoppcn2.w	|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4		knoppcn2.n	|- ( ph -> N e. NN )
5		knoppcn2.c	|- ( ph -> C e. ( -u 1 (,) 1 ) )
6	1 2 3 5 4	knoppf	|- ( ph -> W : RR --> RR )
7		ax-resscn	|- RR C_ CC
8	7	a1i	|- ( ph -> RR C_ CC )
9	5	knoppndvlem3	|- ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
10	9	simpld	|- ( ph -> C e. RR )
11	9	simprd	|- ( ph -> ( abs ` C ) < 1 )
12	1 2 3 4 10 11	knoppcn	|- ( ph -> W e. ( RR -cn-> CC ) )
13	8 12	jca	|- ( ph -> ( RR C_ CC /\ W e. ( RR -cn-> CC ) ) )
14		cncffvrn	|- ( ( RR C_ CC /\ W e. ( RR -cn-> CC ) ) -> ( W e. ( RR -cn-> RR ) <-> W : RR --> RR ) )
15	13 14	syl	|- ( ph -> ( W e. ( RR -cn-> RR ) <-> W : RR --> RR ) )
16	6 15	mpbird	|- ( ph -> W e. ( RR -cn-> RR ) )