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 simpr 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> z e. ( 0 [,] 1 ) )
10 elicc01 
 |-  ( z e. ( 0 [,] 1 ) <-> ( z e. RR /\ 0 <_ z /\ z <_ 1 ) )
11 9 10 sylib 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( z e. RR /\ 0 <_ z /\ z <_ 1 ) )
12 11 simp1d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> z e. RR )
13 resubcl 
 |-  ( ( 1 e. RR /\ z e. RR ) -> ( 1 - z ) e. RR )
14 8 12 13 sylancr 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 - z ) e. RR )
15 14 leidd 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 - z ) <_ ( 1 - z ) )
16 1red 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> 1 e. RR )
17 11 simp3d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> z <_ 1 )
18 12 16 17 abssubge0d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( abs ` ( 1 - z ) ) = ( 1 - z ) )
19 11 simp2d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> 0 <_ z )
20 12 19 absidd 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( abs ` z ) = z )
21 20 oveq2d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 - ( abs ` z ) ) = ( 1 - z ) )
22 21 oveq2d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 x. ( 1 - ( abs ` z ) ) ) = ( 1 x. ( 1 - z ) ) )
23 14 recnd 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 - z ) e. CC )
24 23 mulid2d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 x. ( 1 - z ) ) = ( 1 - z ) )
25 22 24 eqtrd 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( 1 x. ( 1 - ( abs ` z ) ) ) = ( 1 - z ) )
26 15 18 25 3brtr4d 
 |-  ( ( ph /\ z e. ( 0 [,] 1 ) ) -> ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) )
27 7 26 ssrabdv 
 |-  ( ph -> ( 0 [,] 1 ) C_ { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } )
28 27 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 ) ) ) )
29 28 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 )
30 1red 
 |-  ( ph -> 1 e. RR )
31 0le1 
 |-  0 <_ 1
32 31 a1i 
 |-  ( ph -> 0 <_ 1 )
33 eqid 
 |-  { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) } = { z e. CC | ( abs ` ( 1 - z ) ) <_ ( 1 x. ( 1 - ( abs ` z ) ) ) }
34 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 ) ) )
35 1 2 30 32 33 34 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 ) )
36 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 ) ) )
37 27 35 36 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 ) )
38 29 37 eqeltrrd 
 |-  ( ph -> F e. ( ( 0 [,] 1 ) -cn-> CC ) )