Metamath Proof Explorer

Theorem 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 = ℤ ≥ M
isumsup.2 ⊢ G = seq M + F
isumsup.3 ⊢ φ → M ∈ ℤ
isumsup.4 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
isumsup.5 ⊢ φ ∧ k ∈ Z → A ∈ ℝ
isumsup.6 ⊢ φ ∧ k ∈ Z → 0 ≤ A
isumsup.7 ⊢ φ → ∃ x ∈ ℝ ∀ j ∈ Z G ⁡ j ≤ x
Assertion isumsup2 ⊢ φ → G ⇝ sup ran ⁡ G ℝ <

Proof

Step Hyp Ref Expression
1 isumsup.1 ⊢ Z = ℤ ≥ M
2 isumsup.2 ⊢ G = seq M + F
3 isumsup.3 ⊢ φ → M ∈ ℤ
4 isumsup.4 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
5 isumsup.5 ⊢ φ ∧ k ∈ Z → A ∈ ℝ
6 isumsup.6 ⊢ φ ∧ k ∈ Z → 0 ≤ A
7 isumsup.7 ⊢ φ → ∃ x ∈ ℝ ∀ j ∈ Z G ⁡ j ≤ x
8 4 5 eqeltrd ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
9 1 3 8 serfre ⊢ φ → seq M + F : Z ⟶ ℝ
10 2 feq1i ⊢ G : Z ⟶ ℝ ↔ seq M + F : Z ⟶ ℝ
11 9 10 sylibr ⊢ φ → G : Z ⟶ ℝ
12 simpr ⊢ φ ∧ j ∈ Z → j ∈ Z
13 12 1 eleqtrdi ⊢ φ ∧ j ∈ Z → j ∈ ℤ ≥ M
14 eluzelz ⊢ j ∈ ℤ ≥ M → j ∈ ℤ
15 uzid ⊢ j ∈ ℤ → j ∈ ℤ ≥ j
16 peano2uz ⊢ j ∈ ℤ ≥ j → j + 1 ∈ ℤ ≥ j
17 13 14 15 16 4syl ⊢ φ ∧ j ∈ Z → j + 1 ∈ ℤ ≥ j
18 simpl ⊢ φ ∧ j ∈ Z → φ
19 elfzuz ⊢ k ∈ M … j + 1 → k ∈ ℤ ≥ M
20 19 1 eleqtrrdi ⊢ k ∈ M … j + 1 → k ∈ Z
21 18 20 8 syl2an ⊢ φ ∧ j ∈ Z ∧ k ∈ M … j + 1 → F ⁡ k ∈ ℝ
22 1 peano2uzs ⊢ j ∈ Z → j + 1 ∈ Z
23 22 adantl ⊢ φ ∧ j ∈ Z → j + 1 ∈ Z
24 elfzuz ⊢ k ∈ j + 1 … j + 1 → k ∈ ℤ ≥ j + 1
25 1 uztrn2 ⊢ j + 1 ∈ Z ∧ k ∈ ℤ ≥ j + 1 → k ∈ Z
26 23 24 25 syl2an ⊢ φ ∧ j ∈ Z ∧ k ∈ j + 1 … j + 1 → k ∈ Z
27 6 4 breqtrrd ⊢ φ ∧ k ∈ Z → 0 ≤ F ⁡ k
28 27 adantlr ⊢ φ ∧ j ∈ Z ∧ k ∈ Z → 0 ≤ F ⁡ k
29 26 28 syldan ⊢ φ ∧ j ∈ Z ∧ k ∈ j + 1 … j + 1 → 0 ≤ F ⁡ k
30 13 17 21 29 sermono ⊢ φ ∧ j ∈ Z → seq M + F ⁡ j ≤ 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 ⊢ φ ∧ j ∈ Z → G ⁡ j ≤ G ⁡ j + 1
34 1 3 11 33 7 climsup ⊢ φ → G ⇝ sup ran ⁡ G ℝ <