Metamath Proof Explorer


Theorem abelthlem7a

Description: Lemma for abelth . (Contributed by Mario Carneiro, 8-May-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 ) ) )
abelth.7
|- ( ph -> seq 0 ( + , A ) ~~> 0 )
abelthlem6.1
|- ( ph -> X e. ( S \ { 1 } ) )
Assertion abelthlem7a
|- ( ph -> ( X e. CC /\ ( abs ` ( 1 - X ) ) <_ ( M x. ( 1 - ( abs ` X ) ) ) ) )

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 abelth.7
 |-  ( ph -> seq 0 ( + , A ) ~~> 0 )
8 abelthlem6.1
 |-  ( ph -> X e. ( S \ { 1 } ) )
9 8 eldifad
 |-  ( ph -> X e. S )
10 oveq2
 |-  ( z = X -> ( 1 - z ) = ( 1 - X ) )
11 10 fveq2d
 |-  ( z = X -> ( abs ` ( 1 - z ) ) = ( abs ` ( 1 - X ) ) )
12 fveq2
 |-  ( z = X -> ( abs ` z ) = ( abs ` X ) )
13 12 oveq2d
 |-  ( z = X -> ( 1 - ( abs ` z ) ) = ( 1 - ( abs ` X ) ) )
14 13 oveq2d
 |-  ( z = X -> ( M x. ( 1 - ( abs ` z ) ) ) = ( M x. ( 1 - ( abs ` X ) ) ) )
15 11 14 breq12d
 |-  ( z = X -> ( ( abs ` ( 1 - z ) ) <_ ( M x. ( 1 - ( abs ` z ) ) ) <-> ( abs ` ( 1 - X ) ) <_ ( M x. ( 1 - ( abs ` X ) ) ) ) )
16 15 5 elrab2
 |-  ( X e. S <-> ( X e. CC /\ ( abs ` ( 1 - X ) ) <_ ( M x. ( 1 - ( abs ` X ) ) ) ) )
17 9 16 sylib
 |-  ( ph -> ( X e. CC /\ ( abs ` ( 1 - X ) ) <_ ( M x. ( 1 - ( abs ` X ) ) ) ) )