Theorem ibliooicc

Description: If a function is integrable on an open interval, it is integrable on the corresponding closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	ibliooicc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ibliooicc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ibliooicc.3	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 )
	ibliooicc.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ℂ )
Assertion	ibliooicc	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 )

Proof

Step	Hyp	Ref	Expression
1		ibliooicc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		ibliooicc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		ibliooicc.3	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 )
4		ibliooicc.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ℂ )
5		ioossicc	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
6	5	a1i	⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
7	1 2	iccssred	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
8	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
9	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
10		icc0	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
11	8 9 10	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
12	11	biimpar	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( 𝐴 [,] 𝐵 ) = ∅ )
13	12	difeq1d	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( ∅ ∖ ( 𝐴 (,) 𝐵 ) ) )
14		0dif	⊢ ( ∅ ∖ ( 𝐴 (,) 𝐵 ) ) = ∅
15		0ss	⊢ ∅ ⊆ { 𝐴 , 𝐵 }
16	14 15	eqsstri	⊢ ( ∅ ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 }
17	13 16	eqsstrdi	⊢ ( ( 𝜑 ∧ 𝐵 < 𝐴 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 } )
18		ssid	⊢ ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) )
19	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ℝ* )
20	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ℝ* )
21		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ 𝐵 )
22		iccdifioo	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) = { 𝐴 , 𝐵 } )
23	19 20 21 22	syl3anc	⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) = { 𝐴 , 𝐵 } )
24	18 23	sseqtrid	⊢ ( ( 𝜑 ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 } )
25	17 24 2 1	ltlecasei	⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 } )
26		prssi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → { 𝐴 , 𝐵 } ⊆ ℝ )
27	1 2 26	syl2anc	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ ℝ )
28		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
29		ovolfi	⊢ ( ( { 𝐴 , 𝐵 } ∈ Fin ∧ { 𝐴 , 𝐵 } ⊆ ℝ ) → ( vol* ‘ { 𝐴 , 𝐵 } ) = 0 )
30	28 27 29	sylancr	⊢ ( 𝜑 → ( vol* ‘ { 𝐴 , 𝐵 } ) = 0 )
31		ovolssnul	⊢ ( ( ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝐵 } ⊆ ℝ ∧ ( vol* ‘ { 𝐴 , 𝐵 } ) = 0 ) → ( vol* ‘ ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ) = 0 )
32	25 27 30 31	syl3anc	⊢ ( 𝜑 → ( vol* ‘ ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) ) = 0 )
33	6 7 32 4	itgss3	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 ) ∧ ∫ ( 𝐴 (,) 𝐵 ) 𝐶 d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) 𝐶 d 𝑥 ) )
34	33	simpld	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 ) )
35	3 34	mpbid	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐶 ) ∈ 𝐿1 )