Metamath Proof Explorer


Theorem sge0ssrempt

Description: If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0ssrempt.xph xφ
sge0ssrempt.a φAV
sge0ssrempt.b φxAB0+∞
sge0ssrempt.re φsum^xAB
sge0ssrempt.c φCA
Assertion sge0ssrempt φsum^xCB

Proof

Step Hyp Ref Expression
1 sge0ssrempt.xph xφ
2 sge0ssrempt.a φAV
3 sge0ssrempt.b φxAB0+∞
4 sge0ssrempt.re φsum^xAB
5 sge0ssrempt.c φCA
6 5 resmptd φxABC=xCB
7 6 fveq2d φsum^xABC=sum^xCB
8 7 eqcomd φsum^xCB=sum^xABC
9 eqid xAB=xAB
10 1 3 9 fmptdf φxAB:A0+∞
11 2 10 4 sge0ssre φsum^xABC
12 8 11 eqeltrd φsum^xCB