Metamath Proof Explorer

Theorem esumcvgsum

Description: The value of the extended sum when the corresponding sum is convergent. (Contributed by Thierry Arnoux, 29-Oct-2019)

Ref Expression
Hypotheses esumcvgsum.1 ⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐵 )
esumcvgsum.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) )
esumcvgsum.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
esumcvgsum.4 ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝐿 )
esumcvgsum.5 ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
Assertion esumcvgsum ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 = Σ 𝑘 ∈ ℕ 𝐴 )

Proof

Step Hyp Ref Expression
1 esumcvgsum.1 ⊢ ( 𝑘 = 𝑖 → 𝐴 = 𝐵 )
2 esumcvgsum.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,) +∞ ) )
3 esumcvgsum.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4 esumcvgsum.4 ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝐿 )
5 esumcvgsum.5 ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
6 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑗 ) ) → 𝜑 )
7 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑗 ) → 𝑘 ∈ ℕ )
8 7 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑗 ) ) → 𝑘 ∈ ℕ )
9 6 8 3 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
10 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
11 10 eleq2i ⊢ ( 𝑗 ∈ ℕ ↔ 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
12 11 bilani ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
13 mnfxr ⊢ -∞ ∈ ℝ*
14 pnfxr ⊢ +∞ ∈ ℝ*
15 0re ⊢ 0 ∈ ℝ
16 mnflt ⊢ ( 0 ∈ ℝ → -∞ < 0 )
17 15 16 ax-mp ⊢ -∞ < 0
18 pnfge ⊢ ( +∞ ∈ ℝ* → +∞ ≤ +∞ )
19 14 18 ax-mp ⊢ +∞ ≤ +∞
20 icossioo ⊢ ( ( ( -∞ ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( -∞ < 0 ∧ +∞ ≤ +∞ ) ) → ( 0 [,) +∞ ) ⊆ ( -∞ (,) +∞ ) )
21 13 14 17 19 20 mp4an ⊢ ( 0 [,) +∞ ) ⊆ ( -∞ (,) +∞ )
22 ioomax ⊢ ( -∞ (,) +∞ ) = ℝ
23 21 22 sseqtri ⊢ ( 0 [,) +∞ ) ⊆ ℝ
24 6 8 2 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑗 ) ) → 𝐴 ∈ ( 0 [,) +∞ ) )
25 23 24 sselid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑗 ) ) → 𝐴 ∈ ℝ )
26 25 recnd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑗 ) ) → 𝐴 ∈ ℂ )
27 9 12 26 fsumser ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → Σ 𝑘 ∈ ( 1 ... 𝑗 ) 𝐴 = ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) )
28 27 mpteq2dva ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑗 ) 𝐴 ) = ( 𝑗 ∈ ℕ ↦ ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) )
29 1z ⊢ 1 ∈ ℤ
30 seqfn ⊢ ( 1 ∈ ℤ → seq 1 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) )
31 29 30 ax-mp ⊢ seq 1 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 1 )
32 fneq2 ⊢ ( ℕ = ( ℤ≥ ‘ 1 ) → ( seq 1 ( + , 𝐹 ) Fn ℕ ↔ seq 1 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) ) )
33 10 32 ax-mp ⊢ ( seq 1 ( + , 𝐹 ) Fn ℕ ↔ seq 1 ( + , 𝐹 ) Fn ( ℤ≥ ‘ 1 ) )
34 31 33 mpbir ⊢ seq 1 ( + , 𝐹 ) Fn ℕ
35 dffn5 ⊢ ( seq 1 ( + , 𝐹 ) Fn ℕ ↔ seq 1 ( + , 𝐹 ) = ( 𝑗 ∈ ℕ ↦ ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) )
36 34 35 mpbi ⊢ seq 1 ( + , 𝐹 ) = ( 𝑗 ∈ ℕ ↦ ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) )
37 seqex ⊢ seq 1 ( + , 𝐹 ) ∈ V
38 37 a1i ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ V )
39 breldmg ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ V ∧ 𝐿 ∈ ℝ ∧ seq 1 ( + , 𝐹 ) ⇝ 𝐿 ) → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
40 38 5 4 39 syl3anc ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
41 36 40 eqeltrrid ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( seq 1 ( + , 𝐹 ) ‘ 𝑗 ) ) ∈ dom ⇝ )
42 28 41 eqeltrd ⊢ ( 𝜑 → ( 𝑗 ∈ ℕ ↦ Σ 𝑘 ∈ ( 1 ... 𝑗 ) 𝐴 ) ∈ dom ⇝ )
43 2 1 42 esumpcvgval ⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 = Σ 𝑘 ∈ ℕ 𝐴 )