Theorem cnioobibld

Description: A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider F = ( x e. ( 0 (,) 1 ) |-> ( 1 / x ) ) . See cniccibl for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019)

	Ref	Expression
Hypotheses	cnioobibld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	cnioobibld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	cnioobibld.3	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
	cnioobibld.4	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
Assertion	cnioobibld	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )

Proof

Step	Hyp	Ref	Expression
1		cnioobibld.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		cnioobibld.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		cnioobibld.3	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) )
4		cnioobibld.4	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
5		ioombl	⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
6		cnmbf	⊢ ( ( ( 𝐴 (,) 𝐵 ) ∈ dom vol ∧ 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) ) → 𝐹 ∈ MblFn )
7	5 3 6	sylancr	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
8		cncff	⊢ ( 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –cn→ ℂ ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ )
9		fdm	⊢ ( 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℂ → dom 𝐹 = ( 𝐴 (,) 𝐵 ) )
10	3 8 9	3syl	⊢ ( 𝜑 → dom 𝐹 = ( 𝐴 (,) 𝐵 ) )
11	10	fveq2d	⊢ ( 𝜑 → ( vol ‘ dom 𝐹 ) = ( vol ‘ ( 𝐴 (,) 𝐵 ) ) )
12		ioovolcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )
13	1 2 12	syl2anc	⊢ ( 𝜑 → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )
14	11 13	eqeltrd	⊢ ( 𝜑 → ( vol ‘ dom 𝐹 ) ∈ ℝ )
15		bddibl	⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → 𝐹 ∈ 𝐿1 )
16	7 14 4 15	syl3anc	⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )