Step |
Hyp |
Ref |
Expression |
1 |
|
pser.g |
|- G = ( x e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( x ^ n ) ) ) ) |
2 |
|
radcnv.a |
|- ( ph -> A : NN0 --> CC ) |
3 |
|
psergf.x |
|- ( ph -> X e. CC ) |
4 |
|
radcnvlem2.y |
|- ( ph -> Y e. CC ) |
5 |
|
radcnvlem2.a |
|- ( ph -> ( abs ` X ) < ( abs ` Y ) ) |
6 |
|
radcnvlem2.c |
|- ( ph -> seq 0 ( + , ( G ` Y ) ) e. dom ~~> ) |
7 |
|
nn0uz |
|- NN0 = ( ZZ>= ` 0 ) |
8 |
|
1nn0 |
|- 1 e. NN0 |
9 |
8
|
a1i |
|- ( ph -> 1 e. NN0 ) |
10 |
|
id |
|- ( m = k -> m = k ) |
11 |
|
2fveq3 |
|- ( m = k -> ( abs ` ( ( G ` X ) ` m ) ) = ( abs ` ( ( G ` X ) ` k ) ) ) |
12 |
10 11
|
oveq12d |
|- ( m = k -> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) |
13 |
|
eqid |
|- ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) = ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) |
14 |
|
ovex |
|- ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) e. _V |
15 |
12 13 14
|
fvmpt |
|- ( k e. NN0 -> ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) |
16 |
15
|
adantl |
|- ( ( ph /\ k e. NN0 ) -> ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) |
17 |
|
nn0re |
|- ( k e. NN0 -> k e. RR ) |
18 |
17
|
adantl |
|- ( ( ph /\ k e. NN0 ) -> k e. RR ) |
19 |
1 2 3
|
psergf |
|- ( ph -> ( G ` X ) : NN0 --> CC ) |
20 |
19
|
ffvelrnda |
|- ( ( ph /\ k e. NN0 ) -> ( ( G ` X ) ` k ) e. CC ) |
21 |
20
|
abscld |
|- ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( G ` X ) ` k ) ) e. RR ) |
22 |
18 21
|
remulcld |
|- ( ( ph /\ k e. NN0 ) -> ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) e. RR ) |
23 |
16 22
|
eqeltrd |
|- ( ( ph /\ k e. NN0 ) -> ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) e. RR ) |
24 |
|
fvco3 |
|- ( ( ( G ` X ) : NN0 --> CC /\ k e. NN0 ) -> ( ( abs o. ( G ` X ) ) ` k ) = ( abs ` ( ( G ` X ) ` k ) ) ) |
25 |
19 24
|
sylan |
|- ( ( ph /\ k e. NN0 ) -> ( ( abs o. ( G ` X ) ) ` k ) = ( abs ` ( ( G ` X ) ` k ) ) ) |
26 |
21
|
recnd |
|- ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( G ` X ) ` k ) ) e. CC ) |
27 |
25 26
|
eqeltrd |
|- ( ( ph /\ k e. NN0 ) -> ( ( abs o. ( G ` X ) ) ` k ) e. CC ) |
28 |
12
|
cbvmptv |
|- ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) = ( k e. NN0 |-> ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) |
29 |
1 2 3 4 5 6 28
|
radcnvlem1 |
|- ( ph -> seq 0 ( + , ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ) e. dom ~~> ) |
30 |
|
1red |
|- ( ph -> 1 e. RR ) |
31 |
|
1red |
|- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> 1 e. RR ) |
32 |
|
elnnuz |
|- ( k e. NN <-> k e. ( ZZ>= ` 1 ) ) |
33 |
|
nnnn0 |
|- ( k e. NN -> k e. NN0 ) |
34 |
32 33
|
sylbir |
|- ( k e. ( ZZ>= ` 1 ) -> k e. NN0 ) |
35 |
34 18
|
sylan2 |
|- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> k e. RR ) |
36 |
34 21
|
sylan2 |
|- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( ( G ` X ) ` k ) ) e. RR ) |
37 |
20
|
absge0d |
|- ( ( ph /\ k e. NN0 ) -> 0 <_ ( abs ` ( ( G ` X ) ` k ) ) ) |
38 |
34 37
|
sylan2 |
|- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> 0 <_ ( abs ` ( ( G ` X ) ` k ) ) ) |
39 |
|
eluzle |
|- ( k e. ( ZZ>= ` 1 ) -> 1 <_ k ) |
40 |
39
|
adantl |
|- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> 1 <_ k ) |
41 |
31 35 36 38 40
|
lemul1ad |
|- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( 1 x. ( abs ` ( ( G ` X ) ` k ) ) ) <_ ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) |
42 |
|
absidm |
|- ( ( ( G ` X ) ` k ) e. CC -> ( abs ` ( abs ` ( ( G ` X ) ` k ) ) ) = ( abs ` ( ( G ` X ) ` k ) ) ) |
43 |
20 42
|
syl |
|- ( ( ph /\ k e. NN0 ) -> ( abs ` ( abs ` ( ( G ` X ) ` k ) ) ) = ( abs ` ( ( G ` X ) ` k ) ) ) |
44 |
25
|
fveq2d |
|- ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( abs o. ( G ` X ) ) ` k ) ) = ( abs ` ( abs ` ( ( G ` X ) ` k ) ) ) ) |
45 |
26
|
mulid2d |
|- ( ( ph /\ k e. NN0 ) -> ( 1 x. ( abs ` ( ( G ` X ) ` k ) ) ) = ( abs ` ( ( G ` X ) ` k ) ) ) |
46 |
43 44 45
|
3eqtr4d |
|- ( ( ph /\ k e. NN0 ) -> ( abs ` ( ( abs o. ( G ` X ) ) ` k ) ) = ( 1 x. ( abs ` ( ( G ` X ) ` k ) ) ) ) |
47 |
34 46
|
sylan2 |
|- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( ( abs o. ( G ` X ) ) ` k ) ) = ( 1 x. ( abs ` ( ( G ` X ) ` k ) ) ) ) |
48 |
16
|
oveq2d |
|- ( ( ph /\ k e. NN0 ) -> ( 1 x. ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) ) = ( 1 x. ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) ) |
49 |
22
|
recnd |
|- ( ( ph /\ k e. NN0 ) -> ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) e. CC ) |
50 |
49
|
mulid2d |
|- ( ( ph /\ k e. NN0 ) -> ( 1 x. ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) |
51 |
48 50
|
eqtrd |
|- ( ( ph /\ k e. NN0 ) -> ( 1 x. ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) |
52 |
34 51
|
sylan2 |
|- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( 1 x. ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) ) = ( k x. ( abs ` ( ( G ` X ) ` k ) ) ) ) |
53 |
41 47 52
|
3brtr4d |
|- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( abs ` ( ( abs o. ( G ` X ) ) ` k ) ) <_ ( 1 x. ( ( m e. NN0 |-> ( m x. ( abs ` ( ( G ` X ) ` m ) ) ) ) ` k ) ) ) |
54 |
7 9 23 27 29 30 53
|
cvgcmpce |
|- ( ph -> seq 0 ( + , ( abs o. ( G ` X ) ) ) e. dom ~~> ) |