isumsup2

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	isumsup2	$⊢ φ \to G ⇝ sup (ran G ℝ <)$

Proof

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	4 5	eqeltrd	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
9	1 3 8	serfre	$⊢ φ \to seq M (+ F) : Z ⟶ ℝ$
10	2	feq1i	$⊢ G : Z ⟶ ℝ \leftrightarrow seq M (+ F) : Z ⟶ ℝ$
11	9 10	sylibr	$⊢ φ \to G : Z ⟶ ℝ$
12		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
13	12 1	eleqtrdi	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
14		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
15		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
16		peano2uz	$⊢ j \in ℤ_{\geq j} \to j + 1 \in ℤ_{\geq j}$
17	13 14 15 16	4syl	$⊢ (φ \land j \in Z) \to j + 1 \in ℤ_{\geq j}$
18		simpl	$⊢ (φ \land j \in Z) \to φ$
19		elfzuz	$⊢ k \in (M \dots j + 1) \to k \in ℤ_{\geq M}$
20	19 1	eleqtrrdi	$⊢ k \in (M \dots j + 1) \to k \in Z$
21	18 20 8	syl2an	$⊢ ((φ \land j \in Z) \land k \in (M \dots j + 1)) \to F (k) \in ℝ$
22	1	peano2uzs	$⊢ j \in Z \to j + 1 \in Z$
23	22	adantl	$⊢ (φ \land j \in Z) \to j + 1 \in Z$
24		elfzuz	$⊢ k \in (j + 1 \dots j + 1) \to k \in ℤ_{\geq (j + 1)}$
25	1	uztrn2	$⊢ (j + 1 \in Z \land k \in ℤ_{\geq (j + 1)}) \to k \in Z$
26	23 24 25	syl2an	$⊢ ((φ \land j \in Z) \land k \in (j + 1 \dots j + 1)) \to k \in Z$
27	6 4	breqtrrd	$⊢ (φ \land k \in Z) \to 0 \leq F (k)$
28	27	adantlr	$⊢ ((φ \land j \in Z) \land k \in Z) \to 0 \leq F (k)$
29	26 28	syldan	$⊢ ((φ \land j \in Z) \land k \in (j + 1 \dots j + 1)) \to 0 \leq F (k)$
30	13 17 21 29	sermono	$⊢ (φ \land j \in Z) \to seq M (+ F) (j) \leq seq M (+ F) (j + 1)$
31	2	fveq1i	$⊢ G (j) = seq M (+ F) (j)$
32	2	fveq1i	$⊢ G (j + 1) = seq M (+ F) (j + 1)$
33	30 31 32	3brtr4g	$⊢ (φ \land j \in Z) \to G (j) \leq G (j + 1)$
34	1 3 11 33 7	climsup	$⊢ φ \to G ⇝ sup (ran G ℝ <)$

Metamath Proof Explorer

Theorem isumsup2

Proof