Metamath Proof Explorer

Theorem climfsum

Description: Limit of a finite sum of converging sequences. Note that F ( k ) is a collection of functions with implicit parameter k , each of which converges to B ( k ) as n ~> +oo . (Contributed by Mario Carneiro, 22-Jul-2014) (Proof shortened by Mario Carneiro, 22-May-2016)

Ref Expression
Hypotheses climfsum.1 
|- Z = ( ZZ>= ` M )
climfsum.2 
|- ( ph -> M e. ZZ )
climfsum.3 
|- ( ph -> A e. Fin )
climfsum.5 
|- ( ( ph /\ k e. A ) -> F ~~> B )
climfsum.6 
|- ( ph -> H e. W )
climfsum.7 
|- ( ( ph /\ ( k e. A /\ n e. Z ) ) -> ( F ` n ) e. CC )
climfsum.8 
|- ( ( ph /\ n e. Z ) -> ( H ` n ) = sum_ k e. A ( F ` n ) )
Assertion climfsum 
|- ( ph -> H ~~> sum_ k e. A B )

Proof

Step Hyp Ref Expression
1 climfsum.1 
 |-  Z = ( ZZ>= ` M )
2 climfsum.2 
 |-  ( ph -> M e. ZZ )
3 climfsum.3 
 |-  ( ph -> A e. Fin )
4 climfsum.5 
 |-  ( ( ph /\ k e. A ) -> F ~~> B )
5 climfsum.6 
 |-  ( ph -> H e. W )
6 climfsum.7 
 |-  ( ( ph /\ ( k e. A /\ n e. Z ) ) -> ( F ` n ) e. CC )
7 climfsum.8 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) = sum_ k e. A ( F ` n ) )
8 7 mpteq2dva 
 |-  ( ph -> ( n e. Z |-> ( H ` n ) ) = ( n e. Z |-> sum_ k e. A ( F ` n ) ) )
9 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
10 1 9 eqsstri 
 |-  Z C_ ZZ
11 zssre 
 |-  ZZ C_ RR
12 10 11 sstri 
 |-  Z C_ RR
13 12 a1i 
 |-  ( ph -> Z C_ RR )
14 fvexd 
 |-  ( ( ph /\ ( n e. Z /\ k e. A ) ) -> ( F ` n ) e. _V )
15 2 adantr 
 |-  ( ( ph /\ k e. A ) -> M e. ZZ )
16 climrel 
 |-  Rel ~~>
17 16 brrelex1i 
 |-  ( F ~~> B -> F e. _V )
18 4 17 syl 
 |-  ( ( ph /\ k e. A ) -> F e. _V )
19 eqid 
 |-  ( n e. Z |-> ( F ` n ) ) = ( n e. Z |-> ( F ` n ) )
20 1 19 climmpt 
 |-  ( ( M e. ZZ /\ F e. _V ) -> ( F ~~> B <-> ( n e. Z |-> ( F ` n ) ) ~~> B ) )
21 15 18 20 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( F ~~> B <-> ( n e. Z |-> ( F ` n ) ) ~~> B ) )
22 4 21 mpbid 
 |-  ( ( ph /\ k e. A ) -> ( n e. Z |-> ( F ` n ) ) ~~> B )
23 6 anassrs 
 |-  ( ( ( ph /\ k e. A ) /\ n e. Z ) -> ( F ` n ) e. CC )
24 23 fmpttd 
 |-  ( ( ph /\ k e. A ) -> ( n e. Z |-> ( F ` n ) ) : Z --> CC )
25 1 15 24 rlimclim 
 |-  ( ( ph /\ k e. A ) -> ( ( n e. Z |-> ( F ` n ) ) ~~>r B <-> ( n e. Z |-> ( F ` n ) ) ~~> B ) )
26 22 25 mpbird 
 |-  ( ( ph /\ k e. A ) -> ( n e. Z |-> ( F ` n ) ) ~~>r B )
27 13 3 14 26 fsumrlim 
 |-  ( ph -> ( n e. Z |-> sum_ k e. A ( F ` n ) ) ~~>r sum_ k e. A B )
28 3 adantr 
 |-  ( ( ph /\ n e. Z ) -> A e. Fin )
29 6 anass1rs 
 |-  ( ( ( ph /\ n e. Z ) /\ k e. A ) -> ( F ` n ) e. CC )
30 28 29 fsumcl 
 |-  ( ( ph /\ n e. Z ) -> sum_ k e. A ( F ` n ) e. CC )
31 30 fmpttd 
 |-  ( ph -> ( n e. Z |-> sum_ k e. A ( F ` n ) ) : Z --> CC )
32 1 2 31 rlimclim 
 |-  ( ph -> ( ( n e. Z |-> sum_ k e. A ( F ` n ) ) ~~>r sum_ k e. A B <-> ( n e. Z |-> sum_ k e. A ( F ` n ) ) ~~> sum_ k e. A B ) )
33 27 32 mpbid 
 |-  ( ph -> ( n e. Z |-> sum_ k e. A ( F ` n ) ) ~~> sum_ k e. A B )
34 8 33 eqbrtrd 
 |-  ( ph -> ( n e. Z |-> ( H ` n ) ) ~~> sum_ k e. A B )
35 eqid 
 |-  ( n e. Z |-> ( H ` n ) ) = ( n e. Z |-> ( H ` n ) )
36 1 35 climmpt 
 |-  ( ( M e. ZZ /\ H e. W ) -> ( H ~~> sum_ k e. A B <-> ( n e. Z |-> ( H ` n ) ) ~~> sum_ k e. A B ) )
37 2 5 36 syl2anc 
 |-  ( ph -> ( H ~~> sum_ k e. A B <-> ( n e. Z |-> ( H ` n ) ) ~~> sum_ k e. A B ) )
38 34 37 mpbird 
 |-  ( ph -> H ~~> sum_ k e. A B )