This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } ) = ( 𝑥 ∈ ℝ ↦ 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