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