Metamath Proof Explorer

Theorem fsumcvg3

Description: A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumcvg3.1 
|- Z = ( ZZ>= ` M )
fsumcvg3.2 
|- ( ph -> M e. ZZ )
fsumcvg3.3 
|- ( ph -> A e. Fin )
fsumcvg3.4 
|- ( ph -> A C_ Z )
fsumcvg3.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
fsumcvg3.6 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fsumcvg3 
|- ( ph -> seq M ( + , F ) e. dom ~~> )

Proof

Step Hyp Ref Expression
1 fsumcvg3.1 
 |-  Z = ( ZZ>= ` M )
2 fsumcvg3.2 
 |-  ( ph -> M e. ZZ )
3 fsumcvg3.3 
 |-  ( ph -> A e. Fin )
4 fsumcvg3.4 
 |-  ( ph -> A C_ Z )
5 fsumcvg3.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
6 fsumcvg3.6 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
7 sseq1 
 |-  ( A = (/) -> ( A C_ ( M ... n ) <-> (/) C_ ( M ... n ) ) )
8 7 rexbidv 
 |-  ( A = (/) -> ( E. n e. ( ZZ>= ` M ) A C_ ( M ... n ) <-> E. n e. ( ZZ>= ` M ) (/) C_ ( M ... n ) ) )
9 4 adantr 
 |-  ( ( ph /\ A =/= (/) ) -> A C_ Z )
10 9 1 sseqtrdi 
 |-  ( ( ph /\ A =/= (/) ) -> A C_ ( ZZ>= ` M ) )
11 ltso 
 |-  < Or RR
12 3 adantr 
 |-  ( ( ph /\ A =/= (/) ) -> A e. Fin )
13 simpr 
 |-  ( ( ph /\ A =/= (/) ) -> A =/= (/) )
14 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
15 zssre 
 |-  ZZ C_ RR
16 14 15 sstri 
 |-  ( ZZ>= ` M ) C_ RR
17 1 16 eqsstri 
 |-  Z C_ RR
18 9 17 sstrdi 
 |-  ( ( ph /\ A =/= (/) ) -> A C_ RR )
19 12 13 18 3jca 
 |-  ( ( ph /\ A =/= (/) ) -> ( A e. Fin /\ A =/= (/) /\ A C_ RR ) )
20 fisupcl 
 |-  ( ( < Or RR /\ ( A e. Fin /\ A =/= (/) /\ A C_ RR ) ) -> sup ( A , RR , < ) e. A )
21 11 19 20 sylancr 
 |-  ( ( ph /\ A =/= (/) ) -> sup ( A , RR , < ) e. A )
22 10 21 sseldd 
 |-  ( ( ph /\ A =/= (/) ) -> sup ( A , RR , < ) e. ( ZZ>= ` M ) )
23 fimaxre2 
 |-  ( ( A C_ RR /\ A e. Fin ) -> E. k e. RR A. n e. A n <_ k )
24 18 12 23 syl2anc 
 |-  ( ( ph /\ A =/= (/) ) -> E. k e. RR A. n e. A n <_ k )
25 18 13 24 3jca 
 |-  ( ( ph /\ A =/= (/) ) -> ( A C_ RR /\ A =/= (/) /\ E. k e. RR A. n e. A n <_ k ) )
26 suprub 
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. k e. RR A. n e. A n <_ k ) /\ k e. A ) -> k <_ sup ( A , RR , < ) )
27 25 26 sylan 
 |-  ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> k <_ sup ( A , RR , < ) )
28 10 sselda 
 |-  ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> k e. ( ZZ>= ` M ) )
29 14 22 sseldi 
 |-  ( ( ph /\ A =/= (/) ) -> sup ( A , RR , < ) e. ZZ )
30 29 adantr 
 |-  ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> sup ( A , RR , < ) e. ZZ )
31 elfz5 
 |-  ( ( k e. ( ZZ>= ` M ) /\ sup ( A , RR , < ) e. ZZ ) -> ( k e. ( M ... sup ( A , RR , < ) ) <-> k <_ sup ( A , RR , < ) ) )
32 28 30 31 syl2anc 
 |-  ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> ( k e. ( M ... sup ( A , RR , < ) ) <-> k <_ sup ( A , RR , < ) ) )
33 27 32 mpbird 
 |-  ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> k e. ( M ... sup ( A , RR , < ) ) )
34 33 ex 
 |-  ( ( ph /\ A =/= (/) ) -> ( k e. A -> k e. ( M ... sup ( A , RR , < ) ) ) )
35 34 ssrdv 
 |-  ( ( ph /\ A =/= (/) ) -> A C_ ( M ... sup ( A , RR , < ) ) )
36 oveq2 
 |-  ( n = sup ( A , RR , < ) -> ( M ... n ) = ( M ... sup ( A , RR , < ) ) )
37 36 sseq2d 
 |-  ( n = sup ( A , RR , < ) -> ( A C_ ( M ... n ) <-> A C_ ( M ... sup ( A , RR , < ) ) ) )
38 37 rspcev 
 |-  ( ( sup ( A , RR , < ) e. ( ZZ>= ` M ) /\ A C_ ( M ... sup ( A , RR , < ) ) ) -> E. n e. ( ZZ>= ` M ) A C_ ( M ... n ) )
39 22 35 38 syl2anc 
 |-  ( ( ph /\ A =/= (/) ) -> E. n e. ( ZZ>= ` M ) A C_ ( M ... n ) )
40 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
41 2 40 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
42 0ss 
 |-  (/) C_ ( M ... M )
43 oveq2 
 |-  ( n = M -> ( M ... n ) = ( M ... M ) )
44 43 sseq2d 
 |-  ( n = M -> ( (/) C_ ( M ... n ) <-> (/) C_ ( M ... M ) ) )
45 44 rspcev 
 |-  ( ( M e. ( ZZ>= ` M ) /\ (/) C_ ( M ... M ) ) -> E. n e. ( ZZ>= ` M ) (/) C_ ( M ... n ) )
46 41 42 45 sylancl 
 |-  ( ph -> E. n e. ( ZZ>= ` M ) (/) C_ ( M ... n ) )
47 8 39 46 pm2.61ne 
 |-  ( ph -> E. n e. ( ZZ>= ` M ) A C_ ( M ... n ) )
48 1 eleq2i 
 |-  ( k e. Z <-> k e. ( ZZ>= ` M ) )
49 48 5 sylan2br 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
50 49 adantlr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
51 simprl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) -> n e. ( ZZ>= ` M ) )
52 6 adantlr 
 |-  ( ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) /\ k e. A ) -> B e. CC )
53 simprr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) -> A C_ ( M ... n ) )
54 50 51 52 53 fsumcvg2 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` n ) )
55 climrel 
 |-  Rel ~~>
56 55 releldmi 
 |-  ( seq M ( + , F ) ~~> ( seq M ( + , F ) ` n ) -> seq M ( + , F ) e. dom ~~> )
57 54 56 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ A C_ ( M ... n ) ) ) -> seq M ( + , F ) e. dom ~~> )
58 47 57 rexlimddv 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )