itgioo

Description: Equality of integrals on open and closed intervals. (Contributed by Mario Carneiro, 2-Sep-2014)

	Ref	Expression
Hypotheses	itgioo.1	$⊢ φ \to A \in ℝ$
	itgioo.2	$⊢ φ \to B \in ℝ$
	itgioo.3	$⊢ (φ \land x \in [A, B]) \to C \in ℂ$
Assertion	itgioo	$⊢ φ \to \int_{(A, B)} C d x = \int_{[A, B]} C d x$

Proof

Step	Hyp	Ref	Expression
1		itgioo.1	$⊢ φ \to A \in ℝ$
2		itgioo.2	$⊢ φ \to B \in ℝ$
3		itgioo.3	$⊢ (φ \land x \in [A, B]) \to C \in ℂ$
4		ioossicc	$⊢ (A, B) \subseteq [A, B]$
5	4	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
6		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
7	1 2 6	syl2anc	$⊢ φ \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		uncom	$⊢ \{A, B\} \cup (A, B) = (A, B) \cup \{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		prunioo	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to (A, B) \cup \{A, B\} = [A, B]$
23	19 20 21 22	syl3anc	$⊢ (φ \land A \leq B) \to (A, B) \cup \{A, B\} = [A, B]$
24	18 23	syl5req	$⊢ (φ \land A \leq B) \to [A, B] = \{A, B\} \cup (A, B)$
25	24	difeq1d	$⊢ (φ \land A \leq B) \to [A, B] ∖ (A, B) = (\{A, B\} \cup (A, B)) ∖ (A, B)$
26		difun2	$⊢ (\{A, B\} \cup (A, B)) ∖ (A, B) = \{A, B\} ∖ (A, B)$
27	25 26	eqtrdi	$⊢ (φ \land A \leq B) \to [A, B] ∖ (A, B) = \{A, B\} ∖ (A, B)$
28		difss	$⊢ \{A, B\} ∖ (A, B) \subseteq \{A, B\}$
29	27 28	eqsstrdi	$⊢ (φ \land A \leq B) \to [A, B] ∖ (A, B) \subseteq \{A, B\}$
30	17 29 2 1	ltlecasei	$⊢ φ \to [A, B] ∖ (A, B) \subseteq \{A, B\}$
31	1 2	prssd	$⊢ φ \to \{A, B\} \subseteq ℝ$
32		prfi	$⊢ \{A, B\} \in Fin$
33		ovolfi	$⊢ (\{A, B\} \in Fin \land \{A, B\} \subseteq ℝ) \to {vol}^{*} (\{A, B\}) = 0$
34	32 31 33	sylancr	$⊢ φ \to {vol}^{*} (\{A, B\}) = 0$
35		ovolssnul	$⊢ ([A, B] ∖ (A, B) \subseteq \{A, B\} \land \{A, B\} \subseteq ℝ \land {vol}^{} (\{A, B\}) = 0) \to {vol}^{} ([A, B] ∖ (A, B)) = 0$
36	30 31 34 35	syl3anc	$⊢ φ \to {vol}^{*} ([A, B] ∖ (A, B)) = 0$
37	5 7 36 3	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)$
38	37	simprd	$⊢ φ \to \int_{(A, B)} C d x = \int_{[A, B]} C d x$

Metamath Proof Explorer

Theorem itgioo

Proof