Metamath Proof Explorer


Theorem sge0snmptf

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

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

Proof

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