itgioocnicc

Description: The integral of a piecewise continuous function F on an open interval is equal to the integral of the continuous function G , in the corresponding closed interval. G is equal to F on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	itgioocnicc.a	$⊢ φ \to A \in ℝ$
	itgioocnicc.b	$⊢ φ \to B \in ℝ$
	itgioocnicc.f	$⊢ φ \to F : dom F ⟶ ℂ$
	itgioocnicc.fcn	$⊢ φ \to ({F ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ$
	itgioocnicc.fdom	$⊢ φ \to [A, B] \subseteq dom F$
	itgioocnicc.r	$⊢ φ \to R \in (({F ↾}_{(A, B)}) {lim}_{ℂ} A)$
	itgioocnicc.l	$⊢ φ \to L \in (({F ↾}_{(A, B)}) {lim}_{ℂ} B)$
	itgioocnicc.g	$⊢ G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
Assertion	itgioocnicc	$⊢ φ \to (G \in 𝐿^{1} \land \int_{[A, B]} G (x) d x = \int_{[A, B]} F (x) d x)$

Proof

Step	Hyp	Ref	Expression
1		itgioocnicc.a	$⊢ φ \to A \in ℝ$
2		itgioocnicc.b	$⊢ φ \to B \in ℝ$
3		itgioocnicc.f	$⊢ φ \to F : dom F ⟶ ℂ$
4		itgioocnicc.fcn	$⊢ φ \to ({F ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ$
5		itgioocnicc.fdom	$⊢ φ \to [A, B] \subseteq dom F$
6		itgioocnicc.r	$⊢ φ \to R \in (({F ↾}_{(A, B)}) {lim}_{ℂ} A)$
7		itgioocnicc.l	$⊢ φ \to L \in (({F ↾}_{(A, B)}) {lim}_{ℂ} B)$
8		itgioocnicc.g	$⊢ G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x))))$
9		iftrue	$⊢ x = A \to if (x = A, R, if (x = B, L, F (x))) = R$
10		iftrue	$⊢ x = A \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = R$
11	9 10	eqtr4d	$⊢ x = A \to if (x = A, R, if (x = B, L, F (x))) = if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))$
12	11	adantl	$⊢ ((φ \land x \in [A, B]) \land x = A) \to if (x = A, R, if (x = B, L, F (x))) = if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))$
13		iftrue	$⊢ x = B \to if (x = B, L, F (x)) = L$
14		iftrue	$⊢ x = B \to if (x = B, L, ({F ↾}_{(A, B)}) (x)) = L$
15	13 14	eqtr4d	$⊢ x = B \to if (x = B, L, F (x)) = if (x = B, L, ({F ↾}_{(A, B)}) (x))$
16	15	adantl	$⊢ (\neg x = A \land x = B) \to if (x = B, L, F (x)) = if (x = B, L, ({F ↾}_{(A, B)}) (x))$
17	16	ifeq2d	$⊢ (\neg x = A \land x = B) \to if (x = A, R, if (x = B, L, F (x))) = if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))$
18	17	adantll	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) = if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))$
19		iffalse	$⊢ \neg x = A \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
20	19	ad2antlr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
21		iffalse	$⊢ \neg x = B \to if (x = B, L, F (x)) = F (x)$
22	21	adantl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = B, L, F (x)) = F (x)$
23		iffalse	$⊢ \neg x = A \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = B, L, ({F ↾}_{(A, B)}) (x))$
24	23	ad2antlr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))) = if (x = B, L, ({F ↾}_{(A, B)}) (x))$
25		iffalse	$⊢ \neg x = B \to if (x = B, L, ({F ↾}_{(A, B)}) (x)) = ({F ↾}_{(A, B)}) (x)$
26	25	adantl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = B, L, ({F ↾}_{(A, B)}) (x)) = ({F ↾}_{(A, B)}) (x)$
27	1	adantr	$⊢ (φ \land x \in [A, B]) \to A \in ℝ$
28	27	rexrd	$⊢ (φ \land x \in [A, B]) \to A \in ℝ^{*}$
29	28	ad2antrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A \in ℝ^{*}$
30	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
31	30	ad3antrrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to B \in ℝ^{*}$
32	2	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ$
33		simpr	$⊢ (φ \land x \in [A, B]) \to x \in [A, B]$
34		eliccre	$⊢ (A \in ℝ \land B \in ℝ \land x \in [A, B]) \to x \in ℝ$
35	27 32 33 34	syl3anc	$⊢ (φ \land x \in [A, B]) \to x \in ℝ$
36	35	ad2antrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in ℝ$
37	1	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A \in ℝ$
38	35	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to x \in ℝ$
39	30	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ^{*}$
40		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to A \leq x$
41	28 39 33 40	syl3anc	$⊢ (φ \land x \in [A, B]) \to A \leq x$
42	41	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A \leq x$
43		neqne	$⊢ \neg x = A \to x \neq A$
44	43	adantl	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to x \neq A$
45	37 38 42 44	leneltd	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A < x$
46	45	adantr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A < x$
47	35	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x \in ℝ$
48	2	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to B \in ℝ$
49		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to x \leq B$
50	28 39 33 49	syl3anc	$⊢ (φ \land x \in [A, B]) \to x \leq B$
51	50	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x \leq B$
52		eqcom	$⊢ x = B \leftrightarrow B = x$
53	52	notbii	$⊢ \neg x = B \leftrightarrow \neg B = x$
54	53	biimpi	$⊢ \neg x = B \to \neg B = x$
55	54	neqned	$⊢ \neg x = B \to B \neq x$
56	55	adantl	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to B \neq x$
57	47 48 51 56	leneltd	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x < B$
58	57	adantlr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x < B$
59	29 31 36 46 58	eliood	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in (A, B)$
60		fvres	$⊢ x \in (A, B) \to ({F ↾}_{(A, B)}) (x) = F (x)$
61	59 60	syl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to ({F ↾}_{(A, B)}) (x) = F (x)$
62	24 26 61	3eqtrrd	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to F (x) = if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))$
63	20 22 62	3eqtrd	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, F (x))) = if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))$
64	18 63	pm2.61dan	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to if (x = A, R, if (x = B, L, F (x))) = if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))$
65	12 64	pm2.61dan	$⊢ (φ \land x \in [A, B]) \to if (x = A, R, if (x = B, L, F (x))) = if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))$
66	65	mpteq2dva	$⊢ φ \to (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x)))) = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))))$
67	8 66	syl5eq	$⊢ φ \to G = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))))$
68		nfv	$⊢ Ⅎ x φ$
69		eqid	$⊢ (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))) = (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x))))$
70	68 69 1 2 4 7 6	cncfiooicc	$⊢ φ \to (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, ({F ↾}_{(A, B)}) (x)))) : [A, B] \underset{cn}{⟶} ℂ$
71	67 70	eqeltrd	$⊢ φ \to G : [A, B] \underset{cn}{⟶} ℂ$
72		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land G : [A, B] \underset{cn}{⟶} ℂ) \to G \in 𝐿^{1}$
73	1 2 71 72	syl3anc	$⊢ φ \to G \in 𝐿^{1}$
74	9	adantl	$⊢ ((φ \land x \in [A, B]) \land x = A) \to if (x = A, R, if (x = B, L, F (x))) = R$
75		limccl	$⊢ ({F ↾}_{(A, B)}) {lim}_{ℂ} A \subseteq ℂ$
76	75 6	sseldi	$⊢ φ \to R \in ℂ$
77	76	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land x = A) \to R \in ℂ$
78	74 77	eqeltrd	$⊢ ((φ \land x \in [A, B]) \land x = A) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
79	19 13	sylan9eq	$⊢ (\neg x = A \land x = B) \to if (x = A, R, if (x = B, L, F (x))) = L$
80	79	adantll	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) = L$
81		limccl	$⊢ ({F ↾}_{(A, B)}) {lim}_{ℂ} B \subseteq ℂ$
82	81 7	sseldi	$⊢ φ \to L \in ℂ$
83	82	ad3antrrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land x = B) \to L \in ℂ$
84	80 83	eqeltrd	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
85	19 21	sylan9eq	$⊢ (\neg x = A \land \neg x = B) \to if (x = A, R, if (x = B, L, F (x))) = F (x)$
86	85	adantll	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, F (x))) = F (x)$
87	61	eqcomd	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to F (x) = ({F ↾}_{(A, B)}) (x)$
88		cncff	$⊢ ({F ↾}_{(A, B)}) : (A, B) \underset{cn}{⟶} ℂ \to ({F ↾}_{(A, B)}) : (A, B) ⟶ ℂ$
89	4 88	syl	$⊢ φ \to ({F ↾}_{(A, B)}) : (A, B) ⟶ ℂ$
90	89	ad3antrrr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to ({F ↾}_{(A, B)}) : (A, B) ⟶ ℂ$
91	90 59	ffvelrnd	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to ({F ↾}_{(A, B)}) (x) \in ℂ$
92	87 91	eqeltrd	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to F (x) \in ℂ$
93	86 92	eqeltrd	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
94	84 93	pm2.61dan	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
95	78 94	pm2.61dan	$⊢ (φ \land x \in [A, B]) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
96	8	fvmpt2	$⊢ (x \in [A, B] \land if (x = A, R, if (x = B, L, F (x))) \in ℂ) \to G (x) = if (x = A, R, if (x = B, L, F (x)))$
97	33 95 96	syl2anc	$⊢ (φ \land x \in [A, B]) \to G (x) = if (x = A, R, if (x = B, L, F (x)))$
98	97 95	eqeltrd	$⊢ (φ \land x \in [A, B]) \to G (x) \in ℂ$
99	1 2 98	itgioo	$⊢ φ \to \int_{(A, B)} G (x) d x = \int_{[A, B]} G (x) d x$
100	99	eqcomd	$⊢ φ \to \int_{[A, B]} G (x) d x = \int_{(A, B)} G (x) d x$
101		ioossicc	$⊢ (A, B) \subseteq [A, B]$
102	101	sseli	$⊢ x \in (A, B) \to x \in [A, B]$
103	102 97	sylan2	$⊢ (φ \land x \in (A, B)) \to G (x) = if (x = A, R, if (x = B, L, F (x)))$
104	1	adantr	$⊢ (φ \land x \in (A, B)) \to A \in ℝ$
105		eliooord	$⊢ x \in (A, B) \to (A < x \land x < B)$
106	105	simpld	$⊢ x \in (A, B) \to A < x$
107	106	adantl	$⊢ (φ \land x \in (A, B)) \to A < x$
108	104 107	gtned	$⊢ (φ \land x \in (A, B)) \to x \neq A$
109	108	neneqd	$⊢ (φ \land x \in (A, B)) \to \neg x = A$
110	109 19	syl	$⊢ (φ \land x \in (A, B)) \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
111	102 35	sylan2	$⊢ (φ \land x \in (A, B)) \to x \in ℝ$
112	105	simprd	$⊢ x \in (A, B) \to x < B$
113	112	adantl	$⊢ (φ \land x \in (A, B)) \to x < B$
114	111 113	ltned	$⊢ (φ \land x \in (A, B)) \to x \neq B$
115	114	neneqd	$⊢ (φ \land x \in (A, B)) \to \neg x = B$
116	115 21	syl	$⊢ (φ \land x \in (A, B)) \to if (x = B, L, F (x)) = F (x)$
117	103 110 116	3eqtrd	$⊢ (φ \land x \in (A, B)) \to G (x) = F (x)$
118	117	itgeq2dv	$⊢ φ \to \int_{(A, B)} G (x) d x = \int_{(A, B)} F (x) d x$
119	3	adantr	$⊢ (φ \land x \in [A, B]) \to F : dom F ⟶ ℂ$
120	5	sselda	$⊢ (φ \land x \in [A, B]) \to x \in dom F$
121	119 120	ffvelrnd	$⊢ (φ \land x \in [A, B]) \to F (x) \in ℂ$
122	1 2 121	itgioo	$⊢ φ \to \int_{(A, B)} F (x) d x = \int_{[A, B]} F (x) d x$
123	100 118 122	3eqtrd	$⊢ φ \to \int_{[A, B]} G (x) d x = \int_{[A, B]} F (x) d x$
124	73 123	jca	$⊢ φ \to (G \in 𝐿^{1} \land \int_{[A, B]} G (x) d x = \int_{[A, B]} F (x) d x)$

Metamath Proof Explorer

Theorem itgioocnicc

Proof