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	itgvallem 25701*	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 25702*	Lemma for itgposval 25712 and itgreval 25713. (Contributed by Mario Carneiro, 7-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 0)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) = 0)
Theorem	ibl0 25703	The zero function is integrable on any measurable set. (Unlike iblconst 25734, this does not require 𝐴 to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014.)
⊢ (𝐴 ∈ dom vol → (𝐴 × {0}) ∈ 𝐿1)
Theorem	iblcnlem1 25704*	Lemma for iblcnlem 25705. (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 25705*	Expand out the universal quantifier in isibl2 25683. (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 25706*	Expand out the sum in dfitg 25686. (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 25707*	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 25708*	Lemma for iblpos 25709. (Contributed by Mario Carneiro, 31-Jul-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ -𝐵), -𝐵, 0))) = 0)
Theorem	iblpos 25709*	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 25710*	Integrability of a real function. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ if(0 ≤ 𝐵, 𝐵, 0)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ if(0 ≤ -𝐵, -𝐵, 0)) ∈ 𝐿1)))
Theorem	itgrevallem1 25711*	Lemma for itgposval 25712 and itgreval 25713. (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 25712*	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 25713*	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 25714*	Real closure of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ∈ ℝ)
Theorem	iblcn 25715*	Integrability of a complex function. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔ ((𝑥 ∈ 𝐴 ↦ (ℜ‘𝐵)) ∈ 𝐿1 ∧ (𝑥 ∈ 𝐴 ↦ (ℑ‘𝐵)) ∈ 𝐿1)))
Theorem	itgcnval 25716*	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 25717*	Real part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (ℜ‘∫𝐴𝐵 d𝑥) = ∫𝐴(ℜ‘𝐵) d𝑥)
Theorem	itgim 25718*	Imaginary part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (ℑ‘∫𝐴𝐵 d𝑥) = ∫𝐴(ℑ‘𝐵) d𝑥)
Theorem	iblneg 25719*	The negative of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ -𝐵) ∈ 𝐿1)
Theorem	itgneg 25720*	Negation of an integral. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → -∫𝐴𝐵 d𝑥 = ∫𝐴-𝐵 d𝑥)
Theorem	iblss 25721*	A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)
Theorem	iblss2 25722*	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 25723*	Transfer an integral using ∫2 to an equivalent integral using ∫. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ 𝐴)    &   ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ 𝐴) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫ℝ𝐴 d𝑥 = (∫2‘(𝑥 ∈ ℝ ↦ 𝐴)))
Theorem	i1fibl 25724	A simple function is integrable. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝐹 ∈ dom ∫1 → 𝐹 ∈ 𝐿1)
Theorem	itgitg1 25725*	Transfer an integral using ∫1 to an equivalent integral using ∫. (Contributed by Mario Carneiro, 6-Aug-2014.)
⊢ (𝐹 ∈ dom ∫1 → ∫ℝ(𝐹‘𝑥) d𝑥 = (∫1‘𝐹))
Theorem	itgle 25726*	Monotonicity of an integral. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴𝐵 d𝑥 ≤ ∫𝐴𝐶 d𝑥)
Theorem	itgge0 25727*	The integral of a positive function is positive. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ ∫𝐴𝐵 d𝑥)
Theorem	itgss 25728*	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 25729*	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 25730*	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 25731*	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 25732*	Equality of integrals on open and closed intervals. (Contributed by Mario Carneiro, 2-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐵)𝐶 d𝑥 = ∫(𝐴[,]𝐵)𝐶 d𝑥)
Theorem	itgless 25733*	Expand the integral of a nonnegative function. (Contributed by Mario Carneiro, 31-Aug-2014.)
⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ dom vol)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 0 ≤ 𝐶)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴𝐶 d𝑥 ≤ ∫𝐵𝐶 d𝑥)
Theorem	iblconst 25734	A constant function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℂ) → (𝐴 × {𝐵}) ∈ 𝐿1)
Theorem	itgconst 25735*	Integral of a constant function. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ ((𝐴 ∈ dom vol ∧ (vol‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℂ) → ∫𝐴𝐵 d𝑥 = (𝐵 · (vol‘𝐴)))
Theorem	ibladdlem 25736*	Lemma for ibladd 25737. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 = (𝐵 + 𝐶))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)    &   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵), 𝐵, 0))) ∈ ℝ)    &   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶), 𝐶, 0))) ∈ ℝ)    ⇒   ⊢ (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐷), 𝐷, 0))) ∈ ℝ)
Theorem	ibladd 25737*	Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∈ 𝐿1)
Theorem	iblsub 25738*	Subtract two integrals over the same domain. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵 − 𝐶)) ∈ 𝐿1)
Theorem	itgaddlem1 25739*	Lemma for itgadd 25741. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐶)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	itgaddlem2 25740*	Lemma for itgadd 25741. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	itgadd 25741*	Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 + 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 + ∫𝐴𝐶 d𝑥))
Theorem	itgsub 25742*	Subtract two integrals over the same domain. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝐴(𝐵 − 𝐶) d𝑥 = (∫𝐴𝐵 d𝑥 − ∫𝐴𝐶 d𝑥))
Theorem	itgfsum 25743*	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 25744*	Lemma for iblabs 25745. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ 𝐺 = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, (abs‘(𝐹‘𝐵)), 0))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐺 ∈ MblFn ∧ (∫2‘𝐺) ∈ ℝ))
Theorem	iblabs 25745*	The absolute value of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1)
Theorem	iblabsr 25746*	A measurable function is integrable iff its absolute value is integrable. (See iblabs 25745 for the forward implication.) (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (abs‘𝐵)) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)
Theorem	iblmulc2 25747*	Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐶 · 𝐵)) ∈ 𝐿1)
Theorem	itgmulc2lem1 25748*	Lemma for itgmulc2 25750: positive real case. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgmulc2lem2 25749*	Lemma for itgmulc2 25750: real case. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgmulc2 25750*	Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (𝐶 · ∫𝐴𝐵 d𝑥) = ∫𝐴(𝐶 · 𝐵) d𝑥)
Theorem	itgabs 25751*	The triangle inequality for integrals. (Contributed by Mario Carneiro, 25-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → (abs‘∫𝐴𝐵 d𝑥) ≤ ∫𝐴(abs‘𝐵) d𝑥)
Theorem	itgsplit 25752*	The ∫ integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014.)
⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0)    &   ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫𝑈𝐶 d𝑥 = (∫𝐴𝐶 d𝑥 + ∫𝐵𝐶 d𝑥))
Theorem	itgspliticc 25753*	The ∫ integral splits on closed intervals with matching endpoints. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐶)) → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶) ↦ 𝐷) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫(𝐴[,]𝐶)𝐷 d𝑥 = (∫(𝐴[,]𝐵)𝐷 d𝑥 + ∫(𝐵[,]𝐶)𝐷 d𝑥))
Theorem	itgsplitioo 25754*	The ∫ integral splits on open intervals with matching endpoints. (Contributed by Mario Carneiro, 2-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐶)) → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐴(,)𝐵) ↦ 𝐷) ∈ 𝐿1)    &   ⊢ (𝜑 → (𝑥 ∈ (𝐵(,)𝐶) ↦ 𝐷) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ∫(𝐴(,)𝐶)𝐷 d𝑥 = (∫(𝐴(,)𝐵)𝐷 d𝑥 + ∫(𝐵(,)𝐶)𝐷 d𝑥))
Theorem	bddmulibl 25755*	A bounded function times an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ ((𝐹 ∈ MblFn ∧ 𝐺 ∈ 𝐿1 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → (𝐹 ∘f · 𝐺) ∈ 𝐿1)
Theorem	bddibl 25756*	A bounded function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1)
Theorem	cniccibl 25757	A continuous function on a closed bounded interval is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿1)
Theorem	bddiblnc 25758*	Choice-free proof of bddibl 25756. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.)
⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿1)
Theorem	cnicciblnc 25759	Choice-free proof of cniccibl 25757. (Contributed by Brendan Leahy, 2-Nov-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿1)
Theorem	itggt0 25760*	The integral of a strictly positive function is positive. (Contributed by Mario Carneiro, 30-Aug-2014.)
⊢ (𝜑 → 0 < (vol‘𝐴))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 0 < ∫𝐴𝐵 d𝑥)
Theorem	itgcn 25761*	Transfer itg2cn 25680 to the full Lebesgue integral. (Contributed by Mario Carneiro, 1-Sep-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑢 ∈ dom vol((𝑢 ⊆ 𝐴 ∧ (vol‘𝑢) < 𝑑) → ∫𝑢(abs‘𝐵) d𝑥 < 𝐶))
13.2.2.2  Lesbesgue directed integral
Syntax	cdit 25762	Extend class notation with the directed integral.
class ⨜[𝐴 → 𝐵]𝐶 d𝑥
Definition	df-ditg 25763	Define the directed integral, which is just a regular integral but with a sign change when the limits are interchanged. The 𝐴 and 𝐵 here are the lower and upper limits of the integral, usually written as a subscript and superscript next to the integral sign. We define the region of integration to be an open interval instead of closed so that we can use +∞, -∞ for limits and also integrate up to a singularity at an endpoint. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = if(𝐴 ≤ 𝐵, ∫(𝐴(,)𝐵)𝐶 d𝑥, -∫(𝐵(,)𝐴)𝐶 d𝑥)
Theorem	ditgeq1 25764*	Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝐴 = 𝐵 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = ⨜[𝐵 → 𝐶]𝐷 d𝑥)
Theorem	ditgeq2 25765*	Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝐴 = 𝐵 → ⨜[𝐶 → 𝐴]𝐷 d𝑥 = ⨜[𝐶 → 𝐵]𝐷 d𝑥)
Theorem	ditgeq3 25766*	Equality theorem for the directed integral. (The domain of the equality here is very rough; for more precise bounds one should decompose it with ditgpos 25772 first and use the equality theorems for df-itg 25539.) (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (∀𝑥 ∈ ℝ 𝐷 = 𝐸 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ⨜[𝐴 → 𝐵]𝐸 d𝑥)
Theorem	ditgeq3dv 25767*	Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝐷 = 𝐸)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐷 d𝑥 = ⨜[𝐴 → 𝐵]𝐸 d𝑥)
Theorem	ditgex 25768	A directed integral is a set. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 ∈ V
Theorem	ditg0 25769*	Value of the directed integral from a point to itself. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ ⨜[𝐴 → 𝐴]𝐵 d𝑥 = 0
Theorem	cbvditg 25770*	Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    &   ⊢ Ⅎ𝑦𝐶    &   ⊢ Ⅎ𝑥𝐷    ⇒   ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦
Theorem	cbvditgv 25771*	Change bound variable in a directed integral. (Contributed by Mario Carneiro, 7-Sep-2014.)
⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)    ⇒   ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦
Theorem	ditgpos 25772*	Value of the directed integral in the forward direction. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ∫(𝐴(,)𝐵)𝐶 d𝑥)
Theorem	ditgneg 25773*	Value of the directed integral in the backward direction. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝐴 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ⨜[𝐵 → 𝐴]𝐶 d𝑥 = -∫(𝐴(,)𝐵)𝐶 d𝑥)
Theorem	ditgcl 25774*	Closure of a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 ∈ ℂ)
Theorem	ditgswap 25775*	Reverse a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐶) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ⨜[𝐵 → 𝐴]𝐶 d𝑥 = -⨜[𝐴 → 𝐵]𝐶 d𝑥)
Theorem	ditgsplitlem 25776*	Lemma for ditgsplit 25777. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑋[,]𝑌))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ 𝐿1)    &   ⊢ ((𝜓 ∧ 𝜃) ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
Theorem	ditgsplit 25777*	This theorem is the raison d'être for the directed integral, because unlike itgspliticc 25753, there is no constraint on the ordering of the points 𝐴, 𝐵, 𝐶 in the domain. (Contributed by Mario Carneiro, 13-Aug-2014.)
⊢ (𝜑 → 𝑋 ∈ ℝ)    &   ⊢ (𝜑 → 𝑌 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐵 ∈ (𝑋[,]𝑌))    &   ⊢ (𝜑 → 𝐶 ∈ (𝑋[,]𝑌))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋(,)𝑌)) → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ (𝑋(,)𝑌) ↦ 𝐷) ∈ 𝐿1)    ⇒   ⊢ (𝜑 → ⨜[𝐴 → 𝐶]𝐷 d𝑥 = (⨜[𝐴 → 𝐵]𝐷 d𝑥 + ⨜[𝐵 → 𝐶]𝐷 d𝑥))
13.3  Derivatives
13.3.1  Real and complex differentiation
13.3.1.1  Derivatives of functions of one complex or real variable
Syntax	climc 25778	The limit operator.
class limℂ
Syntax	cdv 25779	The derivative operator.
class D
Syntax	cdvn 25780	The 𝑛-th derivative operator.
class D𝑛
Syntax	ccpn 25781	The set of 𝑛-times continuously differentiable functions.
class 𝓑C𝑛
Definition	df-limc 25782*	Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ limℂ = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∣ [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓‘𝑧))) ∈ (((𝑗 ↾t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
Definition	df-dv 25783*	Define the derivative operator. This acts on functions to produce a function that is defined where the original function is differentiable, with value the derivative of the function at these points. The set 𝑠 here is the ambient topological space under which we are evaluating the continuity of the difference quotient. Although the definition is valid for any subset of ℂ and is well-behaved when 𝑠 contains no isolated points, we will restrict our attention to the cases 𝑠 = ℝ or 𝑠 = ℂ for the majority of the development, these corresponding respectively to real and complex differentiation. (Contributed by Mario Carneiro, 7-Aug-2014.)
⊢ D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ ∪ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))
Definition	df-dvn 25784*	Define the 𝑛-th derivative operator on functions on the complex numbers. This just iterates the derivative operation according to the last argument. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
Definition	df-cpn 25785*	Define the set of 𝑛-times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014.)
⊢ 𝓑C𝑛 = (𝑠 ∈ 𝒫 ℂ ↦ (𝑥 ∈ ℕ0 ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ((𝑠 D𝑛 𝑓)‘𝑥) ∈ (dom 𝑓–cn→ℂ)}))
Theorem	reldv 25786	The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Mario Carneiro, 24-Dec-2016.)
⊢ Rel (𝑆 D 𝐹)
Theorem	limcvallem 25787*	Lemma for ellimc 25789. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵}))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))    ⇒   ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → (𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐵) → 𝐶 ∈ ℂ))
Theorem	limcfval 25788*	Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵}))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)} ∧ (𝐹 limℂ 𝐵) ⊆ ℂ))
Theorem	ellimc 25789*	Value of the limit predicate. 𝐶 is the limit of the function 𝐹 at 𝐵 if the function 𝐺, formed by adding 𝐵 to the domain of 𝐹 and setting it to 𝐶, is continuous at 𝐵. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵}))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ 𝐺 = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, (𝐹‘𝑧)))    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐵)))
Theorem	limcrcl 25790	Reverse closure for the limit operator. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝐶 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
Theorem	limccl 25791	Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝐹 limℂ 𝐵) ⊆ ℂ
Theorem	limcdif 25792	It suffices to consider functions which are not defined at 𝐵 to define the limit of a function. In particular, the value of the original function 𝐹 at 𝐵 does not affect the limit of 𝐹. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    ⇒   ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝐹 ↾ (𝐴 ∖ {𝐵})) limℂ 𝐵))
Theorem	ellimc2 25793*	Write the definition of a limit directly in terms of open sets of the topology on the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑢 ∈ 𝐾 (𝐶 ∈ 𝑢 → ∃𝑤 ∈ 𝐾 (𝐵 ∈ 𝑤 ∧ (𝐹 “ (𝑤 ∩ (𝐴 ∖ {𝐵}))) ⊆ 𝑢)))))
Theorem	limcnlp 25794	If 𝐵 is not a limit point of the domain of the function 𝐹, then every point is a limit of 𝐹 at 𝐵. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ ((limPt‘𝐾)‘𝐴))    ⇒   ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ℂ)
Theorem	ellimc3 25795*	Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ 𝐴 ((𝑧 ≠ 𝐵 ∧ (abs‘(𝑧 − 𝐵)) < 𝑦) → (abs‘((𝐹‘𝑧) − 𝐶)) < 𝑥))))
Theorem	limcflflem 25796	Lemma for limcflf 25797. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ 𝐶 = (𝐴 ∖ {𝐵})    &   ⊢ 𝐿 = (((nei‘𝐾)‘{𝐵}) ↾t 𝐶)    ⇒   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝐶))
Theorem	limcflf 25797	The limit operator can be expressed as a filter limit, from the filter of neighborhoods of 𝐵 restricted to 𝐴 ∖ {𝐵}, to the topology of the complex numbers. (If 𝐵 is not a limit point of 𝐴, then it is still formally a filter limit, but the neighborhood filter is not a proper filter in this case.) (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    &   ⊢ 𝐶 = (𝐴 ∖ {𝐵})    &   ⊢ 𝐿 = (((nei‘𝐾)‘{𝐵}) ↾t 𝐶)    ⇒   ⊢ (𝜑 → (𝐹 limℂ 𝐵) = ((𝐾 fLimf 𝐿)‘(𝐹 ↾ 𝐶)))
Theorem	limcmo 25798*	If 𝐵 is a limit point of the domain of the function 𝐹, then there is at most one limit value of 𝐹 at 𝐵. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → 𝐹:𝐴⟶ℂ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ((limPt‘𝐾)‘𝐴))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐹 limℂ 𝐵))
Theorem	limcmpt 25799*	Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝐷 ∈ ℂ)    &   ⊢ 𝐽 = (𝐾 ↾t (𝐴 ∪ {𝐵}))    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ((𝑧 ∈ 𝐴 ↦ 𝐷) limℂ 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝐶, 𝐷)) ∈ ((𝐽 CnP 𝐾)‘𝐵)))
Theorem	limcmpt2 25800*	Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝐵)) → 𝐷 ∈ ℂ)    &   ⊢ 𝐽 = (𝐾 ↾t 𝐴)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → (𝐶 ∈ ((𝑧 ∈ (𝐴 ∖ {𝐵}) ↦ 𝐷) limℂ 𝐵) ↔ (𝑧 ∈ 𝐴 ↦ if(𝑧 = 𝐵, 𝐶, 𝐷)) ∈ ((𝐽 CnP 𝐾)‘𝐵)))