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	⊢ Ⅎ 𝑘 𝜑
	sge0isummpt.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ( 0 [,) +∞ ) )
	sge0isummpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	sge0isummpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	sge0isummpt.b	⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝐵 )
Assertion	sge0isummpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sge0isummpt.kph	⊢ Ⅎ 𝑘 𝜑
2		sge0isummpt.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ( 0 [,) +∞ ) )
3		sge0isummpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		sge0isummpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		sge0isummpt.b	⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝐵 )
6		eqid	⊢ ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) = ( 𝑘 ∈ 𝑍 ↦ 𝐴 )
7	1 2 6	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) : 𝑍 ⟶ ( 0 [,) +∞ ) )
8		eqid	⊢ seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) = seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) )
9	3 4 7 8 5	sge0isum	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) = 𝐵 )