Metamath Proof Explorer

Theorem knoppcnlem11

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

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

Proof

Step Hyp Ref Expression
1 knoppcnlem11.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppcnlem11.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppcnlem11.n 
 |-  ( ph -> N e. NN )
4 knoppcnlem11.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 eqidd 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ l e. ( 0 ... k ) ) -> ( ( F ` w ) ` l ) = ( ( F ` w ) ` l ) )
10 simplr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) -> k e. NN0 )
11 elnn0uz 
 |-  ( k e. NN0 <-> k e. ( ZZ>= ` 0 ) )
12 10 11 sylib 
 |-  ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) -> k e. ( ZZ>= ` 0 ) )
13 5 ad2antrr 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ l e. ( 0 ... k ) ) -> N e. NN )
14 6 ad2antrr 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ l e. ( 0 ... k ) ) -> C e. RR )
15 simplr 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ l e. ( 0 ... k ) ) -> w e. RR )
16 elfzuz 
 |-  ( l e. ( 0 ... k ) -> l e. ( ZZ>= ` 0 ) )
17 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
18 16 17 eleqtrrdi 
 |-  ( l e. ( 0 ... k ) -> l e. NN0 )
19 18 adantl 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ l e. ( 0 ... k ) ) -> l e. NN0 )
20 1 2 13 14 15 19 knoppcnlem3 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ l e. ( 0 ... k ) ) -> ( ( F ` w ) ` l ) e. RR )
21 20 recnd 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) /\ l e. ( 0 ... k ) ) -> ( ( F ` w ) ` l ) e. CC )
22 9 12 21 fsumser 
 |-  ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) -> sum_ l e. ( 0 ... k ) ( ( F ` w ) ` l ) = ( seq 0 ( + , ( F ` w ) ) ` k ) )
23 22 eqcomd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ w e. RR ) -> ( seq 0 ( + , ( F ` w ) ) ` k ) = sum_ l e. ( 0 ... k ) ( ( F ` w ) ` l ) )
24 23 mpteq2dva 
 |-  ( ( ph /\ k e. NN0 ) -> ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` k ) ) = ( w e. RR |-> sum_ l e. ( 0 ... k ) ( ( F ` w ) ` l ) ) )
25 8 24 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) = ( w e. RR |-> sum_ l e. ( 0 ... k ) ( ( F ` w ) ` l ) ) )
26 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
27 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
28 27 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> ( topGen ` ran (,) ) e. ( TopOn ` RR ) )
29 fzfid 
 |-  ( ( ph /\ k e. NN0 ) -> ( 0 ... k ) e. Fin )
30 5 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> N e. NN )
31 6 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> C e. RR )
32 18 adantl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> l e. NN0 )
33 1 2 30 31 32 knoppcnlem10 
 |-  ( ( ( ph /\ k e. NN0 ) /\ l e. ( 0 ... k ) ) -> ( w e. RR |-> ( ( F ` w ) ` l ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
34 26 28 29 33 fsumcn 
 |-  ( ( ph /\ k e. NN0 ) -> ( w e. RR |-> sum_ l e. ( 0 ... k ) ( ( F ` w ) ` l ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
35 ax-resscn 
 |-  RR C_ CC
36 ssid 
 |-  CC C_ CC
37 35 36 pm3.2i 
 |-  ( RR C_ CC /\ CC C_ CC )
38 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
39 26 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
40 39 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
41 26 38 40 cncfcn 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( RR -cn-> CC ) = ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) ) )
42 37 41 ax-mp 
 |-  ( RR -cn-> CC ) = ( ( topGen ` ran (,) ) Cn ( TopOpen ` CCfld ) )
43 34 42 eleqtrrdi 
 |-  ( ( ph /\ k e. NN0 ) -> ( w e. RR |-> sum_ l e. ( 0 ... k ) ( ( F ` w ) ` l ) ) e. ( RR -cn-> CC ) )
44 25 43 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) e. ( RR -cn-> CC ) )
45 44 fmpttd 
 |-  ( ph -> ( k e. NN0 |-> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) ) : NN0 --> ( RR -cn-> CC ) )
46 0z 
 |-  0 e. ZZ
47 seqfn 
 |-  ( 0 e. ZZ -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) Fn ( ZZ>= ` 0 ) )
48 46 47 ax-mp 
 |-  seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) Fn ( ZZ>= ` 0 )
49 17 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 ) )
50 48 49 mpbir 
 |-  seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) Fn NN0
51 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 ) ) )
52 50 51 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 ) )
53 52 feq1i 
 |-  ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) : NN0 --> ( RR -cn-> CC ) <-> ( k e. NN0 |-> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) ) : NN0 --> ( RR -cn-> CC ) )
54 45 53 sylibr 
 |-  ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) : NN0 --> ( RR -cn-> CC ) )