Metamath Proof Explorer

Theorem fsumlessf

Description: A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses fsumlessf.k 
|- F/ k ph
fsumge0.a 
|- ( ph -> A e. Fin )
fsumge0.b 
|- ( ( ph /\ k e. A ) -> B e. RR )
fsumge0.l 
|- ( ( ph /\ k e. A ) -> 0 <_ B )
fsumless.c 
|- ( ph -> C C_ A )
Assertion fsumlessf 
|- ( ph -> sum_ k e. C B <_ sum_ k e. A B )

Proof

Step Hyp Ref Expression
1 fsumlessf.k 
 |-  F/ k ph
2 fsumge0.a 
 |-  ( ph -> A e. Fin )
3 fsumge0.b 
 |-  ( ( ph /\ k e. A ) -> B e. RR )
4 fsumge0.l 
 |-  ( ( ph /\ k e. A ) -> 0 <_ B )
5 fsumless.c 
 |-  ( ph -> C C_ A )
6 nfv 
 |-  F/ k j e. A
7 1 6 nfan 
 |-  F/ k ( ph /\ j e. A )
8 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
9 8 nfel1 
 |-  F/ k [_ j / k ]_ B e. RR
10 7 9 nfim 
 |-  F/ k ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. RR )
11 eleq1w 
 |-  ( k = j -> ( k e. A <-> j e. A ) )
12 11 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. A ) <-> ( ph /\ j e. A ) ) )
13 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
14 13 eleq1d 
 |-  ( k = j -> ( B e. RR <-> [_ j / k ]_ B e. RR ) )
15 12 14 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. A ) -> B e. RR ) <-> ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. RR ) ) )
16 10 15 3 chvarfv 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. RR )
17 nfcv 
 |-  F/_ k 0
18 nfcv 
 |-  F/_ k <_
19 17 18 8 nfbr 
 |-  F/ k 0 <_ [_ j / k ]_ B
20 7 19 nfim 
 |-  F/ k ( ( ph /\ j e. A ) -> 0 <_ [_ j / k ]_ B )
21 13 breq2d 
 |-  ( k = j -> ( 0 <_ B <-> 0 <_ [_ j / k ]_ B ) )
22 12 21 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. A ) -> 0 <_ B ) <-> ( ( ph /\ j e. A ) -> 0 <_ [_ j / k ]_ B ) ) )
23 20 22 4 chvarfv 
 |-  ( ( ph /\ j e. A ) -> 0 <_ [_ j / k ]_ B )
24 2 16 23 5 fsumless 
 |-  ( ph -> sum_ j e. C [_ j / k ]_ B <_ sum_ j e. A [_ j / k ]_ B )
25 nfcv 
 |-  F/_ j B
26 13 25 8 cbvsum 
 |-  sum_ k e. C B = sum_ j e. C [_ j / k ]_ B
27 13 25 8 cbvsum 
 |-  sum_ k e. A B = sum_ j e. A [_ j / k ]_ B
28 26 27 breq12i 
 |-  ( sum_ k e. C B <_ sum_ k e. A B <-> sum_ j e. C [_ j / k ]_ B <_ sum_ j e. A [_ j / k ]_ B )
29 24 28 sylibr 
 |-  ( ph -> sum_ k e. C B <_ sum_ k e. A B )