Metamath Proof Explorer

Theorem esumle

Description: If all of the terms of an extended sums compare, so do the sums. (Contributed by Thierry Arnoux, 8-Jun-2017)

Ref Expression
Hypotheses esumadd.0 
|- ( ph -> A e. V )
esumadd.1 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumadd.2 
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
esumle.3 
|- ( ( ph /\ k e. A ) -> B <_ C )
Assertion esumle 
|- ( ph -> sum* k e. A B <_ sum* k e. A C )

Proof

Step Hyp Ref Expression
1 esumadd.0 
 |-  ( ph -> A e. V )
2 esumadd.1 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
3 esumadd.2 
 |-  ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
4 esumle.3 
 |-  ( ( ph /\ k e. A ) -> B <_ C )
5 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
6 2 ralrimiva 
 |-  ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
7 nfcv 
 |-  F/_ k A
8 7 esumcl 
 |-  ( ( A e. V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( 0 [,] +oo ) )
9 1 6 8 syl2anc 
 |-  ( ph -> sum* k e. A B e. ( 0 [,] +oo ) )
10 5 9 sselid 
 |-  ( ph -> sum* k e. A B e. RR* )
11 5 3 sselid 
 |-  ( ( ph /\ k e. A ) -> C e. RR* )
12 5 2 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. RR* )
13 12 xnegcld 
 |-  ( ( ph /\ k e. A ) -> -e B e. RR* )
14 11 13 xaddcld 
 |-  ( ( ph /\ k e. A ) -> ( C +e -e B ) e. RR* )
15 xsubge0 
 |-  ( ( C e. RR* /\ B e. RR* ) -> ( 0 <_ ( C +e -e B ) <-> B <_ C ) )
16 11 12 15 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( 0 <_ ( C +e -e B ) <-> B <_ C ) )
17 4 16 mpbird 
 |-  ( ( ph /\ k e. A ) -> 0 <_ ( C +e -e B ) )
18 pnfge 
 |-  ( ( C +e -e B ) e. RR* -> ( C +e -e B ) <_ +oo )
19 14 18 syl 
 |-  ( ( ph /\ k e. A ) -> ( C +e -e B ) <_ +oo )
20 0xr 
 |-  0 e. RR*
21 pnfxr 
 |-  +oo e. RR*
22 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( ( C +e -e B ) e. ( 0 [,] +oo ) <-> ( ( C +e -e B ) e. RR* /\ 0 <_ ( C +e -e B ) /\ ( C +e -e B ) <_ +oo ) ) )
23 20 21 22 mp2an 
 |-  ( ( C +e -e B ) e. ( 0 [,] +oo ) <-> ( ( C +e -e B ) e. RR* /\ 0 <_ ( C +e -e B ) /\ ( C +e -e B ) <_ +oo ) )
24 14 17 19 23 syl3anbrc 
 |-  ( ( ph /\ k e. A ) -> ( C +e -e B ) e. ( 0 [,] +oo ) )
25 24 ralrimiva 
 |-  ( ph -> A. k e. A ( C +e -e B ) e. ( 0 [,] +oo ) )
26 7 esumcl 
 |-  ( ( A e. V /\ A. k e. A ( C +e -e B ) e. ( 0 [,] +oo ) ) -> sum* k e. A ( C +e -e B ) e. ( 0 [,] +oo ) )
27 1 25 26 syl2anc 
 |-  ( ph -> sum* k e. A ( C +e -e B ) e. ( 0 [,] +oo ) )
28 5 27 sselid 
 |-  ( ph -> sum* k e. A ( C +e -e B ) e. RR* )
29 20 a1i 
 |-  ( ph -> 0 e. RR* )
30 21 a1i 
 |-  ( ph -> +oo e. RR* )
31 elicc4 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ sum* k e. A ( C +e -e B ) e. RR* ) -> ( sum* k e. A ( C +e -e B ) e. ( 0 [,] +oo ) <-> ( 0 <_ sum* k e. A ( C +e -e B ) /\ sum* k e. A ( C +e -e B ) <_ +oo ) ) )
32 29 30 28 31 syl3anc 
 |-  ( ph -> ( sum* k e. A ( C +e -e B ) e. ( 0 [,] +oo ) <-> ( 0 <_ sum* k e. A ( C +e -e B ) /\ sum* k e. A ( C +e -e B ) <_ +oo ) ) )
33 27 32 mpbid 
 |-  ( ph -> ( 0 <_ sum* k e. A ( C +e -e B ) /\ sum* k e. A ( C +e -e B ) <_ +oo ) )
34 33 simpld 
 |-  ( ph -> 0 <_ sum* k e. A ( C +e -e B ) )
35 xraddge02 
 |-  ( ( sum* k e. A B e. RR* /\ sum* k e. A ( C +e -e B ) e. RR* ) -> ( 0 <_ sum* k e. A ( C +e -e B ) -> sum* k e. A B <_ ( sum* k e. A B +e sum* k e. A ( C +e -e B ) ) ) )
36 35 imp 
 |-  ( ( ( sum* k e. A B e. RR* /\ sum* k e. A ( C +e -e B ) e. RR* ) /\ 0 <_ sum* k e. A ( C +e -e B ) ) -> sum* k e. A B <_ ( sum* k e. A B +e sum* k e. A ( C +e -e B ) ) )
37 10 28 34 36 syl21anc 
 |-  ( ph -> sum* k e. A B <_ ( sum* k e. A B +e sum* k e. A ( C +e -e B ) ) )
38 xaddcom 
 |-  ( ( sum* k e. A B e. RR* /\ sum* k e. A ( C +e -e B ) e. RR* ) -> ( sum* k e. A B +e sum* k e. A ( C +e -e B ) ) = ( sum* k e. A ( C +e -e B ) +e sum* k e. A B ) )
39 10 28 38 syl2anc 
 |-  ( ph -> ( sum* k e. A B +e sum* k e. A ( C +e -e B ) ) = ( sum* k e. A ( C +e -e B ) +e sum* k e. A B ) )
40 37 39 breqtrd 
 |-  ( ph -> sum* k e. A B <_ ( sum* k e. A ( C +e -e B ) +e sum* k e. A B ) )
41 1 24 2 esumadd 
 |-  ( ph -> sum* k e. A ( ( C +e -e B ) +e B ) = ( sum* k e. A ( C +e -e B ) +e sum* k e. A B ) )
42 xrge0npcan 
 |-  ( ( C e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) /\ B <_ C ) -> ( ( C +e -e B ) +e B ) = C )
43 3 2 4 42 syl3anc 
 |-  ( ( ph /\ k e. A ) -> ( ( C +e -e B ) +e B ) = C )
44 43 esumeq2dv 
 |-  ( ph -> sum* k e. A ( ( C +e -e B ) +e B ) = sum* k e. A C )
45 41 44 eqtr3d 
 |-  ( ph -> ( sum* k e. A ( C +e -e B ) +e sum* k e. A B ) = sum* k e. A C )
46 40 45 breqtrd 
 |-  ( ph -> sum* k e. A B <_ sum* k e. A C )