Theorem sge0isummpt2

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

Proof

Step	Hyp	Ref	Expression
1		sge0isummpt2.kph	⊢ Ⅎ 𝑘 𝜑
2		sge0isummpt2.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ( 0 [,) +∞ ) )
3		sge0isummpt2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		sge0isummpt2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		sge0isummpt2.b	⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝐵 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
7		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
8	1 7	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
9		nfcv	⊢ Ⅎ 𝑘 𝑗
10	9	nfcsb1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴
11	10	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ( 0 [,) +∞ )
12	8 11	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ( 0 [,) +∞ ) )
13		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
14	13	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
15		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐴 = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
16	15	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ ( 0 [,) +∞ ) ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ( 0 [,) +∞ ) ) )
17	14 16	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ( 0 [,) +∞ ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ( 0 [,) +∞ ) ) ) )
18	12 17 2	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ( 0 [,) +∞ ) )
19		nfcv	⊢ Ⅎ 𝑖 𝐴
20		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐴
21		csbeq1a	⊢ ( 𝑘 = 𝑖 → 𝐴 = ⦋ 𝑖 / 𝑘 ⦌ 𝐴 )
22	19 20 21	cbvmpt	⊢ ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) = ( 𝑖 ∈ 𝑍 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐴 )
23	22	eqcomi	⊢ ( 𝑖 ∈ 𝑍 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐴 ) = ( 𝑘 ∈ 𝑍 ↦ 𝐴 )
24	9 10 15 23	fvmptf	⊢ ( ( 𝑗 ∈ 𝑍 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑖 ∈ 𝑍 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
25	6 18 24	syl2anc	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝑖 ∈ 𝑍 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐴 ) ‘ 𝑗 ) = ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
26		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
27		ax-resscn	⊢ ℝ ⊆ ℂ
28	26 27	sstri	⊢ ( 0 [,) +∞ ) ⊆ ℂ
29	28 18	sselid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐴 ∈ ℂ )
30	22	a1i	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) = ( 𝑖 ∈ 𝑍 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐴 ) )
31	30	seqeq3d	⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) = seq 𝑀 ( + , ( 𝑖 ∈ 𝑍 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐴 ) ) )
32	31	breq1d	⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) ⇝ 𝐵 ↔ seq 𝑀 ( + , ( 𝑖 ∈ 𝑍 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐴 ) ) ⇝ 𝐵 ) )
33	5 32	mpbid	⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑖 ∈ 𝑍 ↦ ⦋ 𝑖 / 𝑘 ⦌ 𝐴 ) ) ⇝ 𝐵 )
34	4 3 25 29 33	isumclim	⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑍 ⦋ 𝑗 / 𝑘 ⦌ 𝐴 = 𝐵 )
35		nfcv	⊢ Ⅎ 𝑗 𝐴
36	15 35 10	cbvsum	⊢ Σ 𝑘 ∈ 𝑍 𝐴 = Σ 𝑗 ∈ 𝑍 ⦋ 𝑗 / 𝑘 ⦌ 𝐴
37	36	a1i	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = Σ 𝑗 ∈ 𝑍 ⦋ 𝑗 / 𝑘 ⦌ 𝐴 )
38	1 2 3 4 5	sge0isummpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) = 𝐵 )
39	34 37 38	3eqtr4rd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ) = Σ 𝑘 ∈ 𝑍 𝐴 )