Theorem isumsup

Description: An infinite sum of nonnegative terms is equal to the supremum of the partial sums. (Contributed by Mario Carneiro, 12-Jun-2014)

	Ref	Expression
Hypotheses	isumsup.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	isumsup.2	⊢ 𝐺 = seq 𝑀 ( + , 𝐹 )
	isumsup.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isumsup.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	isumsup.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
	isumsup.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐴 )
	isumsup.7	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 )
Assertion	isumsup	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = sup ( ran 𝐺 , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		isumsup.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isumsup.2	⊢ 𝐺 = seq 𝑀 ( + , 𝐹 )
3		isumsup.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		isumsup.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
5		isumsup.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
6		isumsup.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐴 )
7		isumsup.7	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 )
8	5	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
9	1 2 3 4 5 6 7	isumsup2	⊢ ( 𝜑 → 𝐺 ⇝ sup ( ran 𝐺 , ℝ , < ) )
10	2 9	eqbrtrrid	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ sup ( ran 𝐺 , ℝ , < ) )
11	1 3 4 8 10	isumclim	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = sup ( ran 𝐺 , ℝ , < ) )