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 𝐺 , ℝ , < ) )