ibliooicc

Description: If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	ibliooicc.1	$⊢ φ \to A \in ℝ$
	ibliooicc.2	$⊢ φ \to B \in ℝ$
	ibliooicc.3	$⊢ φ \to (x \in (A, B) ⟼ C) \in 𝐿^{1}$
	ibliooicc.4	$⊢ (φ \land x \in [A, B]) \to C \in ℂ$
Assertion	ibliooicc	$⊢ φ \to (x \in [A, B] ⟼ C) \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		ibliooicc.1	$⊢ φ \to A \in ℝ$
2		ibliooicc.2	$⊢ φ \to B \in ℝ$
3		ibliooicc.3	$⊢ φ \to (x \in (A, B) ⟼ C) \in 𝐿^{1}$
4		ibliooicc.4	$⊢ (φ \land x \in [A, B]) \to C \in ℂ$
5		ioossicc	$⊢ (A, B) \subseteq [A, B]$
6	5	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
7	1 2	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
8	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
9	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
10		icc0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$
11	8 9 10	syl2anc	$⊢ φ \to ([A, B] = \emptyset \leftrightarrow B < A)$
12	11	biimpar	$⊢ (φ \land B < A) \to [A, B] = \emptyset$
13	12	difeq1d	$⊢ (φ \land B < A) \to [A, B] ∖ (A, B) = \emptyset ∖ (A, B)$
14		0dif	$⊢ \emptyset ∖ (A, B) = \emptyset$
15		0ss	$⊢ \emptyset \subseteq \{A, B\}$
16	14 15	eqsstri	$⊢ \emptyset ∖ (A, B) \subseteq \{A, B\}$
17	13 16	eqsstrdi	$⊢ (φ \land B < A) \to [A, B] ∖ (A, B) \subseteq \{A, B\}$
18		ssid	$⊢ [A, B] ∖ (A, B) \subseteq [A, B] ∖ (A, B)$
19	8	adantr	$⊢ (φ \land A \leq B) \to A \in ℝ^{*}$
20	9	adantr	$⊢ (φ \land A \leq B) \to B \in ℝ^{*}$
21		simpr	$⊢ (φ \land A \leq B) \to A \leq B$
22		iccdifioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to [A, B] ∖ (A, B) = \{A, B\}$
23	19 20 21 22	syl3anc	$⊢ (φ \land A \leq B) \to [A, B] ∖ (A, B) = \{A, B\}$
24	18 23	sseqtrid	$⊢ (φ \land A \leq B) \to [A, B] ∖ (A, B) \subseteq \{A, B\}$
25	17 24 2 1	ltlecasei	$⊢ φ \to [A, B] ∖ (A, B) \subseteq \{A, B\}$
26		prssi	$⊢ (A \in ℝ \land B \in ℝ) \to \{A, B\} \subseteq ℝ$
27	1 2 26	syl2anc	$⊢ φ \to \{A, B\} \subseteq ℝ$
28		prfi	$⊢ \{A, B\} \in Fin$
29		ovolfi	$⊢ (\{A, B\} \in Fin \land \{A, B\} \subseteq ℝ) \to {vol}^{*} (\{A, B\}) = 0$
30	28 27 29	sylancr	$⊢ φ \to {vol}^{*} (\{A, B\}) = 0$
31		ovolssnul	$⊢ ([A, B] ∖ (A, B) \subseteq \{A, B\} \land \{A, B\} \subseteq ℝ \land {vol}^{} (\{A, B\}) = 0) \to {vol}^{} ([A, B] ∖ (A, B)) = 0$
32	25 27 30 31	syl3anc	$⊢ φ \to {vol}^{*} ([A, B] ∖ (A, B)) = 0$
33	6 7 32 4	itgss3	$⊢ φ \to (((x \in (A, B) ⟼ C) \in 𝐿^{1} \leftrightarrow (x \in [A, B] ⟼ C) \in 𝐿^{1}) \land \int_{(A, B)} C d x = \int_{[A, B]} C d x)$
34	33	simpld	$⊢ φ \to ((x \in (A, B) ⟼ C) \in 𝐿^{1} \leftrightarrow (x \in [A, B] ⟼ C) \in 𝐿^{1})$
35	3 34	mpbid	$⊢ φ \to (x \in [A, B] ⟼ C) \in 𝐿^{1}$

Metamath Proof Explorer

Theorem ibliooicc

Proof