ditgcl

Description: Closure of a directed integral. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Hypotheses	ditgcl.x	$⊢ φ \to X \in ℝ$
	ditgcl.y	$⊢ φ \to Y \in ℝ$
	ditgcl.a	$⊢ φ \to A \in [X, Y]$
	ditgcl.b	$⊢ φ \to B \in [X, Y]$
	ditgcl.c	$⊢ (φ \land x \in (X, Y)) \to C \in V$
	ditgcl.i	$⊢ φ \to (x \in (X, Y) ⟼ C) \in 𝐿^{1}$
Assertion	ditgcl	$⊢ φ \to \int_{A}^{B} C d x \in ℂ$

Proof

Step	Hyp	Ref	Expression
1		ditgcl.x	$⊢ φ \to X \in ℝ$
2		ditgcl.y	$⊢ φ \to Y \in ℝ$
3		ditgcl.a	$⊢ φ \to A \in [X, Y]$
4		ditgcl.b	$⊢ φ \to B \in [X, Y]$
5		ditgcl.c	$⊢ (φ \land x \in (X, Y)) \to C \in V$
6		ditgcl.i	$⊢ φ \to (x \in (X, Y) ⟼ C) \in 𝐿^{1}$
7		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (A \in [X, Y] \leftrightarrow (A \in ℝ \land X \leq A \land A \leq Y))$
8	1 2 7	syl2anc	$⊢ φ \to (A \in [X, Y] \leftrightarrow (A \in ℝ \land X \leq A \land A \leq Y))$
9	3 8	mpbid	$⊢ φ \to (A \in ℝ \land X \leq A \land A \leq Y)$
10	9	simp1d	$⊢ φ \to A \in ℝ$
11		elicc2	$⊢ (X \in ℝ \land Y \in ℝ) \to (B \in [X, Y] \leftrightarrow (B \in ℝ \land X \leq B \land B \leq Y))$
12	1 2 11	syl2anc	$⊢ φ \to (B \in [X, Y] \leftrightarrow (B \in ℝ \land X \leq B \land B \leq Y))$
13	4 12	mpbid	$⊢ φ \to (B \in ℝ \land X \leq B \land B \leq Y)$
14	13	simp1d	$⊢ φ \to B \in ℝ$
15		simpr	$⊢ (φ \land A \leq B) \to A \leq B$
16	15	ditgpos	$⊢ (φ \land A \leq B) \to \int_{A}^{B} C d x = \int_{(A, B)} C d x$
17	1	rexrd	$⊢ φ \to X \in ℝ^{*}$
18	9	simp2d	$⊢ φ \to X \leq A$
19		iooss1	$⊢ (X \in ℝ^{*} \land X \leq A) \to (A, B) \subseteq (X, B)$
20	17 18 19	syl2anc	$⊢ φ \to (A, B) \subseteq (X, B)$
21	2	rexrd	$⊢ φ \to Y \in ℝ^{*}$
22	13	simp3d	$⊢ φ \to B \leq Y$
23		iooss2	$⊢ (Y \in ℝ^{*} \land B \leq Y) \to (X, B) \subseteq (X, Y)$
24	21 22 23	syl2anc	$⊢ φ \to (X, B) \subseteq (X, Y)$
25	20 24	sstrd	$⊢ φ \to (A, B) \subseteq (X, Y)$
26	25	sselda	$⊢ (φ \land x \in (A, B)) \to x \in (X, Y)$
27	26 5	syldan	$⊢ (φ \land x \in (A, B)) \to C \in V$
28		ioombl	$⊢ (A, B) \in dom vol$
29	28	a1i	$⊢ φ \to (A, B) \in dom vol$
30	25 29 5 6	iblss	$⊢ φ \to (x \in (A, B) ⟼ C) \in 𝐿^{1}$
31	27 30	itgcl	$⊢ φ \to \int_{(A, B)} C d x \in ℂ$
32	31	adantr	$⊢ (φ \land A \leq B) \to \int_{(A, B)} C d x \in ℂ$
33	16 32	eqeltrd	$⊢ (φ \land A \leq B) \to \int_{A}^{B} C d x \in ℂ$
34		simpr	$⊢ (φ \land B \leq A) \to B \leq A$
35	14	adantr	$⊢ (φ \land B \leq A) \to B \in ℝ$
36	10	adantr	$⊢ (φ \land B \leq A) \to A \in ℝ$
37	34 35 36	ditgneg	$⊢ (φ \land B \leq A) \to \int_{A}^{B} C d x = - \int_{(B, A)} C d x$
38	13	simp2d	$⊢ φ \to X \leq B$
39		iooss1	$⊢ (X \in ℝ^{*} \land X \leq B) \to (B, A) \subseteq (X, A)$
40	17 38 39	syl2anc	$⊢ φ \to (B, A) \subseteq (X, A)$
41	9	simp3d	$⊢ φ \to A \leq Y$
42		iooss2	$⊢ (Y \in ℝ^{*} \land A \leq Y) \to (X, A) \subseteq (X, Y)$
43	21 41 42	syl2anc	$⊢ φ \to (X, A) \subseteq (X, Y)$
44	40 43	sstrd	$⊢ φ \to (B, A) \subseteq (X, Y)$
45	44	sselda	$⊢ (φ \land x \in (B, A)) \to x \in (X, Y)$
46	45 5	syldan	$⊢ (φ \land x \in (B, A)) \to C \in V$
47		ioombl	$⊢ (B, A) \in dom vol$
48	47	a1i	$⊢ φ \to (B, A) \in dom vol$
49	44 48 5 6	iblss	$⊢ φ \to (x \in (B, A) ⟼ C) \in 𝐿^{1}$
50	46 49	itgcl	$⊢ φ \to \int_{(B, A)} C d x \in ℂ$
51	50	negcld	$⊢ φ \to - \int_{(B, A)} C d x \in ℂ$
52	51	adantr	$⊢ (φ \land B \leq A) \to - \int_{(B, A)} C d x \in ℂ$
53	37 52	eqeltrd	$⊢ (φ \land B \leq A) \to \int_{A}^{B} C d x \in ℂ$
54	10 14 33 53	lecasei	$⊢ φ \to \int_{A}^{B} C d x \in ℂ$

Metamath Proof Explorer

Theorem ditgcl

Proof