Metamath Proof Explorer

Theorem abelthlem3

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 ) ) ) }
Assertion abelthlem3 
|- ( ( ph /\ X e. S ) -> seq 0 ( + , ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) ) e. dom ~~> )

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 1 2 3 4 5 abelthlem2 
 |-  ( ph -> ( 1 e. S /\ ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )
7 6 simprd 
 |-  ( ph -> ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) )
8 ssundif 
 |-  ( S C_ ( { 1 } u. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) <-> ( S \ { 1 } ) C_ ( 0 ( ball ` ( abs o. - ) ) 1 ) )
9 7 8 sylibr 
 |-  ( ph -> S C_ ( { 1 } u. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )
10 9 sselda 
 |-  ( ( ph /\ X e. S ) -> X e. ( { 1 } u. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )
11 elun 
 |-  ( X e. ( { 1 } u. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) <-> ( X e. { 1 } \/ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )
12 10 11 sylib 
 |-  ( ( ph /\ X e. S ) -> ( X e. { 1 } \/ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) )
13 1 feqmptd 
 |-  ( ph -> A = ( n e. NN0 |-> ( A ` n ) ) )
14 1 ffvelrnda 
 |-  ( ( ph /\ n e. NN0 ) -> ( A ` n ) e. CC )
15 14 mulid1d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( A ` n ) x. 1 ) = ( A ` n ) )
16 15 mpteq2dva 
 |-  ( ph -> ( n e. NN0 |-> ( ( A ` n ) x. 1 ) ) = ( n e. NN0 |-> ( A ` n ) ) )
17 13 16 eqtr4d 
 |-  ( ph -> A = ( n e. NN0 |-> ( ( A ` n ) x. 1 ) ) )
18 elsni 
 |-  ( X e. { 1 } -> X = 1 )
19 18 oveq1d 
 |-  ( X e. { 1 } -> ( X ^ n ) = ( 1 ^ n ) )
20 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
21 1exp 
 |-  ( n e. ZZ -> ( 1 ^ n ) = 1 )
22 20 21 syl 
 |-  ( n e. NN0 -> ( 1 ^ n ) = 1 )
23 19 22 sylan9eq 
 |-  ( ( X e. { 1 } /\ n e. NN0 ) -> ( X ^ n ) = 1 )
24 23 oveq2d 
 |-  ( ( X e. { 1 } /\ n e. NN0 ) -> ( ( A ` n ) x. ( X ^ n ) ) = ( ( A ` n ) x. 1 ) )
25 24 mpteq2dva 
 |-  ( X e. { 1 } -> ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) = ( n e. NN0 |-> ( ( A ` n ) x. 1 ) ) )
26 25 eqcomd 
 |-  ( X e. { 1 } -> ( n e. NN0 |-> ( ( A ` n ) x. 1 ) ) = ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) )
27 17 26 sylan9eq 
 |-  ( ( ph /\ X e. { 1 } ) -> A = ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) )
28 27 seqeq3d 
 |-  ( ( ph /\ X e. { 1 } ) -> seq 0 ( + , A ) = seq 0 ( + , ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) ) )
29 2 adantr 
 |-  ( ( ph /\ X e. { 1 } ) -> seq 0 ( + , A ) e. dom ~~> )
30 28 29 eqeltrrd 
 |-  ( ( ph /\ X e. { 1 } ) -> seq 0 ( + , ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) ) e. dom ~~> )
31 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
32 0cn 
 |-  0 e. CC
33 1xr 
 |-  1 e. RR*
34 blssm 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 0 e. CC /\ 1 e. RR* ) -> ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC )
35 31 32 33 34 mp3an 
 |-  ( 0 ( ball ` ( abs o. - ) ) 1 ) C_ CC
36 simpr 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) )
37 35 36 sseldi 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> X e. CC )
38 oveq1 
 |-  ( z = X -> ( z ^ n ) = ( X ^ n ) )
39 38 oveq2d 
 |-  ( z = X -> ( ( A ` n ) x. ( z ^ n ) ) = ( ( A ` n ) x. ( X ^ n ) ) )
40 39 mpteq2dv 
 |-  ( z = X -> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) = ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) )
41 eqid 
 |-  ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) = ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) )
42 nn0ex 
 |-  NN0 e. _V
43 42 mptex 
 |-  ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) e. _V
44 40 41 43 fvmpt 
 |-  ( X e. CC -> ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` X ) = ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) )
45 37 44 syl 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` X ) = ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) )
46 45 seqeq3d 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` X ) ) = seq 0 ( + , ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) ) )
47 1 adantr 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> A : NN0 --> CC )
48 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* , < )
49 37 abscld 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( abs ` X ) e. RR )
50 49 rexrd 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( abs ` X ) e. RR* )
51 1re 
 |-  1 e. RR
52 rexr 
 |-  ( 1 e. RR -> 1 e. RR* )
53 51 52 mp1i 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> 1 e. RR* )
54 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
55 41 47 48 radcnvcl 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. ( 0 [,] +oo ) )
56 54 55 sseldi 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. RR* )
57 eqid 
 |-  ( abs o. - ) = ( abs o. - )
58 57 cnmetdval 
 |-  ( ( X e. CC /\ 0 e. CC ) -> ( X ( abs o. - ) 0 ) = ( abs ` ( X - 0 ) ) )
59 37 32 58 sylancl 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( X ( abs o. - ) 0 ) = ( abs ` ( X - 0 ) ) )
60 37 subid1d 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( X - 0 ) = X )
61 60 fveq2d 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( abs ` ( X - 0 ) ) = ( abs ` X ) )
62 59 61 eqtrd 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( X ( abs o. - ) 0 ) = ( abs ` X ) )
63 elbl3 
 |-  ( ( ( ( abs o. - ) e. ( *Met ` CC ) /\ 1 e. RR* ) /\ ( 0 e. CC /\ X e. CC ) ) -> ( X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( X ( abs o. - ) 0 ) < 1 ) )
64 31 33 63 mpanl12 
 |-  ( ( 0 e. CC /\ X e. CC ) -> ( X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( X ( abs o. - ) 0 ) < 1 ) )
65 32 37 64 sylancr 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) <-> ( X ( abs o. - ) 0 ) < 1 ) )
66 36 65 mpbid 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( X ( abs o. - ) 0 ) < 1 )
67 62 66 eqbrtrrd 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( abs ` X ) < 1 )
68 1 2 abelthlem1 
 |-  ( ph -> 1 <_ sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
69 68 adantr 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> 1 <_ sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
70 50 53 56 67 69 xrltletrd 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> ( abs ` X ) < sup ( { r e. RR | seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
71 41 47 48 37 70 radcnvlt2 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> seq 0 ( + , ( ( z e. CC |-> ( n e. NN0 |-> ( ( A ` n ) x. ( z ^ n ) ) ) ) ` X ) ) e. dom ~~> )
72 46 71 eqeltrrd 
 |-  ( ( ph /\ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) -> seq 0 ( + , ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) ) e. dom ~~> )
73 30 72 jaodan 
 |-  ( ( ph /\ ( X e. { 1 } \/ X e. ( 0 ( ball ` ( abs o. - ) ) 1 ) ) ) -> seq 0 ( + , ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) ) e. dom ~~> )
74 12 73 syldan 
 |-  ( ( ph /\ X e. S ) -> seq 0 ( + , ( n e. NN0 |-> ( ( A ` n ) x. ( X ^ n ) ) ) ) e. dom ~~> )