Metamath Proof Explorer

Theorem knoppcnlem8

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

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

Proof

Step Hyp Ref Expression
1 knoppcnlem8.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppcnlem8.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppcnlem8.n 
 |-  ( ph -> N e. NN )
4 knoppcnlem8.1 
 |-  ( ph -> C e. RR )
5 3 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> N e. NN )
6 4 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> C e. RR )
7 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
8 1 2 5 6 7 knoppcnlem7 
 |-  ( ( ph /\ k e. NN0 ) -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) = ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` k ) ) )
9 simplr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) -> k e. NN0 )
10 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
11 9 10 eleqtrdi 
 |-  ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) -> k e. ( ZZ>= ` 0 ) )
12 5 ad2antrr 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ a e. ( 0 ... k ) ) -> N e. NN )
13 6 ad2antrr 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ a e. ( 0 ... k ) ) -> C e. RR )
14 simplr 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ a e. ( 0 ... k ) ) -> w e. RR )
15 elfznn0 
 |-  ( a e. ( 0 ... k ) -> a e. NN0 )
16 15 adantl 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ a e. ( 0 ... k ) ) -> a e. NN0 )
17 1 2 12 13 14 16 knoppcnlem3 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ a e. ( 0 ... k ) ) -> ( ( F ` w ) ` a ) e. RR )
18 17 recnd 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ a e. ( 0 ... k ) ) -> ( ( F ` w ) ` a ) e. CC )
19 addcl 
 |-  ( ( a e. CC /\ b e. CC ) -> ( a + b ) e. CC )
20 19 adantl 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ ( a e. CC /\ b e. CC ) ) -> ( a + b ) e. CC )
21 11 18 20 seqcl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) -> ( seq 0 ( + , ( F ` w ) ) ` k ) e. CC )
22 21 fmpttd 
 |-  ( ( ph /\ k e. NN0 ) -> ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` k ) ) : RR --> CC )
23 cnex 
 |-  CC e. _V
24 reex 
 |-  RR e. _V
25 23 24 pm3.2i 
 |-  ( CC e. _V /\ RR e. _V )
26 elmapg 
 |-  ( ( CC e. _V /\ RR e. _V ) -> ( ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` k ) ) e. ( CC ^m RR ) <-> ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` k ) ) : RR --> CC ) )
27 25 26 ax-mp 
 |-  ( ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` k ) ) e. ( CC ^m RR ) <-> ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` k ) ) : RR --> CC )
28 22 27 sylibr 
 |-  ( ( ph /\ k e. NN0 ) -> ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` k ) ) e. ( CC ^m RR ) )
29 8 28 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) e. ( CC ^m RR ) )
30 29 fmpttd 
 |-  ( ph -> ( k e. NN0 |-> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) ) : NN0 --> ( CC ^m RR ) )
31 0z 
 |-  0 e. ZZ
32 seqfn 
 |-  ( 0 e. ZZ -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) Fn ( ZZ>= ` 0 ) )
33 31 32 ax-mp 
 |-  seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) Fn ( ZZ>= ` 0 )
34 10 fneq2i 
 |-  ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) Fn NN0 <-> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) Fn ( ZZ>= ` 0 ) )
35 33 34 mpbir 
 |-  seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) Fn NN0
36 dffn5 
 |-  ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) Fn NN0 <-> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) = ( k e. NN0 |-> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) ) )
37 35 36 mpbi 
 |-  seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) = ( k e. NN0 |-> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) )
38 37 feq1i 
 |-  ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) : NN0 --> ( CC ^m RR ) <-> ( k e. NN0 |-> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) ) : NN0 --> ( CC ^m RR ) )
39 30 38 sylibr 
 |-  ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) : NN0 --> ( CC ^m RR ) )