Metamath Proof Explorer

Theorem clim2ser2

Description: The limit of an infinite series with an initial segment added. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 
|- Z = ( ZZ>= ` M )
clim2ser.2 
|- ( ph -> N e. Z )
clim2ser.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
clim2ser2.5 
|- ( ph -> seq ( N + 1 ) ( + , F ) ~~> A )
Assertion clim2ser2 
|- ( ph -> seq M ( + , F ) ~~> ( A + ( seq M ( + , F ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 clim2ser.1 
 |-  Z = ( ZZ>= ` M )
2 clim2ser.2 
 |-  ( ph -> N e. Z )
3 clim2ser.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
4 clim2ser2.5 
 |-  ( ph -> seq ( N + 1 ) ( + , F ) ~~> A )
5 eqid 
 |-  ( ZZ>= ` ( N + 1 ) ) = ( ZZ>= ` ( N + 1 ) )
6 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
7 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
8 6 7 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
9 eluzelz 
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( N + 1 ) e. ZZ )
10 8 9 syl 
 |-  ( ph -> ( N + 1 ) e. ZZ )
11 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
12 6 11 syl 
 |-  ( ph -> M e. ZZ )
13 1 12 3 serf 
 |-  ( ph -> seq M ( + , F ) : Z --> CC )
14 13 2 ffvelrnd 
 |-  ( ph -> ( seq M ( + , F ) ` N ) e. CC )
15 seqex 
 |-  seq M ( + , F ) e. _V
16 15 a1i 
 |-  ( ph -> seq M ( + , F ) e. _V )
17 8 1 eleqtrrdi 
 |-  ( ph -> ( N + 1 ) e. Z )
18 1 uztrn2 
 |-  ( ( ( N + 1 ) e. Z /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. Z )
19 17 18 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. Z )
20 19 3 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> ( F ` k ) e. CC )
21 5 10 20 serf 
 |-  ( ph -> seq ( N + 1 ) ( + , F ) : ( ZZ>= ` ( N + 1 ) ) --> CC )
22 21 ffvelrnda 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq ( N + 1 ) ( + , F ) ` j ) e. CC )
23 14 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( + , F ) ` N ) e. CC )
24 addcl 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k + x ) e. CC )
25 24 adantl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k + x ) e. CC )
26 addass 
 |-  ( ( k e. CC /\ x e. CC /\ y e. CC ) -> ( ( k + x ) + y ) = ( k + ( x + y ) ) )
27 26 adantl 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) /\ ( k e. CC /\ x e. CC /\ y e. CC ) ) -> ( ( k + x ) + y ) = ( k + ( x + y ) ) )
28 simpr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> j e. ( ZZ>= ` ( N + 1 ) ) )
29 6 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> N e. ( ZZ>= ` M ) )
30 elfzuz 
 |-  ( k e. ( M ... j ) -> k e. ( ZZ>= ` M ) )
31 30 1 eleqtrrdi 
 |-  ( k e. ( M ... j ) -> k e. Z )
32 31 3 sylan2 
 |-  ( ( ph /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
33 32 adantlr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
34 25 27 28 29 33 seqsplit 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( + , F ) ` j ) = ( ( seq M ( + , F ) ` N ) + ( seq ( N + 1 ) ( + , F ) ` j ) ) )
35 23 22 34 comraddd 
 |-  ( ( ph /\ j e. ( ZZ>= ` ( N + 1 ) ) ) -> ( seq M ( + , F ) ` j ) = ( ( seq ( N + 1 ) ( + , F ) ` j ) + ( seq M ( + , F ) ` N ) ) )
36 5 10 4 14 16 22 35 climaddc1 
 |-  ( ph -> seq M ( + , F ) ~~> ( A + ( seq M ( + , F ) ` N ) ) )