P. 260 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25901-26000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	itg1le 25901	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 25902*	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 25903*	Lemma for mbfi1fseq 25909. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    ⇒   ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
Theorem	mbfi1fseqlem2 25904*	Lemma for mbfi1fseq 25909. (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 25905*	Lemma for mbfi1fseq 25909. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
Theorem	mbfi1fseqlem4 25906*	Lemma for mbfi1fseq 25909. 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 25907*	Lemma for mbfi1fseq 25909. 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 25908*	Lemma for mbfi1fseq 25909. 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 25909*	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 25910*	Lemma for mbfi1flim 25911. (Contributed by Mario Carneiro, 5-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    ⇒   ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
Theorem	mbfi1flim 25911*	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 25912*	Lemma for mbfmul 25914. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ (𝜑 → 𝑄:ℕ⟶dom ∫1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn)
Theorem	mbfmullem 25913	Lemma for mbfmul 25914. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn)
Theorem	mbfmul 25914	The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝐹 ∘f · 𝐺) ∈ MblFn)
Theorem	itg2lcl 25915*	The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ 𝐿 ⊆ ℝ*
Theorem	itg2val 25916*	Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) = sup(𝐿, ℝ*, < ))
Theorem	itg2l 25917*	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 25918*	Sufficient condition for elementhood in the set 𝐿. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹) → (∫1‘𝐺) ∈ 𝐿)
Theorem	xrge0f 25919	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 25920	The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*)
Theorem	itg2ub 25921	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 25922*	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 25923	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 25924	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 25925	The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (∫2‘(ℝ × {0})) = 0
Theorem	itg2lecl 25926	If an ∫2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐴 ∈ ℝ ∧ (∫2‘𝐹) ≤ 𝐴) → (∫2‘𝐹) ∈ ℝ)
Theorem	itg2le 25927	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 25928*	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 25929*	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 25930*	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 25943, 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 25931*	Approximate version of itg2ub 25921. If 𝐹 approximately dominates 𝐺, then ∫1𝐺 ≤ ∫2𝐹. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐺‘𝑥) ≤ (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → (∫1‘𝐺) ≤ (∫2‘𝐹))
Theorem	itg2lea 25932*	Approximate version of itg2le 25927. If 𝐹 ≤ 𝐺 for almost all 𝑥, then ∫2𝐹 ≤ ∫2𝐺. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) ≤ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (∫2‘𝐹) ≤ (∫2‘𝐺))
Theorem	itg2eqa 25933*	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 25934	Lemma for itg2mulc 25935. (Contributed by Mario Carneiro, 8-Jul-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (∫2‘((ℝ × {𝐴}) ∘f · 𝐹)) ≤ (𝐴 · (∫2‘𝐹)))
Theorem	itg2mulc 25935	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 25936*	Lemma for itg2split 25937. (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 25937*	The ∫2 integral splits under an almost disjoint union. The proof avoids the use of itg2add 25947, 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 25938*	Lemma for itg2mono 25941. 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 25941. 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 25902. 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 25939*	Lemma for itg2mono 25941. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)    &   ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )    &   ⊢ (𝜑 → 𝑃 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝑃 ∘r ≤ 𝐺)    &   ⊢ (𝜑 → ¬ (∫1‘𝑃) ≤ 𝑆)    ⇒   ⊢ (𝜑 → 𝑆 ∈ ℝ)
Theorem	itg2monolem3 25940*	Lemma for itg2mono 25941. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘r ≤ (𝐹‘(𝑛 + 1)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)    &   ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )    &   ⊢ (𝜑 → 𝑃 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝑃 ∘r ≤ 𝐺)    &   ⊢ (𝜑 → ¬ (∫1‘𝑃) ≤ 𝑆)    ⇒   ⊢ (𝜑 → (∫1‘𝑃) ≤ 𝑆)
Theorem	itg2mono 25941*	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 25942*	Subject to the conditions coming from mbfi1fseq 25909, 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 25943*	Subject to the conditions coming from mbfi1fseq 25909, 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 25944*	In an extension to the results of itg2i1fseq 25943, 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 25945*	Special case of itg2i1fseq2 25944: 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 25946*	Lemma for itg2add 25947. (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 25947	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 25948*	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 25949*	Lemma for itgcn 26033. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) = (∫2‘𝐹))
Theorem	itg2cnlem2 25950*	Lemma for itgcn 26033. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
Theorem	itg2cn 25951*	A sort of absolute continuity of the Lebesgue integral (this is the core of ftc1a 26225 which is about actual absolute continuity). (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
Theorem	ibllem 25952	Conditioned equality theorem for the if statement. (Contributed by Mario Carneiro, 31-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
Theorem	isibl 25953*	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 25954*	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 25955	An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.)
⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
Theorem	iblitg 25956*	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 25957*	Evaluate the class substitution in df-itg 25811. (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 25958	An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ∫𝐴𝐵 d𝑥 ∈ V
Theorem	itgeq1f 25959	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.) Avoid axioms. (Revised by GG, 1-Sep-2025.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)
Theorem	itgeq1fOLD 25960	Obsolete version of itgeq1f 25959 as of 1-Sep-2025. (Contributed by Mario Carneiro, 28-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)
Theorem	itgeq1 25961*	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝐴 = 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)
Theorem	nfitg1 25962	Bound-variable hypothesis builder for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ Ⅎ𝑥∫𝐴𝐵 d𝑥
Theorem	nfitg 25963*	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 25964*	Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦
Theorem	cbvitgv 25965*	Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦
Theorem	itgeq2 25966	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥)
Theorem	itgresr 25967	The domain of an integral only matters in its intersection with ℝ. (Contributed by Mario Carneiro, 29-Jun-2014.)
⊢ ∫𝐴𝐵 d𝑥 = ∫(𝐴 ∩ ℝ)𝐵 d𝑥
Theorem	itg0 25968	The integral of anything on the empty set is zero. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ∫∅𝐴 d𝑥 = 0
Theorem	itgz 25969	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 25970*	Equality theorem for an integral. (Contributed by Mario Carneiro, 7-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥)
Theorem	itgmpt 25971*	Change bound variable in an integral. (Contributed by Mario Carneiro, 29-Jun-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) d𝑦)
Theorem	itgcl 25972*	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 25973*	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 25974*	Lemma for itgposval 25984 and itgreval 25985. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 0)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) = 0)
Theorem	ibl0 25975	The zero function is integrable on any measurable set. (Unlike iblconst 26006, this does not require 𝐴 to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (𝐴 ∈ dom vol → (𝐴 × {0}) ∈ 𝐿1)
Theorem	iblcnlem1 25976*	Lemma for iblcnlem 25977. (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 25977*	Expand out the universal quantifier in isibl2 25954. (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 25978*	Expand out the sum in dfitg 25957. (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 25979*	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 25980*	Lemma for iblpos 25981. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) = 0)
Theorem	iblpos 25981*	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 25982*	Integrability of a real function. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿1)))
Theorem	itgrevallem1 25983*	Lemma for itgposval 25984 and itgreval 25985. (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 25984*	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 25985*	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 25986*	Real closure of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℝ)
Theorem	iblcn 25987*	Integrability of a complex function. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)))
Theorem	itgcnval 25988*	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 25989*	Real part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (ℜ‘∫𝐴𝐵 d𝑥) = ∫𝐴(ℜ‘𝐵) d𝑥)
Theorem	itgim 25990*	Imaginary part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (ℑ‘∫𝐴𝐵 d𝑥) = ∫𝐴(ℑ‘𝐵) d𝑥)
Theorem	iblneg 25991*	The negative of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ 𝐿1)
Theorem	itgneg 25992*	Negation of an integral. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → -∫𝐴𝐵 d𝑥 = ∫𝐴-𝐵 d𝑥)
Theorem	iblss 25993*	A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)
Theorem	iblss2 25994*	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 25995*	Transfer an integral using ∫2 to an equivalent integral using ∫. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝐴)    &   ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝐴) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫ℝ𝐴 d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ 𝐴)))
Theorem	i1fibl 25996	A simple function is integrable. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝐹 ∈ dom ∫1 → 𝐹 ∈ 𝐿1)
Theorem	itgitg1 25997*	Transfer an integral using ∫1 to an equivalent integral using ∫. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝐹 ∈ dom ∫1 → ∫ℝ(𝐹‘𝑥) d𝑥 = (∫1‘𝐹))
Theorem	itgle 25998*	Monotonicity of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ≤ ∫𝐴𝐶 d𝑥)
Theorem	itgge0 25999*	The integral of a positive function is positive. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ ∫𝐴𝐵 d𝑥)
Theorem	itgss 26000*	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𝑥)