Metamath Proof Explorer

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 = x ∈ ℝ ⟼ 0
3 2 eqcomi ⊢ x ∈ ℝ ⟼ 0 = ℝ × 0
4 3 fveq2i ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ 0 = ∫ 2 ⁡ ℝ × 0
5 itg20 ⊢ ∫ 2 ⁡ ℝ × 0 = 0
6 4 5 eqtri ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ 0 = 0
7 0re ⊢ 0 ∈ ℝ
8 6 7 eqeltri ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ 0 ∈ ℝ
9 8 rgenw ⊢ ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ 0 ∈ ℝ
10 noel ⊢ ¬ x ∈ ∅
11 10 intnanr ⊢ ¬ x ∈ ∅ ∧ 0 ≤ ℜ ⁡ 0 i k
12 11 iffalsei ⊢ if x ∈ ∅ ∧ 0 ≤ ℜ ⁡ 0 i k ℜ ⁡ 0 i k 0 = 0
13 12 eqcomi ⊢ 0 = if x ∈ ∅ ∧ 0 ≤ ℜ ⁡ 0 i k ℜ ⁡ 0 i k 0
14 13 a1i ⊢ ⊤ ∧ x ∈ ℝ → 0 = if x ∈ ∅ ∧ 0 ≤ ℜ ⁡ 0 i k ℜ ⁡ 0 i k 0
15 14 mpteq2dva ⊢ ⊤ → x ∈ ℝ ⟼ 0 = x ∈ ℝ ⟼ if x ∈ ∅ ∧ 0 ≤ ℜ ⁡ 0 i k ℜ ⁡ 0 i k 0
16 eqidd ⊢ ⊤ ∧ x ∈ ∅ → ℜ ⁡ 0 i k = ℜ ⁡ 0 i k
17 dm0 ⊢ dom ⁡ ∅ = ∅
18 17 a1i ⊢ ⊤ → dom ⁡ ∅ = ∅
19 10 intnan ⊢ ¬ ⊤ ∧ x ∈ ∅
20 19 pm2.21i ⊢ ⊤ ∧ x ∈ ∅ → ∅ ⁡ x = 0
21 15 16 18 20 isibl ⊢ ⊤ → ∅ ∈ 𝐿 1 ↔ ∅ ∈ MblFn ∧ ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ 0 ∈ ℝ
22 21 mptru ⊢ ∅ ∈ 𝐿 1 ↔ ∅ ∈ MblFn ∧ ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ 0 ∈ ℝ
23 1 9 22 mpbir2an ⊢ ∅ ∈ 𝐿 1