Theorem iblempty

Description: The empty function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	iblempty	⊢ ∅ ∈ 𝐿1

Proof

Step	Hyp	Ref	Expression
1		mbf0	⊢ ∅ ∈ MblFn
2		fconstmpt	⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 )
3	2	eqcomi	⊢ ( 𝑥 ∈ ℝ ↦ 0 ) = ( ℝ × { 0 } )
4	3	fveq2i	⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ 0 ) ) = ( ∫2 ‘ ( ℝ × { 0 } ) )
5		itg20	⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) = 0
6	4 5	eqtri	⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ 0 ) ) = 0
7		0re	⊢ 0 ∈ ℝ
8	6 7	eqeltri	⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ 0 ) ) ∈ ℝ
9	8	rgenw	⊢ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ 0 ) ) ∈ ℝ
10		noel	⊢ ¬ 𝑥 ∈ ∅
11	10	intnanr	⊢ ¬ ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) )
12	11	iffalsei	⊢ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) = 0
13	12	eqcomi	⊢ 0 = if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 )
14	13	a1i	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 0 = if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) )
15	14	mpteq2dva	⊢ ( ⊤ → ( 𝑥 ∈ ℝ ↦ 0 ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
16		eqidd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ∅ ) → ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) )
17		dm0	⊢ dom ∅ = ∅
18	17	a1i	⊢ ( ⊤ → dom ∅ = ∅ )
19	10	intnan	⊢ ¬ ( ⊤ ∧ 𝑥 ∈ ∅ )
20	19	pm2.21i	⊢ ( ( ⊤ ∧ 𝑥 ∈ ∅ ) → ( ∅ ‘ 𝑥 ) = 0 )
21	15 16 18 20	isibl	⊢ ( ⊤ → ( ∅ ∈ 𝐿1 ↔ ( ∅ ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ 0 ) ) ∈ ℝ ) ) )
22	21	mptru	⊢ ( ∅ ∈ 𝐿1 ↔ ( ∅ ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ 0 ) ) ∈ ℝ ) )
23	1 9 22	mpbir2an	⊢ ∅ ∈ 𝐿1