Metamath Proof Explorer

Theorem knoppndvlem4

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 15-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 knoppndvlem4.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndvlem4.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndvlem4.w 
 |-  W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4 knoppndvlem4.a 
 |-  ( ph -> A e. RR )
5 knoppndvlem4.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
6 knoppndvlem4.n 
 |-  ( ph -> N e. NN )
7 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
8 0zd 
 |-  ( ph -> 0 e. ZZ )
9 5 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
10 9 simpld 
 |-  ( ph -> C e. RR )
11 1 2 6 10 knoppcnlem8 
 |-  ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) : NN0 --> ( CC ^m RR ) )
12 seqex 
 |-  seq 0 ( + , ( F ` A ) ) e. _V
13 12 a1i 
 |-  ( ph -> seq 0 ( + , ( F ` A ) ) e. _V )
14 6 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> N e. NN )
15 10 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> C e. RR )
16 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
17 1 2 14 15 16 knoppcnlem7 
 |-  ( ( ph /\ k e. NN0 ) -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) = ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) ) )
18 17 fveq1d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) ` A ) = ( ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) ) ` A ) )
19 eqid 
 |-  ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) ) = ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) )
20 fveq2 
 |-  ( v = A -> ( F ` v ) = ( F ` A ) )
21 20 seqeq3d 
 |-  ( v = A -> seq 0 ( + , ( F ` v ) ) = seq 0 ( + , ( F ` A ) ) )
22 21 fveq1d 
 |-  ( v = A -> ( seq 0 ( + , ( F ` v ) ) ` k ) = ( seq 0 ( + , ( F ` A ) ) ` k ) )
23 fvexd 
 |-  ( ph -> ( seq 0 ( + , ( F ` A ) ) ` k ) e. _V )
24 19 22 4 23 fvmptd3 
 |-  ( ph -> ( ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) ) ` A ) = ( seq 0 ( + , ( F ` A ) ) ` k ) )
25 24 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( v e. RR |-> ( seq 0 ( + , ( F ` v ) ) ` k ) ) ` A ) = ( seq 0 ( + , ( F ` A ) ) ` k ) )
26 18 25 eqtrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` k ) ` A ) = ( seq 0 ( + , ( F ` A ) ) ` k ) )
27 9 simprd 
 |-  ( ph -> ( abs ` C ) < 1 )
28 1 2 3 6 10 27 knoppcnlem9 
 |-  ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~>u ` RR ) W )
29 7 8 11 4 13 26 28 ulmclm 
 |-  ( ph -> seq 0 ( + , ( F ` A ) ) ~~> ( W ` A ) )