Theorem knoppcnlem5

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

	Ref	Expression
Hypotheses	knoppcnlem5.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
	knoppcnlem5.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
	knoppcnlem5.n	|- ( ph -> N e. NN )
	knoppcnlem5.1	|- ( ph -> C e. RR )
Assertion	knoppcnlem5	|- ( ph -> ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) : NN0 --> ( CC ^m RR ) )

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem5.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		knoppcnlem5.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3		knoppcnlem5.n	|- ( ph -> N e. NN )
4		knoppcnlem5.1	|- ( ph -> C e. RR )
5	3	ad2antrr	|- ( ( ( ph /\ m e. NN0 ) /\ z e. RR ) -> N e. NN )
6	4	ad2antrr	|- ( ( ( ph /\ m e. NN0 ) /\ z e. RR ) -> C e. RR )
7		simpr	|- ( ( ( ph /\ m e. NN0 ) /\ z e. RR ) -> z e. RR )
8		simplr	|- ( ( ( ph /\ m e. NN0 ) /\ z e. RR ) -> m e. NN0 )
9	1 2 5 6 7 8	knoppcnlem3	|- ( ( ( ph /\ m e. NN0 ) /\ z e. RR ) -> ( ( F ` z ) ` m ) e. RR )
10	9	recnd	|- ( ( ( ph /\ m e. NN0 ) /\ z e. RR ) -> ( ( F ` z ) ` m ) e. CC )
11	10	fmpttd	|- ( ( ph /\ m e. NN0 ) -> ( z e. RR |-> ( ( F ` z ) ` m ) ) : RR --> CC )
12		cnex	|- CC e. _V
13		reex	|- RR e. _V
14	12 13	pm3.2i	|- ( CC e. _V /\ RR e. _V )
15		elmapg	|- ( ( CC e. _V /\ RR e. _V ) -> ( ( z e. RR |-> ( ( F ` z ) ` m ) ) e. ( CC ^m RR ) <-> ( z e. RR |-> ( ( F ` z ) ` m ) ) : RR --> CC ) )
16	14 15	ax-mp	|- ( ( z e. RR |-> ( ( F ` z ) ` m ) ) e. ( CC ^m RR ) <-> ( z e. RR |-> ( ( F ` z ) ` m ) ) : RR --> CC )
17	11 16	sylibr	|- ( ( ph /\ m e. NN0 ) -> ( z e. RR |-> ( ( F ` z ) ` m ) ) e. ( CC ^m RR ) )
18	17	fmpttd	|- ( ph -> ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) : NN0 --> ( CC ^m RR ) )