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 ⊢ G = abs ∘ − ∘ F
ovolfs.2 ⊢ S = seq 1 + G
Assertion ovolsf ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 → S : ℕ ⟶ 0 +∞

Proof

Step Hyp Ref Expression
1 ovolfs.1 ⊢ G = abs ∘ − ∘ F
2 ovolfs.2 ⊢ S = seq 1 + G
3 nnuz ⊢ ℕ = ℤ ≥ 1
4 1zzd ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 → 1 ∈ ℤ
5 1 ovolfsf ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 → G : ℕ ⟶ 0 +∞
6 5 ffvelrnda ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ x ∈ ℕ → G ⁡ x ∈ 0 +∞
7 ge0addcl ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y ∈ 0 +∞
8 7 adantl ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y ∈ 0 +∞
9 3 4 6 8 seqf ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 → seq 1 + G : ℕ ⟶ 0 +∞
10 2 feq1i ⊢ S : ℕ ⟶ 0 +∞ ↔ seq 1 + G : ℕ ⟶ 0 +∞
11 9 10 sylibr ⊢ F : ℕ ⟶ ≤ ∩ ℝ 2 → S : ℕ ⟶ 0 +∞