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

Metamath Proof Explorer

Theorem itg0

Description: The integral of anything on the empty set is zero. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Assertion itg0 ∫ ∅ 𝐴 d 𝑥 = 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) )
2 1 dfitg ⊢ ∫ ∅ 𝐴 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
3 ifan ⊢ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ ∅ , if ( 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
4 noel ⊢ ¬ 𝑥 ∈ ∅
5 4 iffalsei ⊢ if ( 𝑥 ∈ ∅ , if ( 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0
6 3 5 eqtri ⊢ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) = 0
7 6 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ 0 )
8 fconstmpt ⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 )
9 7 8 eqtr4i ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( ℝ × { 0 } )
10 9 fveq2i ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( ℝ × { 0 } ) )
11 itg20 ⊢ ( ∫2 ‘ ( ℝ × { 0 } ) ) = 0
12 10 11 eqtri ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = 0
13 12 oveq2i ⊢ ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · 0 )
14 ax-icn ⊢ i ∈ ℂ
15 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℕ0 )
16 expcl ⊢ ( ( i ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( i ↑ 𝑘 ) ∈ ℂ )
17 14 15 16 sylancr ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( i ↑ 𝑘 ) ∈ ℂ )
18 17 mul01d ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ( i ↑ 𝑘 ) · 0 ) = 0 )
19 13 18 eqtrid ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = 0 )
20 19 sumeq2i ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) 0
21 fzfi ⊢ ( 0 ... 3 ) ∈ Fin
22 21 olci ⊢ ( ( 0 ... 3 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 3 ) ∈ Fin )
23 sumz ⊢ ( ( ( 0 ... 3 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 3 ) ∈ Fin ) → Σ 𝑘 ∈ ( 0 ... 3 ) 0 = 0 )
24 22 23 ax-mp ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) 0 = 0
25 20 24 eqtri ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ∅ ∧ 0 ≤ ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐴 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = 0
26 2 25 eqtri ⊢ ∫ ∅ 𝐴 d 𝑥 = 0