P. 240 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23901-24000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	itg1addlem2 23901*	Lemma for itg1add 23905. 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 23903 and itg1addlem5 23904. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))))    ⇒   ⊢ (𝜑 → 𝐼:(ℝ × ℝ)⟶ℝ)
Theorem	itg1addlem3 23902*	Lemma for itg1add 23905. (Contributed by Mario Carneiro, 26-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))))    ⇒   ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ¬ (𝐴 = 0 ∧ 𝐵 = 0)) → (𝐴𝐼𝐵) = (vol‘((◡𝐹 “ {𝐴}) ∩ (◡𝐺 “ {𝐵}))))
Theorem	itg1addlem4 23903*	Lemma for itg1add . (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))))    &   ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))    ⇒   ⊢ (𝜑 → (∫1‘(𝐹 ∘𝑓 + 𝐺)) = Σ𝑦 ∈ ran 𝐹Σ𝑧 ∈ ran 𝐺((𝑦 + 𝑧) · (𝑦𝐼𝑧)))
Theorem	itg1addlem5 23904*	Lemma for itg1add . (Contributed by Mario Carneiro, 27-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))))    &   ⊢ 𝑃 = ( + ↾ (ran 𝐹 × ran 𝐺))    ⇒   ⊢ (𝜑 → (∫1‘(𝐹 ∘𝑓 + 𝐺)) = ((∫1‘𝐹) + (∫1‘𝐺)))
Theorem	itg1add 23905	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‘(𝐹 ∘𝑓 + 𝐺)) = ((∫1‘𝐹) + (∫1‘𝐺)))
Theorem	i1fmulclem 23906	Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘𝑓 · 𝐹) “ {𝐵}) = (◡𝐹 “ {(𝐵 / 𝐴)}))
Theorem	i1fmulc 23907	A nonnegative constant times a simple function gives another simple function. (Contributed by Mario Carneiro, 25-Jun-2014.)
⊢ (𝜑 → 𝐹 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((ℝ × {𝐴}) ∘𝑓 · 𝐹) ∈ dom ∫1)
Theorem	itg1mulc 23908	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‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫1‘𝐹)))
Theorem	i1fres 23909*	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 23910*	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 23911*	Deduction form of i1fposd 23911. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝐴) ∈ dom ∫1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(0 ≤ 𝐴, 𝐴, 0)) ∈ dom ∫1)
Theorem	i1fsub 23912	The difference of two simple functions is a simple function. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (𝐹 ∘𝑓 − 𝐺) ∈ dom ∫1)
Theorem	itg1sub 23913	The integral of a difference of two simple functions. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1) → (∫1‘(𝐹 ∘𝑓 − 𝐺)) = ((∫1‘𝐹) − (∫1‘𝐺)))
Theorem	itg10a 23914*	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 23915*	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 23916*	Approximate version of itg1le 23917. 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 23917	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 ∧ 𝐹 ∘𝑟 ≤ 𝐺) → (∫1‘𝐹) ≤ (∫1‘𝐺))
Theorem	itg1climres 23918*	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 23919*	Lemma for mbfi1fseq 23925. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    ⇒   ⊢ (𝜑 → 𝐽:(ℕ × ℝ)⟶(0[,)+∞))
Theorem	mbfi1fseqlem2 23920*	Lemma for mbfi1fseq 23925. (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 23921*	Lemma for mbfi1fseq 23925. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (𝐺‘𝐴):ℝ⟶ran (𝑚 ∈ (0...(𝐴 · (2↑𝐴))) ↦ (𝑚 / (2↑𝐴))))
Theorem	mbfi1fseqlem4 23922*	Lemma for mbfi1fseq 23925. 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 23923*	Lemma for mbfi1fseq 23925. Verify that 𝐺 describes an increasing sequence of positive functions. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0)))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ) → (0𝑝 ∘𝑟 ≤ (𝐺‘𝐴) ∧ (𝐺‘𝐴) ∘𝑟 ≤ (𝐺‘(𝐴 + 1))))
Theorem	mbfi1fseqlem6 23924*	Lemma for mbfi1fseq 23925. 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𝑝 ∘𝑟 ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘𝑟 ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
Theorem	mbfi1fseq 23925*	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𝑝 ∘𝑟 ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘𝑟 ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
Theorem	mbfi1flimlem 23926*	Lemma for mbfi1flim 23927. (Contributed by Mario Carneiro, 5-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)    ⇒   ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))
Theorem	mbfi1flim 23927*	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 23928*	Lemma for mbfmul 23930. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ (𝜑 → 𝑄:ℕ⟶dom ∫1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ MblFn)
Theorem	mbfmullem 23929	Lemma for mbfmul 23930. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ)    &   ⊢ (𝜑 → 𝐺:𝐴⟶ℝ)    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ MblFn)
Theorem	mbfmul 23930	The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    ⇒   ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ MblFn)
Theorem	itg2lcl 23931*	The set of lower sums is a set of extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ 𝐿 ⊆ ℝ*
Theorem	itg2val 23932*	Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) = sup(𝐿, ℝ*, < ))
Theorem	itg2l 23933*	Elementhood in the set 𝐿 of lower sums of the integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ (𝐴 ∈ 𝐿 ↔ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝐹 ∧ 𝐴 = (∫1‘𝑔)))
Theorem	itg2lr 23934*	Sufficient condition for elementhood in the set 𝐿. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ 𝐿 = {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝐹 ∧ 𝑥 = (∫1‘𝑔))}    ⇒   ⊢ ((𝐺 ∈ dom ∫1 ∧ 𝐺 ∘𝑟 ≤ 𝐹) → (∫1‘𝐺) ∈ 𝐿)
Theorem	xrge0f 23935	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𝑝 ∘𝑟 ≤ 𝐹) → 𝐹:ℝ⟶(0[,]+∞))
Theorem	itg2cl 23936	The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝐹:ℝ⟶(0[,]+∞) → (∫2‘𝐹) ∈ ℝ*)
Theorem	itg2ub 23937	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 ∧ 𝐺 ∘𝑟 ≤ 𝐹) → (∫1‘𝐺) ≤ (∫2‘𝐹))
Theorem	itg2leub 23938*	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(𝑔 ∘𝑟 ≤ 𝐹 → (∫1‘𝑔) ≤ 𝐴)))
Theorem	itg2ge0 23939	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 23940	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𝑝 ∘𝑟 ≤ 𝐹) → (∫2‘𝐹) = (∫1‘𝐹))
Theorem	itg20 23941	The integral of the zero function. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (∫2‘(ℝ × {0})) = 0
Theorem	itg2lecl 23942	If an ∫2 integral is bounded above, then it is real. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐴 ∈ ℝ ∧ (∫2‘𝐹) ≤ 𝐴) → (∫2‘𝐹) ∈ ℝ)
Theorem	itg2le 23943	If one function dominates another, then the integral of the larger is also larger. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ((𝐹:ℝ⟶(0[,]+∞) ∧ 𝐺:ℝ⟶(0[,]+∞) ∧ 𝐹 ∘𝑟 ≤ 𝐺) → (∫2‘𝐹) ≤ (∫2‘𝐺))
Theorem	itg2const 23944*	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 23945*	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 23946*	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 23959, but unlike that theorem this one doesn't require 𝐹 to be measurable.) (Contributed by Mario Carneiro, 14-Aug-2014.)
⊢ (𝐹:ℝ⟶(0[,]+∞) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (𝑔‘𝑛) ∘𝑟 ≤ 𝐹 ∧ (∫2‘𝐹) = sup(ran (𝑛 ∈ ℕ ↦ (∫1‘(𝑔‘𝑛))), ℝ*, < )))
Theorem	itg2uba 23947*	Approximate version of itg2ub 23937. If 𝐹 approximately dominates 𝐺, then ∫1𝐺 ≤ ∫2𝐹. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐺‘𝑥) ≤ (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → (∫1‘𝐺) ≤ (∫2‘𝐹))
Theorem	itg2lea 23948*	Approximate version of itg2le 23943. If 𝐹 ≤ 𝐺 for almost all 𝑥, then ∫2𝐹 ≤ ∫2𝐺. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,]+∞))    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → (vol*‘𝐴) = 0)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐴)) → (𝐹‘𝑥) ≤ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (∫2‘𝐹) ≤ (∫2‘𝐺))
Theorem	itg2eqa 23949*	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 23950	Lemma for itg2mulc 23951. (Contributed by Mario Carneiro, 8-Jul-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (∫2‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) ≤ (𝐴 · (∫2‘𝐹)))
Theorem	itg2mulc 23951	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‘((ℝ × {𝐴}) ∘𝑓 · 𝐹)) = (𝐴 · (∫2‘𝐹)))
Theorem	itg2splitlem 23952*	Lemma for itg2split 23953. (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 23953*	The ∫2 integral splits under an almost disjoint union. (The proof avoids the use of itg2add 23963 which requires CC.) (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 23954*	Lemma for itg2mono 23957. 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 23957. 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 23918. 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[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)    &   ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )    &   ⊢ (𝜑 → 𝑇 ∈ (0(,)1))    &   ⊢ (𝜑 → 𝐻 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝐻 ∘𝑟 ≤ 𝐺)    &   ⊢ (𝜑 → 𝑆 ∈ ℝ)    &   ⊢ 𝐴 = (𝑛 ∈ ℕ ↦ {𝑥 ∈ ℝ ∣ (𝑇 · (𝐻‘𝑥)) ≤ ((𝐹‘𝑛)‘𝑥)})    ⇒   ⊢ (𝜑 → (𝑇 · (∫1‘𝐻)) ≤ 𝑆)
Theorem	itg2monolem2 23955*	Lemma for itg2mono 23957. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)    &   ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )    &   ⊢ (𝜑 → 𝑃 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝑃 ∘𝑟 ≤ 𝐺)    &   ⊢ (𝜑 → ¬ (∫1‘𝑃) ≤ 𝑆)    ⇒   ⊢ (𝜑 → 𝑆 ∈ ℝ)
Theorem	itg2monolem3 23956*	Lemma for itg2mono 23957. (Contributed by Mario Carneiro, 16-Aug-2014.)
⊢ 𝐺 = (𝑥 ∈ ℝ ↦ sup(ran (𝑛 ∈ ℕ ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ MblFn)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛):ℝ⟶(0[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)    &   ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )    &   ⊢ (𝜑 → 𝑃 ∈ dom ∫1)    &   ⊢ (𝜑 → 𝑃 ∘𝑟 ≤ 𝐺)    &   ⊢ (𝜑 → ¬ (∫1‘𝑃) ≤ 𝑆)    ⇒   ⊢ (𝜑 → (∫1‘𝑃) ≤ 𝑆)
Theorem	itg2mono 23957*	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[,)+∞))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∘𝑟 ≤ (𝐹‘(𝑛 + 1)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℕ ((𝐹‘𝑛)‘𝑥) ≤ 𝑦)    &   ⊢ 𝑆 = sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝐹‘𝑛))), ℝ*, < )    ⇒   ⊢ (𝜑 → (∫2‘𝐺) = 𝑆)
Theorem	itg2i1fseqle 23958*	Subject to the conditions coming from mbfi1fseq 23925, the sequence of simple functions are all less than the target function 𝐹. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑃‘𝑀) ∘𝑟 ≤ 𝐹)
Theorem	itg2i1fseq 23959*	Subject to the conditions coming from mbfi1fseq 23925, 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𝑝 ∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (∫1‘(𝑃‘𝑚)))    ⇒   ⊢ (𝜑 → (∫2‘𝐹) = sup(ran 𝑆, ℝ*, < ))
Theorem	itg2i1fseq2 23960*	In an extension to the results of itg2i1fseq 23959, 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𝑝 ∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (∫1‘(𝑃‘𝑚)))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (∫1‘(𝑃‘𝑘)) ≤ 𝑀)    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (∫2‘𝐹))
Theorem	itg2i1fseq3 23961*	Special case of itg2i1fseq2 23960: 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𝑝 ∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ 𝑆 = (𝑚 ∈ ℕ ↦ (∫1‘(𝑃‘𝑚)))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝑆 ⇝ (∫2‘𝐹))
Theorem	itg2addlem 23962*	Lemma for itg2add 23963. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐺 ∈ MblFn)    &   ⊢ (𝜑 → 𝐺:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → (∫2‘𝐺) ∈ ℝ)    &   ⊢ (𝜑 → 𝑃:ℕ⟶dom ∫1)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))    &   ⊢ (𝜑 → 𝑄:ℕ⟶dom ∫1)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝 ∘𝑟 ≤ (𝑄‘𝑛) ∧ (𝑄‘𝑛) ∘𝑟 ≤ (𝑄‘(𝑛 + 1))))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑄‘𝑛)‘𝑥)) ⇝ (𝐺‘𝑥))    ⇒   ⊢ (𝜑 → (∫2‘(𝐹 ∘𝑓 + 𝐺)) = ((∫2‘𝐹) + (∫2‘𝐺)))
Theorem	itg2add 23963	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‘(𝐹 ∘𝑓 + 𝐺)) = ((∫2‘𝐹) + (∫2‘𝐺)))
Theorem	itg2gt0 23964*	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 23965*	Lemma for itgcn 24046. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    ⇒   ⊢ (𝜑 → sup(ran (𝑛 ∈ ℕ ↦ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑛, (𝐹‘𝑥), 0)))), ℝ*, < ) = (∫2‘𝐹))
Theorem	itg2cnlem2 23966*	Lemma for itgcn 24046. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (∫2‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫2‘𝐹) − (𝐶 / 2)))    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
Theorem	itg2cn 23967*	A sort of absolute continuity of the Lebesgue integral (this is the core of ftc1a 24237 which is about actual absolute continuity). (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝐹 ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘𝐹) ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫2‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
Theorem	ibllem 23968	Conditioned equality theorem for the if statement. (Contributed by Mario Carneiro, 31-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))
Theorem	isibl 23969*	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 23970*	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 23971	An integrable function is measurable. (Contributed by Mario Carneiro, 7-Jul-2014.)
⊢ (𝐹 ∈ 𝐿1 → 𝐹 ∈ MblFn)
Theorem	iblitg 23972*	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 23973*	Evaluate the class substitution in df-itg 23827. (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 23974	An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ ∫𝐴𝐵 d𝑥 ∈ V
Theorem	itgeq1f 23975	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ (𝐴 = 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)
Theorem	itgeq1 23976*	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝐴 = 𝐵 → ∫𝐴𝐶 d𝑥 = ∫𝐵𝐶 d𝑥)
Theorem	nfitg1 23977	Bound-variable hypothesis builder for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ Ⅎ𝑥∫𝐴𝐵 d𝑥
Theorem	nfitg 23978*	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 23979*	Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    &   ⊢ Ⅎ𝑦𝐵    &   ⊢ Ⅎ𝑥𝐶    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦
Theorem	cbvitgv 23980*	Change bound variable in an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)    ⇒   ⊢ ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑦
Theorem	itgeq2 23981	Equality theorem for an integral. (Contributed by Mario Carneiro, 28-Jun-2014.)
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥)
Theorem	itgresr 23982	The domain of an integral only matters in its intersection with ℝ. (Contributed by Mario Carneiro, 29-Jun-2014.)
⊢ ∫𝐴𝐵 d𝑥 = ∫(𝐴 ∩ ℝ)𝐵 d𝑥
Theorem	itg0 23983	The integral of anything on the empty set is zero. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ∫∅𝐴 d𝑥 = 0
Theorem	itgz 23984	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 23985*	Equality theorem for an integral. (Contributed by Mario Carneiro, 7-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴𝐶 d𝑥)
Theorem	itgmpt 23986*	Change bound variable in an integral. (Contributed by Mario Carneiro, 29-Jun-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 = ∫𝐴((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑦) d𝑦)
Theorem	itgcl 23987*	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 23988*	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 23989*	Lemma for itgposval 23999 and itgreval 24000. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 0)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) = 0)
Theorem	ibl0 23990	The zero function is integrable on any measurable set. (Unlike iblconst 24021, this does not require 𝐴 to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (𝐴 ∈ dom vol → (𝐴 × {0}) ∈ 𝐿1)
Theorem	iblcnlem1 23991*	Lemma for iblcnlem 23992. (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 23992*	Expand out the forall in isibl2 23970. (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 23993*	Expand out the sum in dfitg 23973. (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 23994*	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 23995*	Lemma for iblpos 23996. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) = 0)
Theorem	iblpos 23996*	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 23997*	Integrability of a real function. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿1)))
Theorem	itgrevallem1 23998*	Lemma for itgposval 23999 and itgreval 24000. (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 23999*	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 24000*	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𝑥))