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 sselid
 |-  ( ( 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 ~~> )