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	syl5eq	⊢ ( 𝑘 ∈ ( 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