Metamath Proof Explorer

Theorem abelth2

Description: Abel's theorem, restricted to the [ 0 , 1 ] interval. (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Hypotheses abelth2.1 
|- ( ph -> A : NN0 --> CC )
abelth2.2 
|- ( ph -> seq 0 ( + , A ) e. dom ~~> )
abelth2.3 
|- F = ( x e. ( 0 [,] 1 ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )
Assertion abelth2 
|- ( ph -> F e. ( ( 0 [,] 1 ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 abelth2.1 
 |-  ( ph -> A : NN0 --> CC )
2 abelth2.2 
 |-  ( ph -> seq 0 ( + , A ) e. dom ~~> )
3 abelth2.3 
 |-  F = ( x e. ( 0 [,] 1 ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )
4 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
5 ax-resscn 
 |-  RR C_ CC
6 4 5 sstri 
 |-  ( 0 [,] 1 ) C_ CC
7 6 a1i 
 |-  ( ph -> ( 0 [,] 1 ) C_ CC )
8 1re 
 |-  1 e. RR
9 elicc01 
 |-  ( z e. ( 0 [,] 1 ) <-> ( z e. RR /\ 0 <_ z /\ z <_ 1 ) )
10 9 bilani 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( z e. RR /\ 0 <_ z /\ z <_ 1 ) )
11 10 simp1d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> z e. RR )
12 resubcl 
 |-  ( ( 1 e. RR /\ z e. RR ) -> ( 1 - z ) e. RR )
13 8 11 12 sylancr 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 - z ) e. RR )
14 13 leidd 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 - z ) <_ ( 1 - z ) )
15 1red 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> 1 e. RR )
16 10 simp3d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> z <_ 1 )
17 11 15 16 abssubge0d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( abs ` ( 1 - z ) ) = ( 1 - z ) )
18 10 simp2d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> 0 <_ z )
19 11 18 absidd 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( abs ` z ) = z )
20 19 oveq2d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 - ( abs ` z ) ) = ( 1 - z ) )
21 20 oveq2d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 x. ( 1 - ( abs ` z ) ) ) = ( 1 x. ( 1 - z ) ) )
22 13 recnd 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 - z ) e. CC )
23 22 mullidd 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 x. ( 1 - z ) ) = ( 1 - z ) )
24 21 23 eqtrd 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 x. ( 1 - ( abs ` z ) ) ) = ( 1 - z ) )
25 14 17 24 3brtr4d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) )
26 7 25 ssrabdv 
 |-  ( ph -> ( 0 [,] 1 ) C_ { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } )
27 26 resmptd 
 |-  ( ph -> ( ( x e. { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( 0 [,] 1 ) ) = ( x e. ( 0 [,] 1 ) |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) )
28 27 3 eqtr4di 
 |-  ( ph -> ( ( x e. { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( 0 [,] 1 ) ) = F )
29 1red 
 |-  ( ph -> 1 e. RR )
30 0le1 
 |-  0 <_ 1
31 30 a1i 
 |-  ( ph -> 0 <_ 1 )
32 eqid 
 |-  { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) }
33 eqid 
 |-  ( x e. { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) = ( x e. { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) )
34 1 2 29 31 32 33 abelth 
 |-  ( ph -> ( x e. { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) e. ( { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } -cn-> CC ) )
35 rescncf 
 |-  ( ( 0 [,] 1 ) C_ { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } -> ( ( x e. { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) e. ( { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } -cn-> CC ) -> ( ( x e. { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) )
36 26 34 35 sylc 
 |-  ( ph -> ( ( x e. { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } |-> sum_ n e. NN0 ( ( A ` n ) x. ( x ^ n ) ) ) |` ( 0 [,] 1 ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
37 28 36 eqeltrrd 
 |-  ( ph -> F e. ( ( 0 [,] 1 ) -cn-> CC ) )