P. 258 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25701-25800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mbfmulc2lem 25701	Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f · 𝐹) ∈ MblFn)
Theorem	mbfmulc2re 25702	Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 × {𝐵}) ∘f · 𝐹) ∈ MblFn)
Theorem	mbfmax 25703*	The maximum of two functions is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ if((𝐹‘𝑥) ≤ (𝐺‘𝑥), (𝐺‘𝑥), (𝐹‘𝑥)))    ⇒   ⊢ (𝜑 → 𝐻 ∈ MblFn)
Theorem	mbfneg 25704*	The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ MblFn)
Theorem	mbfpos 25705*	The positive part of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)
Theorem	mbfposr 25706*	Converse to mbfpos 25705. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)
Theorem	mbfposb 25707*	A function is measurable iff its positive and negative parts are measurable. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ MblFn ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ MblFn)))
Theorem	ismbf3d 25708*	Simplified form of ismbfd 25693. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (◡𝐹 “ (𝑥(,)+∞)) ∈ dom vol)    ⇒   ⊢ (𝜑 → 𝐹 ∈ MblFn)
Theorem	mbfimaopnlem 25709*	Lemma for mbfimaopn 25710. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐺 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    &   ⊢ 𝐵 = ((,) “ (ℚ × ℚ))    &   ⊢ 𝐾 = ran (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ dom vol)
Theorem	mbfimaopn 25710	The preimage of any open set (in the complex topology) under a measurable function is measurable. (See also cncombf 25712, which explains why 𝐴 ∈ dom vol is too weak a condition for this theorem.) (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ 𝐽) → (◡𝐹 “ 𝐴) ∈ dom vol)
Theorem	mbfimaopn2 25711	The preimage of any set open in the subspace topology of the range of the function is measurable. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝐵)    ⇒   ⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ ℂ) ∧ 𝐶 ∈ 𝐾) → (◡𝐹 “ 𝐶) ∈ dom vol)
Theorem	cncombf 25712	The composition of a continuous function with a measurable function is measurable. (More generally, 𝐺 can be a Borel-measurable function, but notably the condition that 𝐺 be only measurable is too weak, the usual counterexample taking 𝐺 to be the Cantor function and 𝐹 the indicator function of the 𝐺-image of a nonmeasurable set, which is a subset of the Cantor set and hence null and measurable.) (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (𝐺 ∘ 𝐹) ∈ MblFn)
Theorem	cnmbf 25713	A continuous function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 26-Mar-2015.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) → 𝐹 ∈ MblFn)
Theorem	mbfaddlem 25714	The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn)
Theorem	mbfadd 25715	The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn)
Theorem	mbfsub 25716	The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝐹 ∘f − 𝐺) ∈ MblFn)
Theorem	mbfmulc2 25717*	A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ MblFn)
Theorem	mbfsup 25718*	The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, 𝐵(𝑛, 𝑥) is a function of both 𝑛 and 𝑥, since it is an 𝑛-indexed sequence of functions on 𝑥. (Contributed by Mario Carneiro, 14-Aug-2014.) (Revised by Mario Carneiro, 7-Sep-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝐵 ≤ 𝑦)    ⇒   ⊢ (𝜑 → 𝐺 ∈ MblFn)
Theorem	mbfinf 25719*	The infimum of a sequence of measurable, real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 13-Sep-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ 𝐵), ℝ, < ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐺 ∈ MblFn)
Theorem	mbflimsup 25720*	The limit supremum of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.) (Revised by AV, 12-Sep-2020.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)))    &   ⊢ 𝐻 = (𝑚 ∈ ℝ ↦ sup((((𝑛 ∈ 𝑍 ↦ 𝐵) “ (𝑚[,)+∞)) ∩ ℝ*), ℝ*, < ))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (lim sup‘(𝑛 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐺 ∈ MblFn)
Theorem	mbflimlem 25721*	The pointwise limit of a sequence of measurable real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
Theorem	mbflim 25722*	The pointwise limit of a sequence of measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ 𝑍 ↦ 𝐵) ⇝ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴)) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
Syntax	c0p 25723	Extend class notation to include the zero polynomial.
class 0𝑝
Definition	df-0p 25724	Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ 0𝑝 = (ℂ × {0})
Theorem	0pval 25725	The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014.)
⊢ (𝐴 ∈ ℂ → (0𝑝‘𝐴) = 0)
Theorem	0plef 25726	Two ways to say that the function 𝐹 on the reals is nonnegative. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝐹:ℝ⟶(0[,)+∞) ↔ (𝐹:ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ 𝐹))
Theorem	0pledm 25727	Adjust the domain of the left argument to match the right, which works better in our theorems. (Contributed by Mario Carneiro, 28-Jul-2014.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐹 Fn 𝐴)    ⇒   ⊢ (𝜑 → (0𝑝 ∘r ≤ 𝐹 ↔ (𝐴 × {0}) ∘r ≤ 𝐹))
Theorem	isi1f 25728	The predicate "𝐹 is a simple function". A simple function is a finite nonnegative linear combination of indicator functions for finitely measurable sets. We use the idiom 𝐹 ∈ dom ∫1 to represent this concept because ∫1 is the first preparation function for our final definition ∫ (see df-itg 25677); unlike that operator, which can integrate any function, this operator can only integrate simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
Theorem	i1fmbf 25729	Simple functions are measurable. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐹 ∈ dom ∫1 → 𝐹 ∈ MblFn)
Theorem	i1ff 25730	A simple function is a function on the reals. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ (𝐹 ∈ dom ∫1 → 𝐹:ℝ⟶ℝ)
Theorem	i1frn 25731	A simple function has finite range. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ (𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin)
Theorem	i1fima 25732	Any preimage of a simple function is measurable. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ (𝐹 ∈ dom ∫1 → (◡𝐹 “ 𝐴) ∈ dom vol)
Theorem	i1fima2 25733	Any preimage of a simple function not containing zero has finite measure. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ ((𝐹 ∈ dom ∫1 ∧ ¬ 0 ∈ 𝐴) → (vol‘(◡𝐹 “ 𝐴)) ∈ ℝ)
Theorem	i1fima2sn 25734	Preimage of a singleton. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ (𝐵 ∖ {0})) → (vol‘(◡𝐹 “ {𝐴})) ∈ ℝ)
Theorem	i1fd 25735*	A simplified set of assumptions to show that a given function is simple. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    &   ⊢ (𝜑 → ran 𝐹 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom ∫1)
Theorem	i1f0rn 25736	Any simple function takes the value zero on a set of unbounded measure, so in particular this set is not empty. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐹 ∈ dom ∫1 → 0 ∈ ran 𝐹)
Theorem	itg1val 25737*	The value of the integral on simple functions. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝐹 ∈ dom ∫1 → (∫1‘𝐹) = Σ𝑥 ∈ (ran 𝐹 ∖ {0})(𝑥 · (vol‘(◡𝐹 “ {𝑥}))))
Theorem	itg1val2 25738*	The value of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ ((𝐹 ∈ dom ∫1 ∧ (𝐴 ∈ Fin ∧ (ran 𝐹 ∖ {0}) ⊆ 𝐴 ∧ 𝐴 ⊆ (ℝ ∖ {0}))) → (∫1‘𝐹) = Σ𝑥 ∈ 𝐴 (𝑥 · (vol‘(◡𝐹 “ {𝑥}))))
Theorem	itg1cl 25739	Closure of the integral on simple functions. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ (𝐹 ∈ dom ∫1 → (∫1‘𝐹) ∈ ℝ)
Theorem	itg1ge0 25740	Closure of the integral on positive simple functions. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹) → 0 ≤ (∫1‘𝐹))
Theorem	i1f0 25741	The zero function is simple. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (ℝ × {0}) ∈ dom ∫1
Theorem	itg10 25742	The zero function has zero integral. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (∫1‘(ℝ × {0})) = 0
Theorem	i1f1lem 25743*	Lemma for i1f1 25744 and itg11 25745. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0))    ⇒   ⊢ (𝐹:ℝ⟶{0, 1} ∧ (𝐴 ∈ dom vol → (◡𝐹 “ {1}) = 𝐴))
Theorem	i1f1 25744*	Base case simple functions are indicator functions of measurable sets. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0))    ⇒   ⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → 𝐹 ∈ dom ∫1)
Theorem	itg11 25745*	The integral of an indicator function is the volume of the set. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 1, 0))    ⇒   ⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ) → (∫1‘𝐹) = (vol‘𝐴))
Theorem	itg1addlem1 25746*	Decompose a preimage, which is always a disjoint union. (Contributed by Mario Carneiro, 25-Jun-2014.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ (◡𝐹 “ {𝑘}))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (vol‘𝐵) ∈ ℝ)    ⇒   ⊢ (𝜑 → (vol‘∪ 𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (vol‘𝐵))
Theorem	i1faddlem 25747*	Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℂ) → (◡(𝐹 ∘f + 𝐺) “ {𝐴}) = ∪ 𝑦 ∈ ran 𝐺((◡𝐹 “ {(𝐴 − 𝑦)}) ∩ (◡𝐺 “ {𝑦})))
Theorem	i1fmullem 25748*	Decompose the preimage of a product. (Contributed by Mario Carneiro, 19-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (ℂ ∖ {0})) → (◡(𝐹 ∘f · 𝐺) “ {𝐴}) = ∪ 𝑦 ∈ (ran 𝐺 ∖ {0})((◡𝐹 “ {(𝐴 / 𝑦)}) ∩ (◡𝐺 “ {𝑦})))
Theorem	i1fadd 25749	The sum of two simple functions is a simple function. (Contributed by Mario Carneiro, 18-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    ⇒   ⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ dom ∫1)
Theorem	i1fmul 25750	The pointwise product of two simple functions is a simple function. (Contributed by Mario Carneiro, 5-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ dom ∫1)
Theorem	itg1addlem2 25751*	Lemma for itg1add 25756. The function 𝐼 represents the pieces into which we will break up the domain of the sum. Since it is infinite only when both 𝑖 and 𝑗 are zero, we arbitrarily define it to be zero there to simplify the sums that are manipulated in itg1addlem4 25753 and itg1addlem5 25755. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))))    ⇒   ⊢ (𝜑 → 𝐼:(ℝ × ℝ)⟶ℝ)
Theorem	itg1addlem3 25752*	Lemma for itg1add 25756. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))))    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴𝐼𝐵) = (vol‘((◡𝐹 “ {𝐴}) ∩ (◡𝐺 “ {𝐵}))))
Theorem	itg1addlem4 25753*	Lemma for itg1add 25756. (Contributed by Mario Carneiro, 28-Jun-2014.) (Proof shortened by SN, 3-Oct-2024.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))))    &   ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))    ⇒   ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
Theorem	itg1addlem4OLD 25754*	Obsolete version of itg1addlem4 25753 as of 6-Oct-2024. (Contributed by Mario Carneiro, 28-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))))    &   ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))    ⇒   ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
Theorem	itg1addlem5 25755*	Lemma for itg1add 25756. (Contributed by Mario Carneiro, 27-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))))    &   ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))    ⇒   ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = ((∫1‘𝐹) + (∫1‘𝐺)))
Theorem	itg1add 25756	The integral of a sum of simple functions is the sum of the integrals. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    ⇒   ⊢ (𝜑 → (∫1‘(𝐹 ∘f + 𝐺)) = ((∫1‘𝐹) + (∫1‘𝐺)))
Theorem	i1fmulclem 25757	Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝐵}) = (◡𝐹 “ {(𝐵 / 𝐴)}))
Theorem	i1fmulc 25758	A nonnegative constant times a simple function gives another simple function. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((ℝ × {𝐴}) ∘f · 𝐹) ∈ dom ∫1)
Theorem	itg1mulc 25759	The integral of a constant times a simple function is the constant times the original integral. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (∫1‘((ℝ × {𝐴}) ∘f · 𝐹)) = (𝐴 · (∫1‘𝐹)))
Theorem	i1fres 25760*	The "restriction" of a simple function to a measurable subset is simple. (It's not actually a restriction because it is zero instead of undefined outside 𝐴.) (Contributed by Mario Carneiro, 29-Jun-2014.)
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (𝐹‘𝑥), 0))    ⇒   ⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐴 ∈ dom vol) → 𝐺 ∈ dom ∫1)
Theorem	i1fpos 25761*	The positive part of a simple function is simple. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(0 ≤ (𝐹‘𝑥), (𝐹‘𝑥), 0))    ⇒   ⊢ (𝐹 ∈ dom ∫1 → 𝐺 ∈ dom ∫1)
Theorem	i1fposd 25762*	Deduction form of i1fposd 25762. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝐴) ∈ dom ∫1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(0 ≤ 𝐴, 𝐴, 0)) ∈ dom ∫1)
Theorem	i1fsub 25763	The difference of two simple functions is a simple function. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐹 ∘f − 𝐺) ∈ dom ∫1)
Theorem	itg1sub 25764	The integral of a difference of two simple functions. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (∫1‘(𝐹 ∘f − 𝐺)) = ((∫1‘𝐹) − (∫1‘𝐺)))
Theorem	itg10a 25765*	The integral of a simple function supported on a nullset is zero. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) = 0)    ⇒   ⊢ (𝜑 → (∫1‘𝐹) = 0)
Theorem	itg1ge0a 25766*	The integral of an almost positive simple function is positive. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → 0 ≤ (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 0 ≤ (∫1‘𝐹))
Theorem	itg1lea 25767*	Approximate version of itg1le 25768. If 𝐹 ≤ 𝐺 for almost all 𝑥, then ∫1𝐹 ≤ ∫1𝐺. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 6-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) ≤ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (∫1‘𝐹) ≤ (∫1‘𝐺))
Theorem	itg1le 25768	If one simple function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐺) → (∫1‘𝐹) ≤ (∫1‘𝐺))
Theorem	itg1climres 25769*	Restricting the simple function 𝐹 to the increasing sequence 𝐴(𝑛) of measurable sets whose union is ℝ yields a sequence of simple functions whose integrals approach the integral of 𝐹. (Contributed by Mario Carneiro, 15-Aug-2014.)
⊢ (𝜑 → 𝐴:ℕ⟶dom vol)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ (𝐴‘(𝑛 + 1)))    &   ⊢ (𝜑 → ∪ ran 𝐴 = ℝ)    &   ⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝐴‘𝑛), (𝐹‘𝑥), 0))    ⇒   ⊢ (𝜑 → (𝑛 ∈ ℕ ↦ (∫1‘𝐺)) ⇝ (∫1‘𝐹))
Theorem	mbfi1fseqlem1 25770*	Lemma for mbfi1fseq 25776. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    ⇒   ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
Theorem	mbfi1fseqlem2 25771*	Lemma for mbfi1fseq 25776. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))    ⇒   ⊢ (𝐴 ∈ ℕ → (𝐺‘𝐴) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝐴[,]𝐴), if((𝐴𝐽𝑥) ≤ 𝐴, (𝐴𝐽𝑥), 𝐴), 0)))
Theorem	mbfi1fseqlem3 25772*	Lemma for mbfi1fseq 25776. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
Theorem	mbfi1fseqlem4 25773*	Lemma for mbfi1fseq 25776. This lemma is not as interesting as it is long - it is simply checking that 𝐺 is in fact a sequence of simple functions, by verifying that its range is in (0...𝑛2↑𝑛) / (2↑𝑛) (which is to say, the numbers from 0 to 𝑛 in increments of 1 / (2↑𝑛)), and also that the preimage of each point 𝑘 is measurable, because it is equal to (-𝑛[,]𝑛) ∩ (◡𝐹 “ (𝑘[,)𝑘 + 1 / (2↑𝑛))) for 𝑘 < 𝑛 and (-𝑛[,]𝑛) ∩ (◡𝐹 “ (𝑘[,)+∞)) for 𝑘 = 𝑛. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))    ⇒   ⊢ (𝜑 → 𝐺:ℕ⟶dom ∫1)
Theorem	mbfi1fseqlem5 25774*	Lemma for mbfi1fseq 25776. Verify that 𝐺 describes an increasing sequence of positive functions. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0𝑝 ∘r ≤ (𝐺‘𝐴) ∧ (𝐺‘𝐴) ∘r ≤ (𝐺‘(𝐴 + 1))))
Theorem	mbfi1fseqlem6 25775*	Lemma for mbfi1fseq 25776. Verify that 𝐺 converges pointwise to 𝐹, and wrap up the existential quantifier. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))    ⇒   ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
Theorem	mbfi1fseq 25776*	A characterization of measurability in terms of simple functions (this is an if and only if for nonnegative functions, although we don't prove it). Any nonnegative measurable function is the limit of an increasing sequence of nonnegative simple functions. This proof is an example of a poor de Bruijn factor - the formalized proof is much longer than an average hand proof, which usually just describes the function 𝐺 and "leaves the details as an exercise to the reader". (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    ⇒   ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
Theorem	mbfi1flimlem 25777*	Lemma for mbfi1flim 25778. (Contributed by Mario Carneiro, 5-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    ⇒   ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
Theorem	mbfi1flim 25778*	Any real measurable function has a sequence of simple functions that converges to it. (Contributed by Mario Carneiro, 5-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ 𝐴 (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
Theorem	mbfmullem2 25779*	Lemma for mbfmul 25781. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ (𝜑 → 𝑄:ℕ⟶dom ∫1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn)
Theorem	mbfmullem 25780	Lemma for mbfmul 25781. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn)
Theorem	mbfmul 25781	The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn)
Theorem	itg2lcl 25782*	The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ 𝐿 ⊆ ℝ*
Theorem	itg2val 25783*	Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) = sup(𝐿, ℝ*, < ))
Theorem	itg2l 25784*	Elementhood in the set 𝐿 of lower sums of the integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ (𝐴 ∈ 𝐿 ↔ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = (∫1‘𝑔)))
Theorem	itg2lr 25785*	Sufficient condition for elementhood in the set 𝐿. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹) → (∫1‘𝐺) ∈ 𝐿)
Theorem	xrge0f 25786	A real function is a nonnegative extended real function if all its values are greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 28-Jul-2014.)
⊢ ((𝐹:ℝ⟶ℝ ∧ 0𝑝 ∘r ≤ 𝐹) → 𝐹:ℝ⟶(0[,]+∞))
Theorem	itg2cl 25787	The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*)
Theorem	itg2ub 25788	The integral of a nonnegative real function 𝐹 is an upper bound on the integrals of all simple functions 𝐺 dominated by 𝐹. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹) → (∫1‘𝐺) ≤ (∫2‘𝐹))
Theorem	itg2leub 25789*	Any upper bound on the integrals of all simple functions 𝐺 dominated by 𝐹 is greater than (∫2‘𝐹), the least upper bound. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐴 ∈ ℝ*) → ((∫2‘𝐹) ≤ 𝐴 ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 → (∫1‘𝑔) ≤ 𝐴)))
Theorem	itg2ge0 25790	The integral of a nonnegative real function is greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝐹:ℝ⟶(0[,]+∞) → 0 ≤ (∫2‘𝐹))
Theorem	itg2itg1 25791	The integral of a nonnegative simple function using ∫2 is the same as its value under ∫1. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹) → (∫2‘𝐹) = (∫1‘𝐹))
Theorem	itg20 25792	The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (∫2‘(ℝ × {0})) = 0
Theorem	itg2lecl 25793	If an ∫2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐴 ∈ ℝ ∧ (∫2‘𝐹) ≤ 𝐴) → (∫2‘𝐹) ∈ ℝ)
Theorem	itg2le 25794	If one function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐺:ℝ⟶(0[,]+∞) ∧ 𝐹 ∘r ≤ 𝐺) → (∫2‘𝐹) ≤ (∫2‘𝐺))
Theorem	itg2const 25795*	Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ ∧ 𝐵 ∈ (0[,)+∞)) → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) = (𝐵 · (vol‘𝐴)))
Theorem	itg2const2 25796*	When the base set of a constant function has infinite volume, the integral is also infinite and vice-versa. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ+) → ((vol‘𝐴) ∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ))
Theorem	itg2seq 25797*	Definitional property of the ∫2 integral: for any function 𝐹 there is a countable sequence 𝑔 of simple functions less than 𝐹 whose integrals converge to the integral of 𝐹. (This theorem is for the most part unnecessary in lieu of itg2i1fseq 25810, but unlike that theorem this one doesn't require 𝐹 to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014.)
⊢ (𝐹:ℝ⟶(0[,]+∞) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘r ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < )))
Theorem	itg2uba 25798*	Approximate version of itg2ub 25788. If 𝐹 approximately dominates 𝐺, then ∫1𝐺 ≤ ∫2𝐹. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐺‘𝑥) ≤ (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → (∫1‘𝐺) ≤ (∫2‘𝐹))
Theorem	itg2lea 25799*	Approximate version of itg2le 25794. If 𝐹 ≤ 𝐺 for almost all 𝑥, then ∫2𝐹 ≤ ∫2𝐺. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) ≤ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (∫2‘𝐹) ≤ (∫2‘𝐺))
Theorem	itg2eqa 25800*	Approximate equality of integrals. If 𝐹 = 𝐺 for almost all 𝑥, then ∫2𝐹 = ∫2𝐺. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (∫2‘𝐹) = (∫2‘𝐺))