Metamath Proof Explorer

Theorem esumlef

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 esumaddf.0 
|- F/ k ph
esumaddf.a 
|- F/_ k A
esumaddf.1 
|- ( ph -> A e. V )
esumaddf.2 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumaddf.3 
|- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )
esumlef.3 
|- ( ( ph /\ k e. A ) -> B <_ C )
Assertion esumlef 
|- ( ph -> sum* k e. A B <_ sum* k e. A C )

Proof

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