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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isumsup.2 ⊢ 𝐺 = seq 𝑀 ( + , 𝐹 )
isumsup.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isumsup.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
isumsup.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
isumsup.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐴 )
isumsup.7 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 )
Assertion isumsup2 ( 𝜑 → 𝐺 ⇝ 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 4 5 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
9 1 3 8 serfre ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
10 2 feq1i ⊢ ( 𝐺 : 𝑍 ⟶ ℝ ↔ seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
11 9 10 sylibr ⊢ ( 𝜑 → 𝐺 : 𝑍 ⟶ ℝ )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ 𝑍 )
13 12 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) )
14 eluzelz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑗 ∈ ℤ )
15 uzid ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) )
16 peano2uz ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
17 13 14 15 16 4syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝑗 + 1 ) ∈ ( ℤ≥ ‘ 𝑗 ) )
18 simpl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝜑 )
19 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
20 19 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) → 𝑘 ∈ 𝑍 )
21 18 20 8 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑗 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
22 1 peano2uzs ⊢ ( 𝑗 ∈ 𝑍 → ( 𝑗 + 1 ) ∈ 𝑍 )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝑗 + 1 ) ∈ 𝑍 )
24 elfzuz ⊢ ( 𝑘 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) )
25 1 uztrn2 ⊢ ( ( ( 𝑗 + 1 ) ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑗 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
26 23 24 25 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
27 6 4 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
28 27 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
29 26 28 syldan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ( 𝑗 + 1 ) ... ( 𝑗 + 1 ) ) ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
30 13 17 21 29 sermono ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + 1 ) ) )
31 2 fveq1i ⊢ ( 𝐺 ‘ 𝑗 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 )
32 2 fveq1i ⊢ ( 𝐺 ‘ ( 𝑗 + 1 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + 1 ) )
33 30 31 32 3brtr4g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑗 ) ≤ ( 𝐺 ‘ ( 𝑗 + 1 ) ) )
34 1 3 11 33 7 climsup ⊢ ( 𝜑 → 𝐺 ⇝ sup ( ran 𝐺 , ℝ , < ) )