Metamath Proof Explorer


Theorem esumid

Description: Identify the extended sum as any limit points of the infinite sum. (Contributed by Thierry Arnoux, 9-May-2017)

Ref Expression
Hypotheses esumid.p 𝑘 𝜑
esumid.0 𝑘 𝐴
esumid.1 ( 𝜑𝐴𝑉 )
esumid.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
esumid.3 ( 𝜑𝐶 ∈ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) ) )
Assertion esumid ( 𝜑 → Σ* 𝑘𝐴 𝐵 = 𝐶 )

Proof

Step Hyp Ref Expression
1 esumid.p 𝑘 𝜑
2 esumid.0 𝑘 𝐴
3 esumid.1 ( 𝜑𝐴𝑉 )
4 esumid.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
5 esumid.3 ( 𝜑𝐶 ∈ ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) ) )
6 df-esum Σ* 𝑘𝐴 𝐵 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) )
7 eqid ( ℝ*𝑠s ( 0 [,] +∞ ) ) = ( ℝ*𝑠s ( 0 [,] +∞ ) )
8 nfcv 𝑘 ( 0 [,] +∞ )
9 eqid ( 𝑘𝐴𝐵 ) = ( 𝑘𝐴𝐵 )
10 1 2 8 4 9 fmptdF ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
11 7 3 10 5 xrge0tsmseq ( 𝜑𝐶 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐵 ) ) )
12 6 11 eqtr4id ( 𝜑 → Σ* 𝑘𝐴 𝐵 = 𝐶 )