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