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	sseldi	$⊢ φ \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	sseldi	$⊢ φ \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	biimpri	$⊢ \neg x = A \to x \neq A$
72	71	adantl	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to x \neq A$
73	56 62 69 72	leneltd	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to A < x$
74	73	adantr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to A < x$
75		nesym	$⊢ B \neq x \leftrightarrow \neg x = B$
76	75	biimpri	$⊢ \neg x = B \to B \neq x$
77	76	adantl	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to B \neq x$
78	67	simp3d	$⊢ (φ \land x \in [A, B]) \to x \leq B$
79	61 58 78	3jca	$⊢ (φ \land x \in [A, B]) \to (x \in ℝ \land B \in ℝ \land x \leq B)$
80	79	adantr	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to (x \in ℝ \land B \in ℝ \land x \leq B)$
81		leltne	$⊢ (x \in ℝ \land B \in ℝ \land x \leq B) \to (x < B \leftrightarrow B \neq x)$
82	80 81	syl	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to (x < B \leftrightarrow B \neq x)$
83	77 82	mpbird	$⊢ ((φ \land x \in [A, B]) \land \neg x = B) \to x < B$
84	83	adantlr	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x < B$
85	74 84	jca	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to (A < x \land x < B)$
86		elioo3g	$⊢ x \in (A, B) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land x \in ℝ^{*}) \land (A < x \land x < B))$
87	55 85 86	sylanbrc	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to x \in (A, B)$
88	48 87	jca	$⊢ (((φ \land x \in [A, B]) \land \neg x = A) \land \neg x = B) \to (φ \land x \in (A, B))$
89	7	ffvelrnda	$⊢ (φ \land x \in (A, B)) \to F (x) \in ℂ$
90	23 89	eqeltrd	$⊢ (φ \land x \in (A, B)) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
91	88 90	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 ℂ$
92	47 91	pm2.61dan	$⊢ ((φ \land x \in [A, B]) \land \neg x = A) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
93	37 92	pm2.61dan	$⊢ (φ \land x \in [A, B]) \to if (x = A, R, if (x = B, L, F (x))) \in ℂ$
94		nfv	$⊢ Ⅎ x φ$
95		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))))$
96	94 95 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}{⟶} ℂ$
97		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}$
98	1 2 96 97	syl3anc	$⊢ φ \to (x \in [A, B] ⟼ if (x = A, R, if (x = B, L, F (x)))) \in 𝐿^{1}$
99	28 30 93 98	iblss	$⊢ φ \to (x \in (A, B) ⟼ if (x = A, R, if (x = B, L, F (x)))) \in 𝐿^{1}$
100	26 99	eqeltrd	$⊢ φ \to F \in 𝐿^{1}$

Metamath Proof Explorer

Theorem iblcncfioo

Proof