Metamath Proof Explorer


Theorem sge0lessmpt

Description: A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0lessmpt.a φAV
sge0lessmpt.b φxAB0+∞
sge0lessmpt.c φCA
Assertion sge0lessmpt φsum^xCBsum^xAB

Proof

Step Hyp Ref Expression
1 sge0lessmpt.a φAV
2 sge0lessmpt.b φxAB0+∞
3 sge0lessmpt.c φCA
4 id φφ
5 3 resmptd φxABC=xCB
6 5 eqcomd φxCB=xABC
7 4 6 syl φxCB=xABC
8 7 fveq2d φsum^xCB=sum^xABC
9 eqid xAB=xAB
10 2 9 fmptd φxAB:A0+∞
11 1 10 sge0less φsum^xABCsum^xAB
12 8 11 eqbrtrd φsum^xCBsum^xAB