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

Metamath Proof Explorer

Theorem esumcvgsum

Proof