Metamath Proof Explorer


Theorem sge0pnfmpt

Description: If a term in the sum of nonnegative extended reals is +oo , then the value of the sum is +oo . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses sge0pnfmpt.k k φ
sge0pnfmpt.a φ A V
sge0pnfmpt.b φ k A B 0 +∞
sge0pnfmpt.p φ k A B = +∞
Assertion sge0pnfmpt φ sum^ k A B = +∞

Proof

Step Hyp Ref Expression
1 sge0pnfmpt.k k φ
2 sge0pnfmpt.a φ A V
3 sge0pnfmpt.b φ k A B 0 +∞
4 sge0pnfmpt.p φ k A B = +∞
5 eqid k A B = k A B
6 1 3 5 fmptdf φ k A B : A 0 +∞
7 eqcom B = +∞ +∞ = B
8 7 rexbii k A B = +∞ k A +∞ = B
9 4 8 sylib φ k A +∞ = B
10 pnfex +∞ V
11 10 a1i φ +∞ V
12 5 9 11 elrnmptd φ +∞ ran k A B
13 2 6 12 sge0pnfval φ sum^ k A B = +∞