Metamath Proof Explorer

Theorem ibl0

Description: The zero function is integrable on any measurable set. (Unlike iblconst , this does not require A to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion ibl0 ( 𝐴 ∈ dom vol → ( 𝐴 × { 0 } ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 mbfconst ⊢ ( ( 𝐴 ∈ dom vol ∧ 0 ∈ ℂ ) → ( 𝐴 × { 0 } ) ∈ MblFn )
3 1 2 mpan2 ⊢ ( 𝐴 ∈ dom vol → ( 𝐴 × { 0 } ) ∈ MblFn )
4 ax-icn ⊢ i ∈ ℂ
5 ine0 ⊢ i ≠ 0
6 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
7 6 ad2antlr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑘 ∈ ℤ )
8 expclz ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ∈ ℂ )
9 expne0i ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 )
10 8 9 div0d ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( 0 / ( i ↑ 𝑘 ) ) = 0 )
11 4 5 7 10 mp3an12i ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 0 / ( i ↑ 𝑘 ) ) = 0 )
12 11 fveq2d ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ 0 ) )
13 re0 ⊢ ( ℜ ‘ 0 ) = 0
14 12 13 eqtrdi ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) = 0 )
15 14 itgvallem3 ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = 0 )
16 0re ⊢ 0 ∈ ℝ
17 15 16 eqeltrdi ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
18 17 ralrimiva ⊢ ( 𝐴 ∈ dom vol → ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
19 eqidd ⊢ ( 𝐴 ∈ dom vol → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
20 eqidd ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) )
21 c0ex ⊢ 0 ∈ V
22 21 fconst ⊢ ( 𝐴 × { 0 } ) : 𝐴 ⟶ { 0 }
23 fdm ⊢ ( ( 𝐴 × { 0 } ) : 𝐴 ⟶ { 0 } → dom ( 𝐴 × { 0 } ) = 𝐴 )
24 22 23 mp1i ⊢ ( 𝐴 ∈ dom vol → dom ( 𝐴 × { 0 } ) = 𝐴 )
25 21 fvconst2 ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
26 25 adantl ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
27 19 20 24 26 isibl ⊢ ( 𝐴 ∈ dom vol → ( ( 𝐴 × { 0 } ) ∈ 𝐿1 ↔ ( ( 𝐴 × { 0 } ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
28 3 18 27 mpbir2and ⊢ ( 𝐴 ∈ dom vol → ( 𝐴 × { 0 } ) ∈ 𝐿1 )