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 [,) +∞ ) )