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 ) ) ) ) )