Theorem esumsup

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

	Ref	Expression
Hypotheses	esumsup.1	⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
	esumsup.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
Assertion	esumsup	⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 = sup ( ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		esumsup.1	⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
2		esumsup.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
3	2	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ ↦ 𝐴 ) : ℕ ⟶ ( 0 [,] +∞ ) )
4		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ ℕ ↦ 𝐴 )
5	4	esumfsup	⊢ ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) : ℕ ⟶ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ℕ ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ‘ 𝑘 ) = sup ( ran seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) , ℝ* , < ) )
6	3 5	syl	⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ‘ 𝑘 ) = sup ( ran seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) , ℝ* , < ) )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
8		eqid	⊢ ( 𝑘 ∈ ℕ ↦ 𝐴 ) = ( 𝑘 ∈ ℕ ↦ 𝐴 )
9	8	fvmpt2	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝐴 ∈ ( 0 [,] +∞ ) ) → ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ‘ 𝑘 ) = 𝐴 )
10	7 2 9	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ‘ 𝑘 ) = 𝐴 )
11	10	esumeq2dv	⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ‘ 𝑘 ) = Σ* 𝑘 ∈ ℕ 𝐴 )
12		1z	⊢ 1 ∈ ℤ
13		seqfn	⊢ ( 1 ∈ ℤ → seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) Fn ( ℤ≥ ‘ 1 ) )
14	12 13	ax-mp	⊢ seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) Fn ( ℤ≥ ‘ 1 )
15		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
16	15	fneq2i	⊢ ( seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) Fn ℕ ↔ seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) Fn ( ℤ≥ ‘ 1 ) )
17	14 16	mpbir	⊢ seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) Fn ℕ
18		nfcv	⊢ Ⅎ 𝑛 seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) )
19	18	dffn5f	⊢ ( seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) Fn ℕ ↔ seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) ‘ 𝑛 ) ) )
20	17 19	mpbi	⊢ seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) ‘ 𝑛 ) )
21	20	a1i	⊢ ( 𝜑 → seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) ‘ 𝑛 ) ) )
22		fz1ssnn	⊢ ( 1 ... 𝑛 ) ⊆ ℕ
23	22	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 1 ... 𝑛 ) ⊆ ℕ )
24	23	sselda	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝑘 ∈ ℕ )
25		simpll	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝜑 )
26	25 24 2	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
27	24 26 9	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ ( 1 ... 𝑛 ) ) → ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ‘ 𝑘 ) = 𝐴 )
28	27	esumeq2dv	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ‘ 𝑘 ) = Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 )
29	4	esumfzf	⊢ ( ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) : ℕ ⟶ ( 0 [,] +∞ ) ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ‘ 𝑘 ) = ( seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) ‘ 𝑛 ) )
30	3 29	sylan	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) ( ( 𝑘 ∈ ℕ ↦ 𝐴 ) ‘ 𝑘 ) = ( seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) ‘ 𝑛 ) )
31	28 30	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 = ( seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) ‘ 𝑛 ) )
32	31	mpteq2dva	⊢ ( 𝜑 → ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) = ( 𝑛 ∈ ℕ ↦ ( seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) ‘ 𝑛 ) ) )
33	21 32	eqtr4d	⊢ ( 𝜑 → seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) = ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
34	33	rneqd	⊢ ( 𝜑 → ran seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) = ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) )
35	34	supeq1d	⊢ ( 𝜑 → sup ( ran seq 1 ( +𝑒 , ( 𝑘 ∈ ℕ ↦ 𝐴 ) ) , ℝ* , < ) = sup ( ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) , ℝ* , < ) )
36	6 11 35	3eqtr3d	⊢ ( 𝜑 → Σ* 𝑘 ∈ ℕ 𝐴 = sup ( ran ( 𝑛 ∈ ℕ ↦ Σ* 𝑘 ∈ ( 1 ... 𝑛 ) 𝐴 ) , ℝ* , < ) )