Metamath Proof Explorer

Theorem abelthlem4

Description: Lemma for abelth . (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses abelth.1 
|- ( ph -> A : NN0 --> CC )
abelth.2 
|- ( ph -> seq 0 ( + , A ) e. dom ~~> )
abelth.3 
|- ( ph -> M e. RR )
abelth.4 
|- ( ph -> 0 <_ M )
abelth.5 
|- S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }
abelth.6 
|- F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )
Assertion abelthlem4 
|- ( ph -> F : S --> CC )

Proof

Step Hyp Ref Expression
1 abelth.1 
 |-  ( ph -> A : NN0 --> CC )
2 abelth.2 
 |-  ( ph -> seq 0 ( + , A ) e. dom ~~> )
3 abelth.3 
 |-  ( ph -> M e. RR )
4 abelth.4 
 |-  ( ph -> 0 <_ M )
5 abelth.5 
 |-  S = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) }
6 abelth.6 
 |-  F = ( x e. S |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )
7 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
8 0zd 
 |-  ( ( ph /\ x e. S ) -> 0 e. ZZ )
9 fveq2 
 |-  ( m = n -> ( A ` m ) = ( A ` n ) )
10 oveq2 
 |-  ( m = n -> ( x ^ m ) = ( x ^ n ) )
11 9 10 oveq12d 
 |-  ( m = n -> ( ( A ` m ) x. ( x ^ m ) ) = ( ( A ` n ) x. ( x ^ n ) ) )
12 eqid 
 |-  ( m e. NN0 |-> ( ( A ` m ) x. ( x ^ m ) ) ) = ( m e. NN0 |-> ( ( A ` m ) x. ( x ^ m ) ) )
13 ovex 
 |-  ( ( A ` n ) x. ( x ^ n ) ) e. _V
14 11 12 13 fvmpt 
 |-  ( n e. NN0 -> ( ( m e. NN0 |-> ( ( A ` m ) x. ( x ^ m ) ) ) ` n ) = ( ( A ` n ) x. ( x ^ n ) ) )
15 14 adantl 
 |-  ( ( ( ph /\ x e. S ) /\ n e. NN0 ) -> ( ( m e. NN0 |-> ( ( A ` m ) x. ( x ^ m ) ) ) ` n ) = ( ( A ` n ) x. ( x ^ n ) ) )
16 1 adantr 
 |-  ( ( ph /\ x e. S ) -> A : NN0 --> CC )
17 16 ffvelrnda 
 |-  ( ( ( ph /\ x e. S ) /\ n e. NN0 ) -> ( A ` n ) e. CC )
18 5 ssrab3 
 |-  S C_ CC
19 18 a1i 
 |-  ( ph -> S C_ CC )
20 19 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. CC )
21 expcl 
 |-  ( ( x e. CC /\ n e. NN0 ) -> ( x ^ n ) e. CC )
22 20 21 sylan 
 |-  ( ( ( ph /\ x e. S ) /\ n e. NN0 ) -> ( x ^ n ) e. CC )
23 17 22 mulcld 
 |-  ( ( ( ph /\ x e. S ) /\ n e. NN0 ) -> ( ( A ` n ) x. ( x ^ n ) ) e. CC )
24 1 2 3 4 5 abelthlem3 
 |-  ( ( ph /\ x e. S ) -> seq 0 ( + , ( m e. NN0 |-> ( ( A ` m ) x. ( x ^ m ) ) ) ) e. dom ~~> )
25 7 8 15 23 24 isumcl 
 |-  ( ( ph /\ x e. S ) -> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) e. CC )
26 25 6 fmptd 
 |-  ( ph -> F : S --> CC )