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 = +∞