This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isumsup.2 ⊢ 𝐺 = seq 𝑀 ( + , 𝐹 )
isumsup.3 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isumsup.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
isumsup.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
isumsup.6 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐴 )
isumsup.7 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐺 ‘ 𝑗 ) ≤ 𝑥 )
Assertion isumsup ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = 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 5 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
9 1 2 3 4 5 6 7 isumsup2 ⊢ ( 𝜑 → 𝐺 ⇝ sup ( ran 𝐺 , ℝ , < ) )
10 2 9 eqbrtrrid ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ sup ( ran 𝐺 , ℝ , < ) )
11 1 3 4 8 10 isumclim ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = sup ( ran 𝐺 , ℝ , < ) )