Metamath Proof Explorer

Theorem fsumcvg4

Description: A serie with finite support is a finite sum, and therefore converges. (Contributed by Thierry Arnoux, 6-Sep-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses fsumcvg4.s 
|- S = ( ZZ>= ` M )
fsumcvg4.m 
|- ( ph -> M e. ZZ )
fsumcvg4.c 
|- ( ph -> F : S --> CC )
fsumcvg4.f 
|- ( ph -> ( `' F " ( CC \ { 0 } ) ) e. Fin )
Assertion fsumcvg4 
|- ( ph -> seq M ( + , F ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 fsumcvg4.s 
 |-  S = ( ZZ>= ` M )
2 fsumcvg4.m 
 |-  ( ph -> M e. ZZ )
3 fsumcvg4.c 
 |-  ( ph -> F : S --> CC )
4 fsumcvg4.f 
 |-  ( ph -> ( `' F " ( CC \ { 0 } ) ) e. Fin )
5 ffun 
 |-  ( F : S --> CC -> Fun F )
6 difpreima 
 |-  ( Fun F -> ( `' F " ( CC \ { 0 } ) ) = ( ( `' F " CC ) \ ( `' F " { 0 } ) ) )
7 3 5 6 3syl 
 |-  ( ph -> ( `' F " ( CC \ { 0 } ) ) = ( ( `' F " CC ) \ ( `' F " { 0 } ) ) )
8 difss 
 |-  ( ( `' F " CC ) \ ( `' F " { 0 } ) ) C_ ( `' F " CC )
9 7 8 eqsstrdi 
 |-  ( ph -> ( `' F " ( CC \ { 0 } ) ) C_ ( `' F " CC ) )
10 fimacnv 
 |-  ( F : S --> CC -> ( `' F " CC ) = S )
11 3 10 syl 
 |-  ( ph -> ( `' F " CC ) = S )
12 9 11 sseqtrd 
 |-  ( ph -> ( `' F " ( CC \ { 0 } ) ) C_ S )
13 exmidd 
 |-  ( ( ph /\ k e. S ) -> ( k e. ( `' F " ( CC \ { 0 } ) ) \/ -. k e. ( `' F " ( CC \ { 0 } ) ) ) )
14 eqid 
 |-  ( F ` k ) = ( F ` k )
15 14 biantru 
 |-  ( k e. ( `' F " ( CC \ { 0 } ) ) <-> ( k e. ( `' F " ( CC \ { 0 } ) ) /\ ( F ` k ) = ( F ` k ) ) )
16 15 a1i 
 |-  ( ( ph /\ k e. S ) -> ( k e. ( `' F " ( CC \ { 0 } ) ) <-> ( k e. ( `' F " ( CC \ { 0 } ) ) /\ ( F ` k ) = ( F ` k ) ) ) )
17 1 fvexi 
 |-  S e. _V
18 17 a1i 
 |-  ( ph -> S e. _V )
19 0nn0 
 |-  0 e. NN0
20 19 a1i 
 |-  ( ph -> 0 e. NN0 )
21 eqid 
 |-  ( CC \ { 0 } ) = ( CC \ { 0 } )
22 21 ffs2 
 |-  ( ( S e. _V /\ 0 e. NN0 /\ F : S --> CC ) -> ( F supp 0 ) = ( `' F " ( CC \ { 0 } ) ) )
23 18 20 3 22 syl3anc 
 |-  ( ph -> ( F supp 0 ) = ( `' F " ( CC \ { 0 } ) ) )
24 3 ffnd 
 |-  ( ph -> F Fn S )
25 suppvalfn 
 |-  ( ( F Fn S /\ S e. _V /\ 0 e. NN0 ) -> ( F supp 0 ) = { k e. S | ( F ` k ) =/= 0 } )
26 24 18 20 25 syl3anc 
 |-  ( ph -> ( F supp 0 ) = { k e. S | ( F ` k ) =/= 0 } )
27 23 26 eqtr3d 
 |-  ( ph -> ( `' F " ( CC \ { 0 } ) ) = { k e. S | ( F ` k ) =/= 0 } )
28 27 eleq2d 
 |-  ( ph -> ( k e. ( `' F " ( CC \ { 0 } ) ) <-> k e. { k e. S | ( F ` k ) =/= 0 } ) )
29 rabid 
 |-  ( k e. { k e. S | ( F ` k ) =/= 0 } <-> ( k e. S /\ ( F ` k ) =/= 0 ) )
30 28 29 bitrdi 
 |-  ( ph -> ( k e. ( `' F " ( CC \ { 0 } ) ) <-> ( k e. S /\ ( F ` k ) =/= 0 ) ) )
31 30 baibd 
 |-  ( ( ph /\ k e. S ) -> ( k e. ( `' F " ( CC \ { 0 } ) ) <-> ( F ` k ) =/= 0 ) )
32 31 necon2bbid 
 |-  ( ( ph /\ k e. S ) -> ( ( F ` k ) = 0 <-> -. k e. ( `' F " ( CC \ { 0 } ) ) ) )
33 32 biimprd 
 |-  ( ( ph /\ k e. S ) -> ( -. k e. ( `' F " ( CC \ { 0 } ) ) -> ( F ` k ) = 0 ) )
34 33 pm4.71d 
 |-  ( ( ph /\ k e. S ) -> ( -. k e. ( `' F " ( CC \ { 0 } ) ) <-> ( -. k e. ( `' F " ( CC \ { 0 } ) ) /\ ( F ` k ) = 0 ) ) )
35 16 34 orbi12d 
 |-  ( ( ph /\ k e. S ) -> ( ( k e. ( `' F " ( CC \ { 0 } ) ) \/ -. k e. ( `' F " ( CC \ { 0 } ) ) ) <-> ( ( k e. ( `' F " ( CC \ { 0 } ) ) /\ ( F ` k ) = ( F ` k ) ) \/ ( -. k e. ( `' F " ( CC \ { 0 } ) ) /\ ( F ` k ) = 0 ) ) ) )
36 13 35 mpbid 
 |-  ( ( ph /\ k e. S ) -> ( ( k e. ( `' F " ( CC \ { 0 } ) ) /\ ( F ` k ) = ( F ` k ) ) \/ ( -. k e. ( `' F " ( CC \ { 0 } ) ) /\ ( F ` k ) = 0 ) ) )
37 eqif 
 |-  ( ( F ` k ) = if ( k e. ( `' F " ( CC \ { 0 } ) ) , ( F ` k ) , 0 ) <-> ( ( k e. ( `' F " ( CC \ { 0 } ) ) /\ ( F ` k ) = ( F ` k ) ) \/ ( -. k e. ( `' F " ( CC \ { 0 } ) ) /\ ( F ` k ) = 0 ) ) )
38 36 37 sylibr 
 |-  ( ( ph /\ k e. S ) -> ( F ` k ) = if ( k e. ( `' F " ( CC \ { 0 } ) ) , ( F ` k ) , 0 ) )
39 12 sselda 
 |-  ( ( ph /\ k e. ( `' F " ( CC \ { 0 } ) ) ) -> k e. S )
40 3 ffvelrnda 
 |-  ( ( ph /\ k e. S ) -> ( F ` k ) e. CC )
41 39 40 syldan 
 |-  ( ( ph /\ k e. ( `' F " ( CC \ { 0 } ) ) ) -> ( F ` k ) e. CC )
42 1 2 4 12 38 41 fsumcvg3 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )