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

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 ffvelcdmda ⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ℕ ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 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 [,) +∞ ) )