esumsup

Description: Express an extended sum as a supremum of extended sums. (Contributed by Thierry Arnoux, 24-May-2020)

	Ref	Expression
Hypotheses	esumsup.1	$⊢ φ \to B \in [0, +∞]$
	esumsup.2	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞]$
Assertion	esumsup	$⊢ φ \to \underset{k \in ℕ}{\sum^{}} A = sup (ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		esumsup.1	$⊢ φ \to B \in [0, +∞]$
2		esumsup.2	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞]$
3	2	fmpttd	$⊢ φ \to (k \in ℕ ⟼ A) : ℕ ⟶ [0, +∞]$
4		nfmpt1	$⊢ \underline{Ⅎ} k (k \in ℕ ⟼ A)$
5	4	esumfsup	$⊢ (k \in ℕ ⟼ A) : ℕ ⟶ [0, +∞] \to \underset{k \in ℕ}{\sum^{}} (k \in ℕ ⟼ A) (k) = sup (ran seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) ℝ^{} <)$
6	3 5	syl	$⊢ φ \to \underset{k \in ℕ}{\sum^{}} (k \in ℕ ⟼ A) (k) = sup (ran seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) ℝ^{} <)$
7		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
8		eqid	$⊢ (k \in ℕ ⟼ A) = (k \in ℕ ⟼ A)$
9	8	fvmpt2	$⊢ (k \in ℕ \land A \in [0, +∞]) \to (k \in ℕ ⟼ A) (k) = A$
10	7 2 9	syl2anc	$⊢ (φ \land k \in ℕ) \to (k \in ℕ ⟼ A) (k) = A$
11	10	esumeq2dv	$⊢ φ \to \underset{k \in ℕ}{\sum^{}} (k \in ℕ ⟼ A) (k) = \underset{k \in ℕ}{\sum^{}} A$
12		1z	$⊢ 1 \in ℤ$
13		seqfn	$⊢ 1 \in ℤ \to seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) Fn ℤ_{\geq 1}$
14	12 13	ax-mp	$⊢ seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) Fn ℤ_{\geq 1}$
15		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
16	15	fneq2i	$⊢ seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) Fn ℕ \leftrightarrow seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) Fn ℤ_{\geq 1}$
17	14 16	mpbir	$⊢ seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) Fn ℕ$
18		nfcv	$⊢ \underline{Ⅎ} n seq 1 (+_{𝑒}, (k \in ℕ ⟼ A))$
19	18	dffn5f	$⊢ seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) Fn ℕ \leftrightarrow seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) = (n \in ℕ ⟼ seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) (n))$
20	17 19	mpbi	$⊢ seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) = (n \in ℕ ⟼ seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) (n))$
21	20	a1i	$⊢ φ \to seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) = (n \in ℕ ⟼ seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) (n))$
22		fz1ssnn	$⊢ (1 \dots n) \subseteq ℕ$
23	22	a1i	$⊢ (φ \land n \in ℕ) \to (1 \dots n) \subseteq ℕ$
24	23	sselda	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to k \in ℕ$
25		simpll	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to φ$
26	25 24 2	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to A \in [0, +∞]$
27	24 26 9	syl2anc	$⊢ ((φ \land n \in ℕ) \land k \in (1 \dots n)) \to (k \in ℕ ⟼ A) (k) = A$
28	27	esumeq2dv	$⊢ (φ \land n \in ℕ) \to {\sum^{}}_{k = 1}^{n} (k \in ℕ ⟼ A) (k) = {\sum^{}}_{k = 1}^{n} A$
29	4	esumfzf	$⊢ ((k \in ℕ ⟼ A) : ℕ ⟶ [0, +∞] \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} (k \in ℕ ⟼ A) (k) = seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) (n)$
30	3 29	sylan	$⊢ (φ \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} (k \in ℕ ⟼ A) (k) = seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) (n)$
31	28 30	eqtr3d	$⊢ (φ \land n \in ℕ) \to {\sum^{*}}_{k = 1}^{n} A = seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) (n)$
32	31	mpteq2dva	$⊢ φ \to (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A) = (n \in ℕ ⟼ seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) (n))$
33	21 32	eqtr4d	$⊢ φ \to seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) = (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A)$
34	33	rneqd	$⊢ φ \to ran seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) = ran (n \in ℕ ⟼ {\sum^{*}}_{k = 1}^{n} A)$
35	34	supeq1d	$⊢ φ \to sup (ran seq 1 (+_{𝑒}, (k \in ℕ ⟼ A)) ℝ^{} <) = sup (ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ℝ^{*} <)$
36	6 11 35	3eqtr3d	$⊢ φ \to \underset{k \in ℕ}{\sum^{}} A = sup (ran (n \in ℕ ⟼ {\sum^{}}_{k = 1}^{n} A) ℝ^{*} <)$

Metamath Proof Explorer

Theorem esumsup

Proof