Metamath Proof Explorer

Theorem knoppcnlem9

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

Ref Expression
Hypotheses knoppcnlem9.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppcnlem9.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppcnlem9.w 
|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
knoppcnlem9.n 
|- ( ph -> N e. NN )
knoppcnlem9.1 
|- ( ph -> C e. RR )
knoppcnlem9.2 
|- ( ph -> ( abs ` C ) < 1 )
Assertion knoppcnlem9 
|- ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) W )

Proof

Step Hyp Ref Expression
1 knoppcnlem9.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppcnlem9.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppcnlem9.w 
 |-  W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4 knoppcnlem9.n 
 |-  ( ph -> N e. NN )
5 knoppcnlem9.1 
 |-  ( ph -> C e. RR )
6 knoppcnlem9.2 
 |-  ( ph -> ( abs ` C ) < 1 )
7 1 2 4 5 6 knoppcnlem6 
 |-  ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) e. dom ( ~~>u ` RR ) )
8 seqex 
 |-  seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) e. _V
9 8 eldm 
 |-  ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) e. dom ( ~~>u ` RR ) <-> E. f seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f )
10 7 9 sylib 
 |-  ( ph -> E. f seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f )
11 simpr 
 |-  ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f )
12 ulmcl 
 |-  ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f -> f : RR --> CC )
13 12 feqmptd 
 |-  ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f -> f = ( w e. RR |-> ( f ` w ) ) )
14 13 adantl 
 |-  ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) -> f = ( w e. RR |-> ( f ` w ) ) )
15 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
16 0zd 
 |-  ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) -> 0 e. ZZ )
17 eqidd 
 |-  ( ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) /\ i e. NN0 ) -> ( ( F ` w ) ` i ) = ( ( F ` w ) ` i ) )
18 4 ad2antrr 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> N e. NN )
19 5 ad2antrr 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> C e. RR )
20 simplr 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> w e. RR )
21 simpr 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> i e. NN0 )
22 1 2 18 19 20 21 knoppcnlem3 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> ( ( F ` w ) ` i ) e. RR )
23 22 adantllr 
 |-  ( ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) /\ i e. NN0 ) -> ( ( F ` w ) ` i ) e. RR )
24 23 recnd 
 |-  ( ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) /\ i e. NN0 ) -> ( ( F ` w ) ` i ) e. CC )
25 1 2 4 5 knoppcnlem8 
 |-  ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) : NN0 --> ( CC ^m RR ) )
26 25 ad2antrr 
 |-  ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) : NN0 --> ( CC ^m RR ) )
27 simpr 
 |-  ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) -> w e. RR )
28 seqex 
 |-  seq 0 ( + , ( F ` w ) ) e. _V
29 28 a1i 
 |-  ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) -> seq 0 ( + , ( F ` w ) ) e. _V )
30 4 ad2antrr 
 |-  ( ( ( ph /\ w e. RR ) /\ k e. NN0 ) -> N e. NN )
31 5 ad2antrr 
 |-  ( ( ( ph /\ w e. RR ) /\ k e. NN0 ) -> C e. RR )
32 simpr 
 |-  ( ( ( ph /\ w e. RR ) /\ k e. NN0 ) -> k e. NN0 )
33 1 2 30 31 32 knoppcnlem7 
 |-  ( ( ( ph /\ w e. RR ) /\ k e. NN0 ) -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) = ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) ) )
34 33 adantllr 
 |-  ( ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) /\ k e. NN0 ) -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) = ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) ) )
35 34 fveq1d 
 |-  ( ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) /\ k e. NN0 ) -> ( ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) ` w ) = ( ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) ) ` w ) )
36 eqid 
 |-  ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) ) = ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) )
37 fveq2 
 |-  ( v = w -> ( F ` v ) = ( F ` w ) )
38 37 seqeq3d 
 |-  ( v = w -> seq 0 ( + , ( F ` v ) ) = seq 0 ( + , ( F ` w ) ) )
39 38 fveq1d 
 |-  ( v = w -> ( seq 0 ( + , ( F ` v ) ) ` k ) = ( seq 0 ( + , ( F ` w ) ) ` k ) )
40 27 adantr 
 |-  ( ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) /\ k e. NN0 ) -> w e. RR )
41 fvexd 
 |-  ( ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) /\ k e. NN0 ) -> ( seq 0 ( + , ( F ` w ) ) ` k ) e. _V )
42 36 39 40 41 fvmptd3 
 |-  ( ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) /\ k e. NN0 ) -> ( ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) ) ` w ) = ( seq 0 ( + , ( F ` w ) ) ` k ) )
43 35 42 eqtrd 
 |-  ( ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) /\ k e. NN0 ) -> ( ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) ` w ) = ( seq 0 ( + , ( F ` w ) ) ` k ) )
44 simplr 
 |-  ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f )
45 15 16 26 27 29 43 44 ulmclm 
 |-  ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) -> seq 0 ( + , ( F ` w ) ) ~~> ( f ` w ) )
46 15 16 17 24 45 isumclim 
 |-  ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) -> sum_ i e. NN0 ( ( F ` w ) ` i ) = ( f ` w ) )
47 46 eqcomd 
 |-  ( ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) /\ w e. RR ) -> ( f ` w ) = sum_ i e. NN0 ( ( F ` w ) ` i ) )
48 47 mpteq2dva 
 |-  ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) -> ( w e. RR |-> ( f ` w ) ) = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) ) )
49 3 a1i 
 |-  ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) -> W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) ) )
50 49 eqcomd 
 |-  ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) -> ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) ) = W )
51 14 48 50 3eqtrd 
 |-  ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) -> f = W )
52 11 51 breqtrd 
 |-  ( ( ph /\ seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f ) -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) W )
53 52 ex 
 |-  ( ph -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) W ) )
54 53 exlimdv 
 |-  ( ph -> ( E. f seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) f -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) W ) )
55 10 54 mpd 
 |-  ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) W )