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	$⊢ k = i \to A = B$
	esumcvgsum.2	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞)$
	esumcvgsum.3	$⊢ (φ \land k \in ℕ) \to F (k) = A$
	esumcvgsum.4	$⊢ φ \to seq 1 (+ F) ⇝ L$
	esumcvgsum.5	$⊢ φ \to L \in ℝ$
Assertion	esumcvgsum	$⊢ φ \to \underset{k \in ℕ}{\sum^{*}} A = \sum_{k \in ℕ} A$

Proof

Step	Hyp	Ref	Expression
1		esumcvgsum.1	$⊢ k = i \to A = B$
2		esumcvgsum.2	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞)$
3		esumcvgsum.3	$⊢ (φ \land k \in ℕ) \to F (k) = A$
4		esumcvgsum.4	$⊢ φ \to seq 1 (+ F) ⇝ L$
5		esumcvgsum.5	$⊢ φ \to L \in ℝ$
6		simpll	$⊢ ((φ \land j \in ℕ) \land k \in (1 \dots j)) \to φ$
7		elfznn	$⊢ k \in (1 \dots j) \to k \in ℕ$
8	7	adantl	$⊢ ((φ \land j \in ℕ) \land k \in (1 \dots j)) \to k \in ℕ$
9	6 8 3	syl2anc	$⊢ ((φ \land j \in ℕ) \land k \in (1 \dots j)) \to F (k) = A$
10		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
11	10	eleq2i	$⊢ j \in ℕ \leftrightarrow j \in ℤ_{\geq 1}$
12	11	biimpi	$⊢ j \in ℕ \to j \in ℤ_{\geq 1}$
13	12	adantl	$⊢ (φ \land j \in ℕ) \to j \in ℤ_{\geq 1}$
14		mnfxr	$⊢ −∞ \in ℝ^{*}$
15		pnfxr	$⊢ +∞ \in ℝ^{*}$
16		0re	$⊢ 0 \in ℝ$
17		mnflt	$⊢ 0 \in ℝ \to −∞ < 0$
18	16 17	ax-mp	$⊢ −∞ < 0$
19		pnfge	$⊢ +∞ \in ℝ^{*} \to +∞ \leq +∞$
20	15 19	ax-mp	$⊢ +∞ \leq +∞$
21		icossioo	$⊢ ((−∞ \in ℝ^{} \land +∞ \in ℝ^{}) \land (−∞ < 0 \land +∞ \leq +∞)) \to [0, +∞) \subseteq (−∞, +∞)$
22	14 15 18 20 21	mp4an	$⊢ [0, +∞) \subseteq (−∞, +∞)$
23		ioomax	$⊢ (−∞, +∞) = ℝ$
24	22 23	sseqtri	$⊢ [0, +∞) \subseteq ℝ$
25	6 8 2	syl2anc	$⊢ ((φ \land j \in ℕ) \land k \in (1 \dots j)) \to A \in [0, +∞)$
26	24 25	sseldi	$⊢ ((φ \land j \in ℕ) \land k \in (1 \dots j)) \to A \in ℝ$
27	26	recnd	$⊢ ((φ \land j \in ℕ) \land k \in (1 \dots j)) \to A \in ℂ$
28	9 13 27	fsumser	$⊢ (φ \land j \in ℕ) \to \sum_{k = 1}^{j} A = seq 1 (+ F) (j)$
29	28	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ \sum_{k = 1}^{j} A) = (j \in ℕ ⟼ seq 1 (+ F) (j))$
30		1z	$⊢ 1 \in ℤ$
31		seqfn	$⊢ 1 \in ℤ \to seq 1 (+ F) Fn ℤ_{\geq 1}$
32	30 31	ax-mp	$⊢ seq 1 (+ F) Fn ℤ_{\geq 1}$
33		fneq2	$⊢ ℕ = ℤ_{\geq 1} \to (seq 1 (+ F) Fn ℕ \leftrightarrow seq 1 (+ F) Fn ℤ_{\geq 1})$
34	10 33	ax-mp	$⊢ seq 1 (+ F) Fn ℕ \leftrightarrow seq 1 (+ F) Fn ℤ_{\geq 1}$
35	32 34	mpbir	$⊢ seq 1 (+ F) Fn ℕ$
36		dffn5	$⊢ seq 1 (+ F) Fn ℕ \leftrightarrow seq 1 (+ F) = (j \in ℕ ⟼ seq 1 (+ F) (j))$
37	35 36	mpbi	$⊢ seq 1 (+ F) = (j \in ℕ ⟼ seq 1 (+ F) (j))$
38		seqex	$⊢ seq 1 (+ F) \in V$
39	38	a1i	$⊢ φ \to seq 1 (+ F) \in V$
40		breldmg	$⊢ (seq 1 (+ F) \in V \land L \in ℝ \land seq 1 (+ F) ⇝ L) \to seq 1 (+ F) \in dom ⇝$
41	39 5 4 40	syl3anc	$⊢ φ \to seq 1 (+ F) \in dom ⇝$
42	37 41	eqeltrrid	$⊢ φ \to (j \in ℕ ⟼ seq 1 (+ F) (j)) \in dom ⇝$
43	29 42	eqeltrd	$⊢ φ \to (j \in ℕ ⟼ \sum_{k = 1}^{j} A) \in dom ⇝$
44	2 1 43	esumpcvgval	$⊢ φ \to \underset{k \in ℕ}{\sum^{*}} A = \sum_{k \in ℕ} A$

Metamath Proof Explorer

Theorem esumcvgsum

Proof