Theorem esumcvg2

Description: Simpler version of esumcvg . (Contributed by Thierry Arnoux, 5-Sep-2017)

	Ref	Expression
Hypotheses	esumcvg2.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
	esumcvg2.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
	esumcvg2.l	⊢ ( 𝑘 = 𝑙 → 𝐴 = 𝐵 )
	esumcvg2.m	⊢ ( 𝑘 = 𝑚 → 𝐴 = 𝐶 )
Assertion	esumcvg2	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ( ⇝𝑡 ‘ 𝐽 ) Σ* 𝑘 ∈ ℕ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		esumcvg2.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
2		esumcvg2.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
3		esumcvg2.l	⊢ ( 𝑘 = 𝑙 → 𝐴 = 𝐵 )
4		esumcvg2.m	⊢ ( 𝑘 = 𝑚 → 𝐴 = 𝐶 )
5	4	cbvesumv	⊢ Σ* 𝑘 ∈ ( 1 ... 𝑖 ) 𝐴 = Σ* 𝑚 ∈ ( 1 ... 𝑖 ) 𝐶
6		oveq2	⊢ ( 𝑖 = 𝑛 → ( 1 ... 𝑖 ) = ( 1 ... 𝑛 ) )
7		esumeq1	⊢ ( ( 1 ... 𝑖 ) = ( 1 ... 𝑛 ) → Σ* 𝑘 ∈ ( 1 ... 𝑖 ) 𝐴 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
8	6 7	syl	⊢ ( 𝑖 = 𝑛 → Σ* 𝑘 ∈ ( 1 ... 𝑖 ) 𝐴 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
9	5 8	eqtr3id	⊢ ( 𝑖 = 𝑛 → Σ* 𝑚 ∈ ( 1 ... 𝑖 ) 𝐶 = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
10	9	cbvmptv	⊢ ( 𝑖 ∈ ℕ ↦ Σ* 𝑚 ∈ ( 1 ... 𝑖 ) 𝐶 ) = ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
11	1 10 2 3	esumcvg	⊢ ( 𝜑 → ( 𝑖 ∈ ℕ ↦ Σ* 𝑚 ∈ ( 1 ... 𝑖 ) 𝐶 ) ( ⇝𝑡 ‘ 𝐽 ) Σ* 𝑘 ∈ ℕ 𝐴 )
12	10 11	eqbrtrrid	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) ( ⇝𝑡 ‘ 𝐽 ) Σ* 𝑘 ∈ ℕ 𝐴 )