Metamath Proof Explorer

Theorem itg2cl

Description: The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg2cl ⊢ F : ℝ ⟶ 0 +∞ → ∫ 2 ⁡ F ∈ ℝ *

Proof

Step Hyp Ref Expression
1 eqid ⊢ x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f F ∧ x = ∫ 1 ⁡ g = x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f F ∧ x = ∫ 1 ⁡ g
2 1 itg2val ⊢ F : ℝ ⟶ 0 +∞ → ∫ 2 ⁡ F = sup x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f F ∧ x = ∫ 1 ⁡ g ℝ * <
3 1 itg2lcl ⊢ x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f F ∧ x = ∫ 1 ⁡ g ⊆ ℝ *
4 supxrcl ⊢ x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f F ∧ x = ∫ 1 ⁡ g ⊆ ℝ * → sup x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f F ∧ x = ∫ 1 ⁡ g ℝ * < ∈ ℝ *
5 3 4 ax-mp ⊢ sup x | ∃ g ∈ dom ⁡ ∫ 1 g ≤ f F ∧ x = ∫ 1 ⁡ g ℝ * < ∈ ℝ *
6 2 5 eqeltrdi ⊢ F : ℝ ⟶ 0 +∞ → ∫ 2 ⁡ F ∈ ℝ *