iblcncfioo

Description: A continuous function F on an open interval ( A (,) B ) with a finite right limit R in A and a finite left limit L in B is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	iblcncfioo.a	$⊢ φ \to A \in ℝ$
	iblcncfioo.b	$⊢ φ \to B \in ℝ$
	iblcncfioo.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
	iblcncfioo.l	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
	iblcncfioo.r	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
Assertion	iblcncfioo	$⊢ φ \to F \in 𝐿^{1}$

Proof

Step	Hyp	Ref	Expression
1		iblcncfioo.a	$⊢ φ \to A \in ℝ$
2		iblcncfioo.b	$⊢ φ \to B \in ℝ$
3		iblcncfioo.f	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
4		iblcncfioo.l	$⊢ φ \to L \in (F {lim}_{ℂ} B)$
5		iblcncfioo.r	$⊢ φ \to R \in (F {lim}_{ℂ} A)$
6		cncff	$⊢ F : (A, B) \underset{cn}{⟶} ℂ \to F : (A, B) ⟶ ℂ$
7	3 6	syl	$⊢ φ \to F : (A, B) ⟶ ℂ$
8	7	feqmptd	$⊢ φ \to F = (x \in (A, B) ⟼ F (x))$
9	1	adantr	$⊢ (φ \land x \in (A, B)) \to A \in ℝ$
10		eliooord	$⊢ x \in (A, B) \to (A < x \land x < B)$
11	10	simpld	$⊢ x \in (A, B) \to A < x$
12	11	adantl	$⊢ (φ \land x \in (A, B)) \to A < x$
13	9 12	gtned	$⊢ (φ \land x \in (A, B)) \to x \neq A$
14	13	neneqd	$⊢ (φ \land x \in (A, B)) \to \neg x = A$
15	14	iffalsed	$⊢ (φ \land x \in (A, B)) \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
16		elioore	$⊢ x \in (A, B) \to x \in ℝ$
17	16	adantl	$⊢ (φ \land x \in (A, B)) \to x \in ℝ$
18	10	simprd	$⊢ x \in (A, B) \to x < B$
19	18	adantl	$⊢ (φ \land x \in (A, B)) \to x < B$
20	17 19	ltned	$⊢ (φ \land x \in (A, B)) \to x \neq B$
21	20	neneqd	$⊢ (φ \land x \in (A, B)) \to \neg x = B$
22	21	iffalsed	$⊢ (φ \land x \in (A, B)) \to if (x = B, L, F (x)) = F (x)$
23	15 22	eqtrd	$⊢ (φ \land x \in (A, B)) \to if (x = A, R, if (x = B, L, F (x))) = F (x)$
24	23	eqcomd	$⊢ (φ \land x \in (A, B)) \to F (x) = if (x = A, R, if (x = B, L, F (x)))$
25	24	mpteq2dva	$⊢ φ \to (x \in (A, B) ⟼ F (x)) = (x \in (A, B) ⟼ if (x = A, R, if (x = B, L, F (x))))$
26	8 25	eqtrd	$⊢ φ \to F = (x \in (A, B) ⟼ if (x = A, R, if (x = B, L, F (x))))$
27		ioossicc	$⊢ (A, B) \subseteq [A, B]$
28	27	a1i	$⊢ φ \to (A, B) \subseteq [A, B]$
29		ioombl	$⊢ (A, B) \in dom vol$
30	29	a1i	$⊢ φ \to (A, B) \in dom vol$
31		iftrue	$⊢ x = A \to if (x = A, R, if (x = B, L, F (x))) = R$
32	31	adantl	$⊢ (φ \land x = A) \to if (x = A, R, if (x = B, L, F (x))) = R$
33		limccl	$⊢ F {lim}_{ℂ} A \subseteq ℂ$
34	33 5	sselid	$⊢ φ \to R \in ℂ$
35	34	adantr	$⊢ (φ \land x = A) \to R \in ℂ$
36	32 35	eqeltrd	$⊢ (φ \land x = A) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
37	36	adantlr	$⊢ ((φ \land x \in [A, B]) \land x = A) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
38		iffalse	$⊢ \neg x = A \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
39	38	ad2antlr	$⊢ ((φ \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) = if (x = B, L, F (x))$
40		iftrue	$⊢ x = B \to if (x = B, L, F (x)) = L$
41	40	adantl	$⊢ ((φ \land \neg x = A) \land x = B) \to if (x = B, L, F (x)) = L$
42	39 41	eqtrd	$⊢ ((φ \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) = L$
43		limccl	$⊢ F {lim}_{ℂ} B \subseteq ℂ$
44	43 4	sselid	$⊢ φ \to L \in ℂ$
45	44	ad2antrr	$⊢ ((φ \land \neg x = A) \land x = B) \to L \in ℂ$
46	42 45	eqeltrd	$⊢ ((φ \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
47	46	adantllr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land x = B) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
48		simplll	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to φ$
49	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
50	48 49	syl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A \in ℝ^{*}$
51	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
52	48 51	syl	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to B \in ℝ^{*}$
53		eliccxr	$⊢ x \in [A, B] \to x \in ℝ^{*}$
54	53	ad3antlr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in ℝ^{*}$
55	50 52 54	3jca	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to (A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ^{*})$
56	1	ad2antrr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A \in ℝ$
57	1	adantr	$⊢ (φ \land x \in [A, B]) \to A \in ℝ$
58	2	adantr	$⊢ (φ \land x \in [A, B]) \to B \in ℝ$
59		simpr	$⊢ (φ \land x \in [A, B]) \to x \in [A, B]$
60		eliccre	$⊢ (A \in ℝ \land B \in ℝ \land x \in [A, B]) \to x \in ℝ$
61	57 58 59 60	syl3anc	$⊢ (φ \land x \in [A, B]) \to x \in ℝ$
62	61	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to x \in ℝ$
63	1 2	jca	$⊢ φ \to (A \in ℝ \land B \in ℝ)$
64	63	adantr	$⊢ (φ \land x \in [A, B]) \to (A \in ℝ \land B \in ℝ)$
65		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
66	64 65	syl	$⊢ (φ \land x \in [A, B]) \to (x \in [A, B] \leftrightarrow (x \in ℝ \land A \leq x \land x \leq B))$
67	59 66	mpbid	$⊢ (φ \land x \in [A, B]) \to (x \in ℝ \land A \leq x \land x \leq B)$
68	67	simp2d	$⊢ (φ \land x \in [A, B]) \to A \leq x$
69	68	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A \leq x$
70		df-ne	$⊢ x \neq A \leftrightarrow \neg x = A$
71	70	bilanri	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to x \neq A$
72	56 62 69 71	leneltd	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A < x$
73	72	adantr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A < x$
74		nesym	$⊢ B \neq x \leftrightarrow \neg x = B$
75	74	bilanri	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to B \neq x$
76	67	simp3d	$⊢ (φ \land x \in [A, B]) \to x \leq B$
77	61 58 76	3jca	$⊢ (φ \land x \in [A, B]) \to (x \in ℝ \land B \in ℝ \land x \leq B)$
78	77	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to (x \in ℝ \land B \in ℝ \land x \leq B)$
79		leltne	$⊢ (x \in ℝ \land B \in ℝ \land x \leq B) \to (x < B \leftrightarrow B \neq x)$
80	78 79	syl	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to (x < B \leftrightarrow B \neq x)$
81	75 80	mpbird	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x < B$
82	81	adantlr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x < B$
83	73 82	jca	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to (A < x \land x < B)$
84		elioo3g	$⊢ x \in (A, B) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ^{*}) \land (A < x \land x < B))$
85	55 83 84	sylanbrc	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in (A, B)$
86	48 85	jca	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to (φ \land x \in (A, B))$
87	7	ffvelcdmda	$⊢ (φ \land x \in (A, B)) \to F (x) \in ℂ$
88	23 87	eqeltrd	$⊢ (φ \land x \in (A, B)) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
89	86 88	syl	$⊢ (((φ \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 ℂ$
90	47 89	pm2.61dan	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
91	37 90	pm2.61dan	$⊢ (φ \land x \in [A, B]) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
92		nfv	$⊢ Ⅎ x φ$
93		eqid	$⊢ (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 (x))))$
94	92 93 1 2 3 4 5	cncfiooicc	$⊢ φ \to (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x)))) : [A, B] \underset{cn}{⟶} ℂ$
95		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x)))) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x)))) \in 𝐿^{1}$
96	1 2 94 95	syl3anc	$⊢ φ \to (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x)))) \in 𝐿^{1}$
97	28 30 91 96	iblss	$⊢ φ \to (x \in (A, B) ⟼ if (x = A, R, if (x = B, L, F (x)))) \in 𝐿^{1}$
98	26 97	eqeltrd	$⊢ φ \to F \in 𝐿^{1}$

Metamath Proof Explorer

Theorem iblcncfioo

Proof