Metamath Proof Explorer


Theorem sge0snmpt

Description: A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0snmpt.a φ A V
sge0snmpt.c φ C 0 +∞
sge0snmpt.b k = A B = C
Assertion sge0snmpt φ sum^ k A B = C

Proof

Step Hyp Ref Expression
1 sge0snmpt.a φ A V
2 sge0snmpt.c φ C 0 +∞
3 sge0snmpt.b k = A B = C
4 elsni k A k = A
5 4 3 syl k A B = C
6 5 adantl φ k A B = C
7 2 adantr φ k A C 0 +∞
8 6 7 eqeltrd φ k A B 0 +∞
9 eqid k A B = k A B
10 8 9 fmptd φ k A B : A 0 +∞
11 1 10 sge0sn φ sum^ k A B = k A B A
12 eqidd φ k A B = k A B
13 3 adantl φ k = A B = C
14 snidg A V A A
15 1 14 syl φ A A
16 12 13 15 2 fvmptd φ k A B A = C
17 11 16 eqtrd φ sum^ k A B = C