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	$⊢ φ \to A \in ℝ$
	cnioobibld.2	$⊢ φ \to B \in ℝ$
	cnioobibld.3	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
	cnioobibld.4	$⊢ φ \to \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x$
Assertion	cnioobibld	$⊢ φ \to F \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		cnioobibld.1	$⊢ φ \to A \in ℝ$
2		cnioobibld.2	$⊢ φ \to B \in ℝ$
3		cnioobibld.3	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
4		cnioobibld.4	$⊢ φ \to \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x$
5		ioombl	$⊢ (A, B) \in dom vol$
6		cnmbf	$⊢ ((A, B) \in dom vol \land F : (A, B) \underset{cn}{⟶} ℂ) \to F \in MblFn$
7	5 3 6	sylancr	$⊢ φ \to F \in MblFn$
8		cncff	$⊢ F : (A, B) \underset{cn}{⟶} ℂ \to F : (A, B) ⟶ ℂ$
9		fdm	$⊢ F : (A, B) ⟶ ℂ \to dom F = (A, B)$
10	3 8 9	3syl	$⊢ φ \to dom F = (A, B)$
11	10	fveq2d	$⊢ φ \to vol (dom F) = vol ((A, B))$
12		ioovolcl	$⊢ (A \in ℝ \land B \in ℝ) \to vol ((A, B)) \in ℝ$
13	1 2 12	syl2anc	$⊢ φ \to vol ((A, B)) \in ℝ$
14	11 13	eqeltrd	$⊢ φ \to vol (dom F) \in ℝ$
15		bddibl	$⊢ (F \in MblFn \land vol (dom F) \in ℝ \land \exists x \in ℝ \forall y \in dom F \|F (y)\| \leq x) \to F \in 𝐿^{1}$
16	7 14 4 15	syl3anc	$⊢ φ \to F \in 𝐿^{1}$

Metamath Proof Explorer

Theorem cnioobibld

Proof