Metamath Proof Explorer


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 ... 𝑛 ) 𝐴 ) ( ⇝𝑡𝐽 ) Σ* 𝑘 ∈ ℕ 𝐴 )