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	$⊢ Z = ℤ_{\geq M}$
	isumsup.2	$⊢ G = seq M (+ F)$
	isumsup.3	$⊢ φ \to M \in ℤ$
	isumsup.4	$⊢ (φ \land k \in Z) \to F (k) = A$
	isumsup.5	$⊢ (φ \land k \in Z) \to A \in ℝ$
	isumsup.6	$⊢ (φ \land k \in Z) \to 0 \leq A$
	isumsup.7	$⊢ φ \to \exists x \in ℝ \forall j \in Z G (j) \leq x$
Assertion	isumsup	$⊢ φ \to \sum_{k \in Z} A = sup (ran G ℝ <)$

Step	Hyp	Ref	Expression
1		isumsup.1	$⊢ Z = ℤ_{\geq M}$
2		isumsup.2	$⊢ G = seq M (+ F)$
3		isumsup.3	$⊢ φ \to M \in ℤ$
4		isumsup.4	$⊢ (φ \land k \in Z) \to F (k) = A$
5		isumsup.5	$⊢ (φ \land k \in Z) \to A \in ℝ$
6		isumsup.6	$⊢ (φ \land k \in Z) \to 0 \leq A$
7		isumsup.7	$⊢ φ \to \exists x \in ℝ \forall j \in Z G (j) \leq x$
8	5	recnd	$⊢ (φ \land k \in Z) \to A \in ℂ$
9	1 2 3 4 5 6 7	isumsup2	$⊢ φ \to G ⇝ sup (ran G ℝ <)$
10	2 9	eqbrtrrid	$⊢ φ \to seq M (+ F) ⇝ sup (ran G ℝ <)$
11	1 3 4 8 10	isumclim	$⊢ φ \to \sum_{k \in Z} A = sup (ran G ℝ <)$

Metamath Proof Explorer