Metamath Proof Explorer

Theorem itgz

Description: The integral of zero on any set is zero. (Contributed by Mario Carneiro, 29-Jun-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion itgz ∫ 𝐴 0 d 𝑥 = 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) )
2 1 dfitg ⊢ ∫ 𝐴 0 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
3 ax-icn ⊢ i ∈ ℂ
4 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℕ0 )
5 expcl ⊢ ( ( i ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( i ↑ 𝑘 ) ∈ ℂ )
6 3 4 5 sylancr ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( i ↑ 𝑘 ) ∈ ℂ )
7 ine0 ⊢ i ≠ 0
8 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
9 expne0i ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 )
10 3 7 8 9 mp3an12i ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( i ↑ 𝑘 ) ≠ 0 )
11 6 10 div0d ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( 0 / ( i ↑ 𝑘 ) ) = 0 )
12 11 fveq2d ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ 0 ) )
13 re0 ⊢ ( ℜ ‘ 0 ) = 0
14 12 13 eqtrdi ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) = 0 )
15 14 ifeq1d ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , 0 , 0 ) )
16 ifid ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , 0 , 0 ) = 0
17 15 16 eqtrdi ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) = 0 )
18 17 mpteq2dv ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ 0 ) )
19 fconstmpt ⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 )
20 18 19 eqtr4di ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( ℝ × { 0 } ) )
21 20 fveq2d ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( ℝ × { 0 } ) ) )
22 itg20 ⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) = 0
23 21 22 eqtrdi ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = 0 )
24 23 oveq2d ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · 0 ) )
25 6 mul01d ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ( i ↑ 𝑘 ) · 0 ) = 0 )
26 24 25 eqtrd ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = 0 )
27 26 sumeq2i ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 0 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) 0
28 fzfi ⊢ ( 0 ... 3 ) ∈ Fin
29 28 olci ⊢ ( ( 0 ... 3 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 3 ) ∈ Fin )
30 sumz ⊢ ( ( ( 0 ... 3 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 3 ) ∈ Fin ) → Σ 𝑘 ∈ ( 0 ... 3 ) 0 = 0 )
31 29 30 ax-mp ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) 0 = 0
32 2 27 31 3eqtri ⊢ ∫ 𝐴 0 d 𝑥 = 0