Metamath Proof Explorer

Theorem knoppcnlem6

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

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

Proof

Step Hyp Ref Expression
1 knoppcnlem6.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppcnlem6.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppcnlem6.n 
 |-  ( ph -> N e. NN )
4 knoppcnlem6.1 
 |-  ( ph -> C e. RR )
5 knoppcnlem6.2 
 |-  ( ph -> ( abs ` C ) < 1 )
6 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
7 0zd 
 |-  ( ph -> 0 e. ZZ )
8 reex 
 |-  RR e. _V
9 8 a1i 
 |-  ( ph -> RR e. _V )
10 1 2 3 4 knoppcnlem5 
 |-  ( ph -> ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) : NN0 --> ( CC ^m RR ) )
11 nn0ex 
 |-  NN0 e. _V
12 11 mptex 
 |-  ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) e. _V
13 12 a1i 
 |-  ( ph -> ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) e. _V )
14 eqid 
 |-  ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) = ( m e. NN0 |-> ( ( abs ` C ) ^ m ) )
15 14 a1i 
 |-  ( ( ph /\ k e. NN0 ) -> ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) = ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) )
16 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ m = k ) -> m = k )
17 16 oveq2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ m = k ) -> ( ( abs ` C ) ^ m ) = ( ( abs ` C ) ^ k ) )
18 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
19 ovexd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( abs ` C ) ^ k ) e. _V )
20 15 17 18 19 fvmptd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ` k ) = ( ( abs ` C ) ^ k ) )
21 4 recnd 
 |-  ( ph -> C e. CC )
22 21 abscld 
 |-  ( ph -> ( abs ` C ) e. RR )
23 22 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> ( abs ` C ) e. RR )
24 23 18 reexpcld 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( abs ` C ) ^ k ) e. RR )
25 20 24 eqeltrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ` k ) e. RR )
26 eqid 
 |-  ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) = ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) )
27 26 a1i 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) = ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) )
28 simpr 
 |-  ( ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) /\ m = k ) -> m = k )
29 28 fveq2d 
 |-  ( ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) /\ m = k ) -> ( ( F ` z ) ` m ) = ( ( F ` z ) ` k ) )
30 29 mpteq2dv 
 |-  ( ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) /\ m = k ) -> ( z e. RR |-> ( ( F ` z ) ` m ) ) = ( z e. RR |-> ( ( F ` z ) ` k ) ) )
31 18 adantrr 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> k e. NN0 )
32 8 mptex 
 |-  ( z e. RR |-> ( ( F ` z ) ` k ) ) e. _V
33 32 a1i 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> ( z e. RR |-> ( ( F ` z ) ` k ) ) e. _V )
34 27 30 31 33 fvmptd 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> ( ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ` k ) = ( z e. RR |-> ( ( F ` z ) ` k ) ) )
35 simpr 
 |-  ( ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) /\ z = w ) -> z = w )
36 35 fveq2d 
 |-  ( ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) /\ z = w ) -> ( F ` z ) = ( F ` w ) )
37 36 fveq1d 
 |-  ( ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) /\ z = w ) -> ( ( F ` z ) ` k ) = ( ( F ` w ) ` k ) )
38 simprr 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> w e. RR )
39 fvexd 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> ( ( F ` w ) ` k ) e. _V )
40 34 37 38 39 fvmptd 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> ( ( ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ` k ) ` w ) = ( ( F ` w ) ` k ) )
41 40 fveq2d 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> ( abs ` ( ( ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ` k ) ` w ) ) = ( abs ` ( ( F ` w ) ` k ) ) )
42 3 adantr 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> N e. NN )
43 4 adantr 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> C e. RR )
44 1 2 42 43 38 31 knoppcnlem4 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> ( abs ` ( ( F ` w ) ` k ) ) <_ ( ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ` k ) )
45 41 44 eqbrtrd 
 |-  ( ( ph /\ ( k e. NN0 /\ w e. RR ) ) -> ( abs ` ( ( ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ` k ) ` w ) ) <_ ( ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ` k ) )
46 22 recnd 
 |-  ( ph -> ( abs ` C ) e. CC )
47 absidm 
 |-  ( C e. CC -> ( abs ` ( abs ` C ) ) = ( abs ` C ) )
48 21 47 syl 
 |-  ( ph -> ( abs ` ( abs ` C ) ) = ( abs ` C ) )
49 48 5 eqbrtrd 
 |-  ( ph -> ( abs ` ( abs ` C ) ) < 1 )
50 46 49 20 geolim 
 |-  ( ph -> seq 0 ( + , ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ) ~~> ( 1 / ( 1 - ( abs ` C ) ) ) )
51 seqex 
 |-  seq 0 ( + , ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ) e. _V
52 ovex 
 |-  ( 1 / ( 1 - ( abs ` C ) ) ) e. _V
53 51 52 breldm 
 |-  ( seq 0 ( + , ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ) ~~> ( 1 / ( 1 - ( abs ` C ) ) ) -> seq 0 ( + , ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ) e. dom ~~> )
54 50 53 syl 
 |-  ( ph -> seq 0 ( + , ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ) e. dom ~~> )
55 6 7 9 10 13 25 45 54 mtest 
 |-  ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) e. dom ( ~~>u ` RR ) )