itgsplitioo

Description: The S. integral splits on open intervals with matching endpoints. (Contributed by Mario Carneiro, 2-Sep-2014)

	Ref	Expression
Hypotheses	itgsplitioo.1	$⊢ φ \to A \in ℝ$
	itgsplitioo.2	$⊢ φ \to C \in ℝ$
	itgsplitioo.3	$⊢ φ \to B \in [A, C]$
	itgsplitioo.4	$⊢ (φ \land x \in (A, C)) \to D \in ℂ$
	itgsplitioo.5	$⊢ φ \to (x \in (A, B) ⟼ D) \in 𝐿^{1}$
	itgsplitioo.6	$⊢ φ \to (x \in (B, C) ⟼ D) \in 𝐿^{1}$
Assertion	itgsplitioo	$⊢ φ \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		itgsplitioo.1	$⊢ φ \to A \in ℝ$
2		itgsplitioo.2	$⊢ φ \to C \in ℝ$
3		itgsplitioo.3	$⊢ φ \to B \in [A, C]$
4		itgsplitioo.4	$⊢ (φ \land x \in (A, C)) \to D \in ℂ$
5		itgsplitioo.5	$⊢ φ \to (x \in (A, B) ⟼ D) \in 𝐿^{1}$
6		itgsplitioo.6	$⊢ φ \to (x \in (B, C) ⟼ D) \in 𝐿^{1}$
7		elicc2	$⊢ (A \in ℝ \land C \in ℝ) \to (B \in [A, C] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq C))$
8	1 2 7	syl2anc	$⊢ φ \to (B \in [A, C] \leftrightarrow (B \in ℝ \land A \leq B \land B \leq C))$
9	3 8	mpbid	$⊢ φ \to (B \in ℝ \land A \leq B \land B \leq C)$
10	9	simp2d	$⊢ φ \to A \leq B$
11	9	simp1d	$⊢ φ \to B \in ℝ$
12	1 11	leloed	$⊢ φ \to (A \leq B \leftrightarrow (A < B \lor A = B))$
13	10 12	mpbid	$⊢ φ \to (A < B \lor A = B)$
14	13	ord	$⊢ φ \to (\neg A < B \to A = B)$
15	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
16		iooss1	$⊢ (A \in ℝ^{*} \land A \leq B) \to (B, C) \subseteq (A, C)$
17	15 10 16	syl2anc	$⊢ φ \to (B, C) \subseteq (A, C)$
18	17	sselda	$⊢ (φ \land x \in (B, C)) \to x \in (A, C)$
19	18 4	syldan	$⊢ (φ \land x \in (B, C)) \to D \in ℂ$
20	19 6	itgcl	$⊢ φ \to \int_{(B, C)} D d x \in ℂ$
21	20	addid2d	$⊢ φ \to 0 + \int_{(B, C)} D d x = \int_{(B, C)} D d x$
22	21	eqcomd	$⊢ φ \to \int_{(B, C)} D d x = 0 + \int_{(B, C)} D d x$
23		oveq1	$⊢ A = B \to (A, C) = (B, C)$
24		itgeq1	$⊢ (A, C) = (B, C) \to \int_{(A, C)} D d x = \int_{(B, C)} D d x$
25	23 24	syl	$⊢ A = B \to \int_{(A, C)} D d x = \int_{(B, C)} D d x$
26		oveq1	$⊢ A = B \to (A, B) = (B, B)$
27		iooid	$⊢ (B, B) = \emptyset$
28	26 27	eqtrdi	$⊢ A = B \to (A, B) = \emptyset$
29		itgeq1	$⊢ (A, B) = \emptyset \to \int_{(A, B)} D d x = \int_{\emptyset} D d x$
30	28 29	syl	$⊢ A = B \to \int_{(A, B)} D d x = \int_{\emptyset} D d x$
31		itg0	$⊢ \int_{\emptyset} D d x = 0$
32	30 31	eqtrdi	$⊢ A = B \to \int_{(A, B)} D d x = 0$
33	32	oveq1d	$⊢ A = B \to \int_{(A, B)} D d x + \int_{(B, C)} D d x = 0 + \int_{(B, C)} D d x$
34	25 33	eqeq12d	$⊢ A = B \to (\int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x \leftrightarrow \int_{(B, C)} D d x = 0 + \int_{(B, C)} D d x)$
35	22 34	syl5ibrcom	$⊢ φ \to (A = B \to \int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x)$
36	14 35	syld	$⊢ φ \to (\neg A < B \to \int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x)$
37	9	simp3d	$⊢ φ \to B \leq C$
38	11 2	leloed	$⊢ φ \to (B \leq C \leftrightarrow (B < C \lor B = C))$
39	37 38	mpbid	$⊢ φ \to (B < C \lor B = C)$
40	39	ord	$⊢ φ \to (\neg B < C \to B = C)$
41	2	rexrd	$⊢ φ \to C \in ℝ^{*}$
42		iooss2	$⊢ (C \in ℝ^{*} \land B \leq C) \to (A, B) \subseteq (A, C)$
43	41 37 42	syl2anc	$⊢ φ \to (A, B) \subseteq (A, C)$
44	43	sselda	$⊢ (φ \land x \in (A, B)) \to x \in (A, C)$
45	44 4	syldan	$⊢ (φ \land x \in (A, B)) \to D \in ℂ$
46	45 5	itgcl	$⊢ φ \to \int_{(A, B)} D d x \in ℂ$
47	46	addid1d	$⊢ φ \to \int_{(A, B)} D d x + 0 = \int_{(A, B)} D d x$
48	47	eqcomd	$⊢ φ \to \int_{(A, B)} D d x = \int_{(A, B)} D d x + 0$
49		oveq2	$⊢ B = C \to (A, B) = (A, C)$
50		itgeq1	$⊢ (A, B) = (A, C) \to \int_{(A, B)} D d x = \int_{(A, C)} D d x$
51	49 50	syl	$⊢ B = C \to \int_{(A, B)} D d x = \int_{(A, C)} D d x$
52		oveq2	$⊢ B = C \to (B, B) = (B, C)$
53	27 52	eqtr3id	$⊢ B = C \to \emptyset = (B, C)$
54		itgeq1	$⊢ \emptyset = (B, C) \to \int_{\emptyset} D d x = \int_{(B, C)} D d x$
55	53 54	syl	$⊢ B = C \to \int_{\emptyset} D d x = \int_{(B, C)} D d x$
56	31 55	eqtr3id	$⊢ B = C \to 0 = \int_{(B, C)} D d x$
57	56	oveq2d	$⊢ B = C \to \int_{(A, B)} D d x + 0 = \int_{(A, B)} D d x + \int_{(B, C)} D d x$
58	51 57	eqeq12d	$⊢ B = C \to (\int_{(A, B)} D d x = \int_{(A, B)} D d x + 0 \leftrightarrow \int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x)$
59	48 58	syl5ibcom	$⊢ φ \to (B = C \to \int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x)$
60	40 59	syld	$⊢ φ \to (\neg B < C \to \int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x)$
61		indir	$⊢ ((A, B) \cup \{B\}) \cap (B, C) = ((A, B) \cap (B, C)) \cup (\{B\} \cap (B, C))$
62	11	rexrd	$⊢ φ \to B \in ℝ^{*}$
63	15 62	jca	$⊢ φ \to (A \in ℝ^{} \land B \in ℝ^{})$
64	63	adantr	$⊢ (φ \land (A < B \land B < C)) \to (A \in ℝ^{} \land B \in ℝ^{})$
65	62 41	jca	$⊢ φ \to (B \in ℝ^{} \land C \in ℝ^{})$
66	65	adantr	$⊢ (φ \land (A < B \land B < C)) \to (B \in ℝ^{} \land C \in ℝ^{})$
67	11	adantr	$⊢ (φ \land (A < B \land B < C)) \to B \in ℝ$
68	67	leidd	$⊢ (φ \land (A < B \land B < C)) \to B \leq B$
69		ioodisj	$⊢ (((A \in ℝ^{} \land B \in ℝ^{}) \land (B \in ℝ^{} \land C \in ℝ^{})) \land B \leq B) \to (A, B) \cap (B, C) = \emptyset$
70	64 66 68 69	syl21anc	$⊢ (φ \land (A < B \land B < C)) \to (A, B) \cap (B, C) = \emptyset$
71		incom	$⊢ \{B\} \cap (B, C) = (B, C) \cap \{B\}$
72	67	ltnrd	$⊢ (φ \land (A < B \land B < C)) \to \neg B < B$
73		eliooord	$⊢ B \in (B, C) \to (B < B \land B < C)$
74	73	simpld	$⊢ B \in (B, C) \to B < B$
75	72 74	nsyl	$⊢ (φ \land (A < B \land B < C)) \to \neg B \in (B, C)$
76		disjsn	$⊢ (B, C) \cap \{B\} = \emptyset \leftrightarrow \neg B \in (B, C)$
77	75 76	sylibr	$⊢ (φ \land (A < B \land B < C)) \to (B, C) \cap \{B\} = \emptyset$
78	71 77	syl5eq	$⊢ (φ \land (A < B \land B < C)) \to \{B\} \cap (B, C) = \emptyset$
79	70 78	uneq12d	$⊢ (φ \land (A < B \land B < C)) \to ((A, B) \cap (B, C)) \cup (\{B\} \cap (B, C)) = \emptyset \cup \emptyset$
80		un0	$⊢ \emptyset \cup \emptyset = \emptyset$
81	79 80	eqtrdi	$⊢ (φ \land (A < B \land B < C)) \to ((A, B) \cap (B, C)) \cup (\{B\} \cap (B, C)) = \emptyset$
82	61 81	syl5eq	$⊢ (φ \land (A < B \land B < C)) \to ((A, B) \cup \{B\}) \cap (B, C) = \emptyset$
83	82	fveq2d	$⊢ (φ \land (A < B \land B < C)) \to {vol}^{} (((A, B) \cup \{B\}) \cap (B, C)) = {vol}^{} (\emptyset)$
84		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
85	83 84	eqtrdi	$⊢ (φ \land (A < B \land B < C)) \to {vol}^{*} (((A, B) \cup \{B\}) \cap (B, C)) = 0$
86	15 62 41	3jca	$⊢ φ \to (A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*})$
87		ioojoin	$⊢ ((A \in ℝ^{} \land B \in ℝ^{} \land C \in ℝ^{*}) \land (A < B \land B < C)) \to ((A, B) \cup \{B\}) \cup (B, C) = (A, C)$
88	86 87	sylan	$⊢ (φ \land (A < B \land B < C)) \to ((A, B) \cup \{B\}) \cup (B, C) = (A, C)$
89	88	eqcomd	$⊢ (φ \land (A < B \land B < C)) \to (A, C) = ((A, B) \cup \{B\}) \cup (B, C)$
90	4	adantlr	$⊢ ((φ \land (A < B \land B < C)) \land x \in (A, C)) \to D \in ℂ$
91	5	adantr	$⊢ (φ \land (A < B \land B < C)) \to (x \in (A, B) ⟼ D) \in 𝐿^{1}$
92		ssun1	$⊢ (A, B) \subseteq (A, B) \cup \{B\}$
93	92	a1i	$⊢ (φ \land (A < B \land B < C)) \to (A, B) \subseteq (A, B) \cup \{B\}$
94		ioossre	$⊢ (A, B) \subseteq ℝ$
95	94	a1i	$⊢ (φ \land (A < B \land B < C)) \to (A, B) \subseteq ℝ$
96	67	snssd	$⊢ (φ \land (A < B \land B < C)) \to \{B\} \subseteq ℝ$
97	95 96	unssd	$⊢ (φ \land (A < B \land B < C)) \to (A, B) \cup \{B\} \subseteq ℝ$
98		uncom	$⊢ (A, B) \cup \{B\} = \{B\} \cup (A, B)$
99	98	difeq1i	$⊢ ((A, B) \cup \{B\}) ∖ (A, B) = (\{B\} \cup (A, B)) ∖ (A, B)$
100		difun2	$⊢ (\{B\} \cup (A, B)) ∖ (A, B) = \{B\} ∖ (A, B)$
101	99 100	eqtri	$⊢ ((A, B) \cup \{B\}) ∖ (A, B) = \{B\} ∖ (A, B)$
102		difss	$⊢ \{B\} ∖ (A, B) \subseteq \{B\}$
103	101 102	eqsstri	$⊢ ((A, B) \cup \{B\}) ∖ (A, B) \subseteq \{B\}$
104		ovolsn	$⊢ B \in ℝ \to {vol}^{*} (\{B\}) = 0$
105	67 104	syl	$⊢ (φ \land (A < B \land B < C)) \to {vol}^{*} (\{B\}) = 0$
106		ovolssnul	$⊢ (((A, B) \cup \{B\}) ∖ (A, B) \subseteq \{B\} \land \{B\} \subseteq ℝ \land {vol}^{} (\{B\}) = 0) \to {vol}^{} (((A, B) \cup \{B\}) ∖ (A, B)) = 0$
107	103 96 105 106	mp3an2i	$⊢ (φ \land (A < B \land B < C)) \to {vol}^{*} (((A, B) \cup \{B\}) ∖ (A, B)) = 0$
108		ssun1	$⊢ (A, B) \cup \{B\} \subseteq ((A, B) \cup \{B\}) \cup (B, C)$
109	108 88	sseqtrid	$⊢ (φ \land (A < B \land B < C)) \to (A, B) \cup \{B\} \subseteq (A, C)$
110	109	sselda	$⊢ ((φ \land (A < B \land B < C)) \land x \in ((A, B) \cup \{B\})) \to x \in (A, C)$
111	110 90	syldan	$⊢ ((φ \land (A < B \land B < C)) \land x \in ((A, B) \cup \{B\})) \to D \in ℂ$
112	93 97 107 111	itgss3	$⊢ (φ \land (A < B \land B < C)) \to (((x \in (A, B) ⟼ D) \in 𝐿^{1} \leftrightarrow (x \in ((A, B) \cup \{B\}) ⟼ D) \in 𝐿^{1}) \land \int_{(A, B)} D d x = \int_{((A, B) \cup \{B\})} D d x)$
113	112	simpld	$⊢ (φ \land (A < B \land B < C)) \to ((x \in (A, B) ⟼ D) \in 𝐿^{1} \leftrightarrow (x \in ((A, B) \cup \{B\}) ⟼ D) \in 𝐿^{1})$
114	91 113	mpbid	$⊢ (φ \land (A < B \land B < C)) \to (x \in ((A, B) \cup \{B\}) ⟼ D) \in 𝐿^{1}$
115	6	adantr	$⊢ (φ \land (A < B \land B < C)) \to (x \in (B, C) ⟼ D) \in 𝐿^{1}$
116	85 89 90 114 115	itgsplit	$⊢ (φ \land (A < B \land B < C)) \to \int_{(A, C)} D d x = \int_{((A, B) \cup \{B\})} D d x + \int_{(B, C)} D d x$
117	112	simprd	$⊢ (φ \land (A < B \land B < C)) \to \int_{(A, B)} D d x = \int_{((A, B) \cup \{B\})} D d x$
118	117	oveq1d	$⊢ (φ \land (A < B \land B < C)) \to \int_{(A, B)} D d x + \int_{(B, C)} D d x = \int_{((A, B) \cup \{B\})} D d x + \int_{(B, C)} D d x$
119	116 118	eqtr4d	$⊢ (φ \land (A < B \land B < C)) \to \int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x$
120	119	ex	$⊢ φ \to ((A < B \land B < C) \to \int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x)$
121	36 60 120	ecased	$⊢ φ \to \int_{(A, C)} D d x = \int_{(A, B)} D d x + \int_{(B, C)} D d x$

Metamath Proof Explorer

Theorem itgsplitioo

Proof