# Metamath Proof Explorer

## Theorem ovolsf

Description: Closure for the partial sums of the interval length function. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypotheses ovolfs.1 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
ovolfs.2 𝑆 = seq 1 ( + , 𝐺 )
Assertion ovolsf ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )

### Proof

Step Hyp Ref Expression
1 ovolfs.1 𝐺 = ( ( abs ∘ − ) ∘ 𝐹 )
2 ovolfs.2 𝑆 = seq 1 ( + , 𝐺 )
3 nnuz ℕ = ( ℤ ‘ 1 )
4 1zzd ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 1 ∈ ℤ )
5 1 ovolfsf ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐺 : ℕ ⟶ ( 0 [,) +∞ ) )
6 5 ffvelrnda ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺𝑥 ) ∈ ( 0 [,) +∞ ) )
7 ge0addcl ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
8 7 adantl ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
9 3 4 6 8 seqf ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → seq 1 ( + , 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) )
10 2 feq1i ( 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) ↔ seq 1 ( + , 𝐺 ) : ℕ ⟶ ( 0 [,) +∞ ) )
11 9 10 sylibr ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝑆 : ℕ ⟶ ( 0 [,) +∞ ) )