Metamath Proof Explorer

Theorem isumless

Description: A finite sum of nonnegative numbers is less than or equal to its limit. (Contributed by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isumless.1 
|- Z = ( ZZ>= ` M )
isumless.2 
|- ( ph -> M e. ZZ )
isumless.3 
|- ( ph -> A e. Fin )
isumless.4 
|- ( ph -> A C_ Z )
isumless.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
isumless.6 
|- ( ( ph /\ k e. Z ) -> B e. RR )
isumless.7 
|- ( ( ph /\ k e. Z ) -> 0 <_ B )
isumless.8 
|- ( ph -> seq M ( + , F ) e. dom ~~> )
Assertion isumless 
|- ( ph -> sum_ k e. A B <_ sum_ k e. Z B )

Proof

Step Hyp Ref Expression
1 isumless.1 
 |-  Z = ( ZZ>= ` M )
2 isumless.2 
 |-  ( ph -> M e. ZZ )
3 isumless.3 
 |-  ( ph -> A e. Fin )
4 isumless.4 
 |-  ( ph -> A C_ Z )
5 isumless.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
6 isumless.6 
 |-  ( ( ph /\ k e. Z ) -> B e. RR )
7 isumless.7 
 |-  ( ( ph /\ k e. Z ) -> 0 <_ B )
8 isumless.8 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
9 4 sselda 
 |-  ( ( ph /\ k e. A ) -> k e. Z )
10 6 recnd 
 |-  ( ( ph /\ k e. Z ) -> B e. CC )
11 9 10 syldan 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
12 11 ralrimiva 
 |-  ( ph -> A. k e. A B e. CC )
13 1 eqimssi 
 |-  Z C_ ( ZZ>= ` M )
14 13 orci 
 |-  ( Z C_ ( ZZ>= ` M ) \/ Z e. Fin )
15 14 a1i 
 |-  ( ph -> ( Z C_ ( ZZ>= ` M ) \/ Z e. Fin ) )
16 sumss2 
 |-  ( ( ( A C_ Z /\ A. k e. A B e. CC ) /\ ( Z C_ ( ZZ>= ` M ) \/ Z e. Fin ) ) -> sum_ k e. A B = sum_ k e. Z if ( k e. A , B , 0 ) )
17 4 12 15 16 syl21anc 
 |-  ( ph -> sum_ k e. A B = sum_ k e. Z if ( k e. A , B , 0 ) )
18 eleq1w 
 |-  ( j = k -> ( j e. A <-> k e. A ) )
19 fveq2 
 |-  ( j = k -> ( F ` j ) = ( F ` k ) )
20 18 19 ifbieq1d 
 |-  ( j = k -> if ( j e. A , ( F ` j ) , 0 ) = if ( k e. A , ( F ` k ) , 0 ) )
21 eqid 
 |-  ( j e. Z |-> if ( j e. A , ( F ` j ) , 0 ) ) = ( j e. Z |-> if ( j e. A , ( F ` j ) , 0 ) )
22 fvex 
 |-  ( F ` k ) e. _V
23 c0ex 
 |-  0 e. _V
24 22 23 ifex 
 |-  if ( k e. A , ( F ` k ) , 0 ) e. _V
25 20 21 24 fvmpt 
 |-  ( k e. Z -> ( ( j e. Z |-> if ( j e. A , ( F ` j ) , 0 ) ) ` k ) = if ( k e. A , ( F ` k ) , 0 ) )
26 25 adantl 
 |-  ( ( ph /\ k e. Z ) -> ( ( j e. Z |-> if ( j e. A , ( F ` j ) , 0 ) ) ` k ) = if ( k e. A , ( F ` k ) , 0 ) )
27 5 ifeq1d 
 |-  ( ( ph /\ k e. Z ) -> if ( k e. A , ( F ` k ) , 0 ) = if ( k e. A , B , 0 ) )
28 26 27 eqtrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( j e. Z |-> if ( j e. A , ( F ` j ) , 0 ) ) ` k ) = if ( k e. A , B , 0 ) )
29 0re 
 |-  0 e. RR
30 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( k e. A , B , 0 ) e. RR )
31 6 29 30 sylancl 
 |-  ( ( ph /\ k e. Z ) -> if ( k e. A , B , 0 ) e. RR )
32 leid 
 |-  ( B e. RR -> B <_ B )
33 breq1 
 |-  ( B = if ( k e. A , B , 0 ) -> ( B <_ B <-> if ( k e. A , B , 0 ) <_ B ) )
34 breq1 
 |-  ( 0 = if ( k e. A , B , 0 ) -> ( 0 <_ B <-> if ( k e. A , B , 0 ) <_ B ) )
35 33 34 ifboth 
 |-  ( ( B <_ B /\ 0 <_ B ) -> if ( k e. A , B , 0 ) <_ B )
36 32 35 sylan 
 |-  ( ( B e. RR /\ 0 <_ B ) -> if ( k e. A , B , 0 ) <_ B )
37 6 7 36 syl2anc 
 |-  ( ( ph /\ k e. Z ) -> if ( k e. A , B , 0 ) <_ B )
38 1 2 3 4 28 11 fsumcvg3 
 |-  ( ph -> seq M ( + , ( j e. Z |-> if ( j e. A , ( F ` j ) , 0 ) ) ) e. dom ~~> )
39 1 2 28 31 5 6 37 38 8 isumle 
 |-  ( ph -> sum_ k e. Z if ( k e. A , B , 0 ) <_ sum_ k e. Z B )
40 17 39 eqbrtrd 
 |-  ( ph -> sum_ k e. A B <_ sum_ k e. Z B )