Metamath Proof Explorer

Theorem sge0isummpt

Description: If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0isummpt.kph ⊢ Ⅎ k φ
sge0isummpt.a ⊢ φ ∧ k ∈ Z → A ∈ 0 +∞
sge0isummpt.m ⊢ φ → M ∈ ℤ
sge0isummpt.z ⊢ Z = ℤ ≥ M
sge0isummpt.b ⊢ φ → seq M + k ∈ Z ⟼ A ⇝ B
Assertion sge0isummpt ⊢ φ → sum^ ⁡ k ∈ Z ⟼ A = B

Proof

Step Hyp Ref Expression
1 sge0isummpt.kph ⊢ Ⅎ k φ
2 sge0isummpt.a ⊢ φ ∧ k ∈ Z → A ∈ 0 +∞
3 sge0isummpt.m ⊢ φ → M ∈ ℤ
4 sge0isummpt.z ⊢ Z = ℤ ≥ M
5 sge0isummpt.b ⊢ φ → seq M + k ∈ Z ⟼ A ⇝ B
6 eqid ⊢ k ∈ Z ⟼ A = k ∈ Z ⟼ A
7 1 2 6 fmptdf ⊢ φ → k ∈ Z ⟼ A : Z ⟶ 0 +∞
8 eqid ⊢ seq M + k ∈ Z ⟼ A = seq M + k ∈ Z ⟼ A
9 3 4 7 8 5 sge0isum ⊢ φ → sum^ ⁡ k ∈ Z ⟼ A = B