itgspliticc

Description: The S. integral splits on closed intervals with matching endpoints. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Hypotheses	itgspliticc.1	$⊢ φ \to A \in ℝ$
	itgspliticc.2	$⊢ φ \to C \in ℝ$
	itgspliticc.3	$⊢ φ \to B \in [A, C]$
	itgspliticc.4	$⊢ (φ \land x \in [A, C]) \to D \in V$
	itgspliticc.5	$⊢ φ \to (x \in [A, B] ⟼ D) \in 𝐿^{1}$
	itgspliticc.6	$⊢ φ \to (x \in [B, C] ⟼ D) \in 𝐿^{1}$
Assertion	itgspliticc	$⊢ φ \to \int_{[A, C]} D d x = \int_{[A, B]} D d x + \int_{[B, C]} D d x$

Proof

Step	Hyp	Ref	Expression
1		itgspliticc.1	$⊢ φ \to A \in ℝ$
2		itgspliticc.2	$⊢ φ \to C \in ℝ$
3		itgspliticc.3	$⊢ φ \to B \in [A, C]$
4		itgspliticc.4	$⊢ (φ \land x \in [A, C]) \to D \in V$
5		itgspliticc.5	$⊢ φ \to (x \in [A, B] ⟼ D) \in 𝐿^{1}$
6		itgspliticc.6	$⊢ φ \to (x \in [B, C] ⟼ D) \in 𝐿^{1}$
7	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
8		elicc2	$⊢ (A \in ℝ \land C \in ℝ) \to (B \in [A, C] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq C))$
9	1 2 8	syl2anc	$⊢ φ \to (B \in [A, C] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq C))$
10	3 9	mpbid	$⊢ φ \to (B \in ℝ \land A \leq B \land B \leq C)$
11	10	simp1d	$⊢ φ \to B \in ℝ$
12	11	rexrd	$⊢ φ \to B \in ℝ^{*}$
13	2	rexrd	$⊢ φ \to C \in ℝ^{*}$
14		df-icc	$⊢ [.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x \leq z \land z \leq y)\})$
15		xrmaxle	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land z \in ℝ^{*}) \to (if (A \leq B, B, A) \leq z \leftrightarrow (A \leq z \land B \leq z))$
16		xrlemin	$⊢ (z \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \to (z \leq if (B \leq C, B, C) \leftrightarrow (z \leq B \land z \leq C))$
17	14 15 16	ixxin	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (B \in ℝ^{} \land C \in ℝ^{})) \to [A, B] \cap [B, C] = [if (A \leq B, B, A), if (B \leq C, B, C)]$
18	7 12 12 13 17	syl22anc	$⊢ φ \to [A, B] \cap [B, C] = [if (A \leq B, B, A), if (B \leq C, B, C)]$
19	10	simp2d	$⊢ φ \to A \leq B$
20	19	iftrued	$⊢ φ \to if (A \leq B, B, A) = B$
21	10	simp3d	$⊢ φ \to B \leq C$
22	21	iftrued	$⊢ φ \to if (B \leq C, B, C) = B$
23	20 22	oveq12d	$⊢ φ \to [if (A \leq B, B, A), if (B \leq C, B, C)] = [B, B]$
24		iccid	$⊢ B \in ℝ^{*} \to [B, B] = \{B\}$
25	12 24	syl	$⊢ φ \to [B, B] = \{B\}$
26	18 23 25	3eqtrd	$⊢ φ \to [A, B] \cap [B, C] = \{B\}$
27	26	fveq2d	$⊢ φ \to {vol}^{} ([A, B] \cap [B, C]) = {vol}^{} (\{B\})$
28		ovolsn	$⊢ B \in ℝ \to {vol}^{*} (\{B\}) = 0$
29	11 28	syl	$⊢ φ \to {vol}^{*} (\{B\}) = 0$
30	27 29	eqtrd	$⊢ φ \to {vol}^{*} ([A, B] \cap [B, C]) = 0$
31		iccsplit	$⊢ (A \in ℝ \land C \in ℝ \land B \in [A, C]) \to [A, C] = [A, B] \cup [B, C]$
32	1 2 3 31	syl3anc	$⊢ φ \to [A, C] = [A, B] \cup [B, C]$
33	30 32 4 5 6	itgsplit	$⊢ φ \to \int_{[A, C]} D d x = \int_{[A, B]} D d x + \int_{[B, C]} D d x$

Metamath Proof Explorer

Theorem itgspliticc

Proof