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	itg2cl 25701	The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*)
Theorem	itg2ub 25702	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 25703*	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 25704	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 25705	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 25706	The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (∫2‘(ℝ × {0})) = 0
Theorem	itg2lecl 25707	If an ∫2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐴 ∈ ℝ ∧ (∫2‘𝐹) ≤ 𝐴) → (∫2‘𝐹) ∈ ℝ)
Theorem	itg2le 25708	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 25709*	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 25710*	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 25711*	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 25724, 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 25712*	Approximate version of itg2ub 25702. If 𝐹 approximately dominates 𝐺, then ∫1𝐺 ≤ ∫2𝐹. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐺‘𝑥) ≤ (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → (∫1‘𝐺) ≤ (∫2‘𝐹))
Theorem	itg2lea 25713*	Approximate version of itg2le 25708. If 𝐹 ≤ 𝐺 for almost all 𝑥, then ∫2𝐹 ≤ ∫2𝐺. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) ≤ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (∫2‘𝐹) ≤ (∫2‘𝐺))
Theorem	itg2eqa 25714*	Approximate equality of integrals. If 𝐹 = 𝐺 for almost all 𝑥, then ∫2𝐹 = ∫2𝐺. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) = (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (∫2‘𝐹) = (∫2‘𝐺))
Theorem	itg2mulclem 25715	Lemma for itg2mulc 25716. (Contributed by Mario Carneiro, 8-Jul-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ≤ (𝐴 · (∫2‘𝐹)))
Theorem	itg2mulc 25716	The integral of a nonnegative constant times a function is the constant times the integral of the original function. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → (∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) = (𝐴 · (∫2‘𝐹)))
Theorem	itg2splitlem 25717*	Lemma for itg2split 25718. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ (𝜑 → 𝐵 ∈ dom vol)    &   ⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0)    &   ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞))    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0))    &   ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ)    ⇒   ⊢ (𝜑 → (∫2‘𝐻) ≤ ((∫2‘𝐹) + (∫2‘𝐺)))
Theorem	itg2split 25718*	The ∫2 integral splits under an almost disjoint union. The proof avoids the use of itg2add 25728, which requires countable choice. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ (𝜑 → 𝐵 ∈ dom vol)    &   ⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0)    &   ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ (0[,]+∞))    &   ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐶, 0))    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, 𝐶, 0))    &   ⊢ 𝐻 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, 𝐶, 0))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ)    ⇒   ⊢ (𝜑 → (∫2‘𝐻) = ((∫2‘𝐹) + (∫2‘𝐺)))
Theorem	itg2monolem1 25719*	Lemma for itg2mono 25722. We show that for any constant 𝑡 less than one, 𝑡 · ∫1𝐻 is less than 𝑆, and so ∫1𝐻 ≤ 𝑆, which is one half of the equality in itg2mono 25722. Consider the sequence 𝐴(𝑛) = {𝑥 ∣ 𝑡 · 𝐻 ≤ 𝐹(𝑛)}. This is an increasing sequence of measurable sets whose union is ℝ, and so 𝐻 ↾ 𝐴(𝑛) has an integral which equals ∫1𝐻 in the limit, by itg1climres 25683. Then by taking the limit in (𝑡 · 𝐻) ↾ 𝐴(𝑛) ≤ 𝐹(𝑛), we get 𝑡 · ∫1𝐻 ≤ 𝑆 as desired. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)    &   ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )    &   ⊢ (𝜑 → 𝑇 ∈ (0(,)1))    &   ⊢ (𝜑 → 𝐻 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐻 ∘r ≤ 𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ ℝ)    &   ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})    ⇒   ⊢ (𝜑 → (𝑇 · (∫1‘𝐻)) ≤ 𝑆)
Theorem	itg2monolem2 25720*	Lemma for itg2mono 25722. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)    &   ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )    &   ⊢ (𝜑 → 𝑃 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝑃 ∘r ≤ 𝐺)    &   ⊢ (𝜑 → ¬ (∫1‘𝑃) ≤ 𝑆)    ⇒   ⊢ (𝜑 → 𝑆 ∈ ℝ)
Theorem	itg2monolem3 25721*	Lemma for itg2mono 25722. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)    &   ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )    &   ⊢ (𝜑 → 𝑃 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝑃 ∘r ≤ 𝐺)    &   ⊢ (𝜑 → ¬ (∫1‘𝑃) ≤ 𝑆)    ⇒   ⊢ (𝜑 → (∫1‘𝑃) ≤ 𝑆)
Theorem	itg2mono 25722*	The Monotone Convergence Theorem for nonnegative functions. If {(𝐹‘𝑛):𝑛 ∈ ℕ} is a monotone increasing sequence of positive, measurable, real-valued functions, and 𝐺 is the pointwise limit of the sequence, then (∫2‘𝐺) is the limit of the sequence {(∫2‘(𝐹‘𝑛)):𝑛 ∈ ℕ}. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)    &   ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )    ⇒   ⊢ (𝜑 → (∫2‘𝐺) = 𝑆)
Theorem	itg2i1fseqle 25723*	Subject to the conditions coming from mbfi1fseq 25690, the sequence of simple functions are all less than the target function 𝐹. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑃‘𝑀) ∘r ≤ 𝐹)
Theorem	itg2i1fseq 25724*	Subject to the conditions coming from mbfi1fseq 25690, the integral of the sequence of simple functions converges to the integral of the target function. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (∫1‘(𝑃‘𝑚)))    ⇒   ⊢ (𝜑 → (∫2‘𝐹) = sup(ran 𝑆, ℝ*, < ))
Theorem	itg2i1fseq2 25725*	In an extension to the results of itg2i1fseq 25724, if there is an upper bound on the integrals of the simple functions approaching 𝐹, then ∫2𝐹 is real and the standard limit relation applies. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (∫1‘(𝑃‘𝑚)))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑃‘𝑘)) ≤ 𝑀)    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (∫2‘𝐹))
Theorem	itg2i1fseq3 25726*	Special case of itg2i1fseq2 25725: if the integral of 𝐹 is a real number, then the standard limit relation holds on the integrals of simple functions approaching 𝐹. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (∫1‘(𝑃‘𝑚)))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (∫2‘𝐹))
Theorem	itg2addlem 25727*	Lemma for itg2add 25728. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ)    &   ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘r ≤ (𝑃‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ (𝜑 → 𝑄:ℕ⟶dom ∫1)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑄‘𝑛) ∧ (𝑄‘𝑛) ∘r ≤ (𝑄‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (∫2‘(𝐹 ∘f + 𝐺)) = ((∫2‘𝐹) + (∫2‘𝐺)))
Theorem	itg2add 25728	The ∫2 integral is linear. (Measurability is an essential component of this theorem; otherwise consider the characteristic function of a nonmeasurable set and its complement.) (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ)    ⇒   ⊢ (𝜑 → (∫2‘(𝐹 ∘f + 𝐺)) = ((∫2‘𝐹) + (∫2‘𝐺)))
Theorem	itg2gt0 25729*	If the function 𝐹 is strictly positive on a set of positive measure, then the integral of the function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ (𝜑 → 0 < (vol‘𝐴))    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 < (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → 0 < (∫2‘𝐹))
Theorem	itg2cnlem1 25730*	Lemma for itgcn 25814. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) = (∫2‘𝐹))
Theorem	itg2cnlem2 25731*	Lemma for itgcn 25814. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
Theorem	itg2cn 25732*	A sort of absolute continuity of the Lebesgue integral (this is the core of ftc1a 26012 which is about actual absolute continuity). (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
Theorem	ibllem 25733	Conditioned equality theorem for the if statement. (Contributed by Mario Carneiro, 31-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
Theorem	isibl 25734*	The predicate "𝐹 is integrable". The "integrable" predicate corresponds roughly to the range of validity of ∫𝐴𝐵 d𝑥, which is to say that the expression ∫𝐴𝐵 d𝑥 doesn't make sense unless (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝑘))))    &   ⊢ (𝜑 → dom 𝐹 = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ 𝐿1 ↔ (𝐹 ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘𝐺) ∈ ℝ)))
Theorem	isibl2 25735*	The predicate "𝐹 is integrable" when 𝐹 is a mapping operation. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝑘))))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘𝐺) ∈ ℝ)))
Theorem	iblmbf 25736	An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.)
⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
Theorem	iblitg 25737*	If a function is integrable, then the ∫2 integrals of the function's decompositions all exist. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝐾))))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) → (∫2‘𝐺) ∈ ℝ)
Theorem	dfitg 25738*	Evaluate the class substitution in df-itg 25592. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝑇 = (ℜ‘(𝐵 / (i↑𝑘)))    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))))
Theorem	itgex 25739	An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ∫𝐴𝐵 d𝑥 ∈ V
Theorem	itgeq1f 25740	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) Avoid axioms. (Revised by GG, 1-Sep-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)
Theorem	itgeq1fOLD 25741	Obsolete version of itgeq1f 25740 as of 1-Sep-2025. (Contributed by Mario Carneiro, 28-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)
Theorem	itgeq1 25742*	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝐴 = 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)
Theorem	nfitg1 25743	Bound-variable hypothesis builder for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ Ⅎ𝑥∫𝐴𝐵 d𝑥
Theorem	nfitg 25744*	Bound-variable hypothesis builder for an integral: if 𝑦 is (effectively) not free in 𝐴 and 𝐵, it is not free in ∫𝐴𝐵 d𝑥. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ Ⅎ𝑦𝐴    &   ⊢ Ⅎ𝑦𝐵    ⇒   ⊢ Ⅎ𝑦∫𝐴𝐵 d𝑥
Theorem	cbvitg 25745*	Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦
Theorem	cbvitgv 25746*	Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦
Theorem	itgeq2 25747	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥)
Theorem	itgresr 25748	The domain of an integral only matters in its intersection with ℝ. (Contributed by Mario Carneiro, 29-Jun-2014.)
⊢ ∫𝐴𝐵 d𝑥 = ∫(𝐴 ∩ ℝ)𝐵 d𝑥
Theorem	itg0 25749	The integral of anything on the empty set is zero. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ∫∅𝐴 d𝑥 = 0
Theorem	itgz 25750	The integral of zero on any set is zero. (Contributed by Mario Carneiro, 29-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ∫𝐴0 d𝑥 = 0
Theorem	itgeq2dv 25751*	Equality theorem for an integral. (Contributed by Mario Carneiro, 7-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥)
Theorem	itgmpt 25752*	Change bound variable in an integral. (Contributed by Mario Carneiro, 29-Jun-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) d𝑦)
Theorem	itgcl 25753*	The integral of an integrable function is a complex number. This is Metamath 100 proof #86. (Contributed by Mario Carneiro, 29-Jun-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℂ)
Theorem	itgvallem 25754*	Substitution lemma. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (i↑𝐾) = 𝑇    ⇒   ⊢ (𝑘 = 𝐾 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / 𝑇))), (ℜ‘(𝐵 / 𝑇)), 0))))
Theorem	itgvallem3 25755*	Lemma for itgposval 25765 and itgreval 25766. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 0)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) = 0)
Theorem	ibl0 25756	The zero function is integrable on any measurable set. (Unlike iblconst 25787, this does not require 𝐴 to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (𝐴 ∈ dom vol → (𝐴 × {0}) ∈ 𝐿1)
Theorem	iblcnlem1 25757*	Lemma for iblcnlem 25758. (Contributed by Mario Carneiro, 6-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))    &   ⊢ 𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)))    &   ⊢ 𝑇 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)))    &   ⊢ 𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))
Theorem	iblcnlem 25758*	Expand out the universal quantifier in isibl2 25735. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))    &   ⊢ 𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)))    &   ⊢ 𝑇 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)))    &   ⊢ 𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ))))
Theorem	itgcnlem 25759*	Expand out the sum in dfitg 25738. (Contributed by Mario Carneiro, 1-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝑅 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘𝐵)), (ℜ‘𝐵), 0)))    &   ⊢ 𝑆 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℜ‘𝐵)), -(ℜ‘𝐵), 0)))    &   ⊢ 𝑇 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℑ‘𝐵)), (ℑ‘𝐵), 0)))    &   ⊢ 𝑈 = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -(ℑ‘𝐵)), -(ℑ‘𝐵), 0)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ((𝑅 − 𝑆) + (i · (𝑇 − 𝑈))))
Theorem	iblrelem 25760*	Integrability of a real function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ ∧ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) ∈ ℝ)))
Theorem	iblposlem 25761*	Lemma for iblpos 25762. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) = 0)
Theorem	iblpos 25762*	Integrability of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))) ∈ ℝ)))
Theorem	iblre 25763*	Integrability of a real function. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿1)))
Theorem	itgrevallem1 25764*	Lemma for itgposval 25765 and itgreval 25766. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) − (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0)))))
Theorem	itgposval 25765*	The integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, 𝐵, 0))))
Theorem	itgreval 25766*	Decompose the integral of a real function into positive and negative parts. (Contributed by Mario Carneiro, 31-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴if(0 ≤ 𝐵, 𝐵, 0) d𝑥 − ∫𝐴if(0 ≤ -𝐵, -𝐵, 0) d𝑥))
Theorem	itgrecl 25767*	Real closure of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℝ)
Theorem	iblcn 25768*	Integrability of a complex function. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)))
Theorem	itgcnval 25769*	Decompose the integral of a complex function into real and imaginary parts. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = (∫𝐴(ℜ‘𝐵) d𝑥 + (i · ∫𝐴(ℑ‘𝐵) d𝑥)))
Theorem	itgre 25770*	Real part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (ℜ‘∫𝐴𝐵 d𝑥) = ∫𝐴(ℜ‘𝐵) d𝑥)
Theorem	itgim 25771*	Imaginary part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (ℑ‘∫𝐴𝐵 d𝑥) = ∫𝐴(ℑ‘𝐵) d𝑥)
Theorem	iblneg 25772*	The negative of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ 𝐿1)
Theorem	itgneg 25773*	Negation of an integral. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → -∫𝐴𝐵 d𝑥 = ∫𝐴-𝐵 d𝑥)
Theorem	iblss 25774*	A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)
Theorem	iblss2 25775*	Change the domain of an integrability predicate. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1)
Theorem	itgitg2 25776*	Transfer an integral using ∫2 to an equivalent integral using ∫. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝐴)    &   ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝐴) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫ℝ𝐴 d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ 𝐴)))
Theorem	i1fibl 25777	A simple function is integrable. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝐹 ∈ dom ∫1 → 𝐹 ∈ 𝐿1)
Theorem	itgitg1 25778*	Transfer an integral using ∫1 to an equivalent integral using ∫. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝐹 ∈ dom ∫1 → ∫ℝ(𝐹‘𝑥) d𝑥 = (∫1‘𝐹))
Theorem	itgle 25779*	Monotonicity of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ≤ ∫𝐴𝐶 d𝑥)
Theorem	itgge0 25780*	The integral of a positive function is positive. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ ∫𝐴𝐵 d𝑥)
Theorem	itgss 25781*	Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)
Theorem	itgss2 25782*	Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝐴 ⊆ 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵if(𝑥 ∈ 𝐴, 𝐶, 0) d𝑥)
Theorem	itgeqa 25783*	Approximate equality of integrals. If 𝐶(𝑥) = 𝐷(𝑥) for almost all 𝑥, then ∫𝐵𝐶(𝑥) d𝑥 = ∫𝐵𝐷(𝑥) d𝑥 and one is integrable iff the other is. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Mario Carneiro, 2-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 𝐷)    ⇒   ⊢ (𝜑 → (((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1 ↔ (𝑥 ∈ 𝐵 ↦ 𝐷) ∈ 𝐿1) ∧ ∫𝐵𝐶 d𝑥 = ∫𝐵𝐷 d𝑥))
Theorem	itgss3 25784*	Expand the set of an integral by a nullset. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Mario Carneiro, 2-Sep-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘(𝐵 ∖ 𝐴)) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1 ↔ (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1) ∧ ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥))
Theorem	itgioo 25785*	Equality of integrals on open and closed intervals. (Contributed by Mario Carneiro, 2-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)𝐶 d𝑥 = ∫(𝐴[,]𝐵)𝐶 d𝑥)
Theorem	itgless 25786*	Expand the integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 0 ≤ 𝐶)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 ≤ ∫𝐵𝐶 d𝑥)
Theorem	iblconst 25787	A constant function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℂ) → (𝐴 × {𝐵}) ∈ 𝐿1)
Theorem	itgconst 25788*	Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℂ) → ∫𝐴𝐵 d𝑥 = (𝐵 · (vol‘𝐴)))
Theorem	ibladdlem 25789*	Lemma for ibladd 25790. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 = (𝐵 + 𝐶))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ)    &   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ)
Theorem	ibladd 25790*	Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿1)
Theorem	iblsub 25791*	Subtract two integrals over the same domain. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ 𝐿1)
Theorem	itgaddlem1 25792*	Lemma for itgadd 25794. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	itgaddlem2 25793*	Lemma for itgadd 25794. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	itgadd 25794*	Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	itgsub 25795*	Subtract two integrals over the same domain. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 − 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 − ∫𝐴𝐶 d𝑥))
Theorem	itgfsum 25796*	Take a finite sum of integrals over the same domain. (Contributed by Mario Carneiro, 24-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ∈ 𝐿1 ∧ ∫𝐴Σ𝑘 ∈ 𝐵 𝐶 d𝑥 = Σ𝑘 ∈ 𝐵 ∫𝐴𝐶 d𝑥))
Theorem	iblabslem 25797*	Lemma for iblabs 25798. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐺 ∈ MblFn ∧ (∫2‘𝐺) ∈ ℝ))
Theorem	iblabs 25798*	The absolute value of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1)
Theorem	iblabsr 25799*	A measurable function is integrable iff its absolute value is integrable. (See iblabs 25798 for the forward implication.) (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)
Theorem	iblmulc2 25800*	Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)