Metamath Proof Explorer

Theorem abelthlem1

Description: Lemma for abelth . (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Hypotheses abelth.1 
|- ( ph -> A : NN0 --> CC )
abelth.2 
|- ( ph -> seq 0 ( + , A ) e. dom ~~> )
Assertion abelthlem1 
|- ( ph -> 1 <_ sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )

Proof

Step Hyp Ref Expression
1 abelth.1 
 |-  ( ph -> A : NN0 --> CC )
2 abelth.2 
 |-  ( ph -> seq 0 ( + , A ) e. dom ~~> )
3 abs1 
 |-  ( abs ` 1 ) = 1
4 eqid 
 |-  ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) = ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) )
5 eqid 
 |-  sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) = sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < )
6 1cnd 
 |-  ( ph -> 1 e. CC )
7 1 feqmptd 
 |-  ( ph -> A = ( n e. NN0 |-> ( A ` n ) ) )
8 1 ffvelrnda 
 |-  ( ( ph /\ n e. NN0 ) -> ( A ` n ) e. CC )
9 8 mulid1d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( A ` n ) x. 1 ) = ( A ` n ) )
10 9 mpteq2dva 
 |-  ( ph -> ( n e. NN0 |-> ( ( A ` n ) x. 1 ) ) = ( n e. NN0 |-> ( A ` n ) ) )
11 7 10 eqtr4d 
 |-  ( ph -> A = ( n e. NN0 |-> ( ( A ` n ) x. 1 ) ) )
12 ax-1cn 
 |-  1 e. CC
13 oveq1 
 |-  ( z = 1 -> ( z ^ n ) = ( 1 ^ n ) )
14 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
15 1exp 
 |-  ( n e. ZZ -> ( 1 ^ n ) = 1 )
16 14 15 syl 
 |-  ( n e. NN0 -> ( 1 ^ n ) = 1 )
17 13 16 sylan9eq 
 |-  ( ( z = 1 /\ n e. NN0 ) -> ( z ^ n ) = 1 )
18 17 oveq2d 
 |-  ( ( z = 1 /\ n e. NN0 ) -> ( ( A ` n ) x. ( z ^ n ) ) = ( ( A ` n ) x. 1 ) )
19 18 mpteq2dva 
 |-  ( z = 1 -> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) = ( n e. NN0 |-> ( ( A ` n ) x. 1 ) ) )
20 nn0ex 
 |-  NN0 e. _V
21 20 mptex 
 |-  ( n e. NN0 |-> ( ( A ` n ) x. 1 ) ) e. _V
22 19 4 21 fvmpt 
 |-  ( 1 e. CC -> ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` 1 ) = ( n e. NN0 |-> ( ( A ` n ) x. 1 ) ) )
23 12 22 ax-mp 
 |-  ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` 1 ) = ( n e. NN0 |-> ( ( A ` n ) x. 1 ) )
24 11 23 eqtr4di 
 |-  ( ph -> A = ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` 1 ) )
25 24 seqeq3d 
 |-  ( ph -> seq 0 ( + , A ) = seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` 1 ) ) )
26 25 2 eqeltrrd 
 |-  ( ph -> seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` 1 ) ) e. dom ~~> )
27 4 1 5 6 26 radcnvle 
 |-  ( ph -> ( abs ` 1 ) <_ sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
28 3 27 eqbrtrrid 
 |-  ( ph -> 1 <_ sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )