Metamath Proof Explorer

Theorem itgss

Description: Expand the set of an integral by adding zeroes outside the domain. (Contributed by Mario Carneiro, 11-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses itgss.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
itgss.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
Assertion itgss ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgss.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2 itgss.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
3 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
4 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0 )
5 4 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0 )
6 eldif ⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) )
7 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
8 7 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝐶 / ( i ↑ 𝑘 ) ) = ( 0 / ( i ↑ 𝑘 ) ) )
9 ax-icn ⊢ i ∈ ℂ
10 ine0 ⊢ i ≠ 0
11 expclz ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ∈ ℂ )
12 9 10 11 mp3an12 ⊢ ( 𝑘 ∈ ℤ → ( i ↑ 𝑘 ) ∈ ℂ )
13 expne0i ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 )
14 9 10 13 mp3an12 ⊢ ( 𝑘 ∈ ℤ → ( i ↑ 𝑘 ) ≠ 0 )
15 12 14 div0d ⊢ ( 𝑘 ∈ ℤ → ( 0 / ( i ↑ 𝑘 ) ) = 0 )
16 15 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 0 / ( i ↑ 𝑘 ) ) = 0 )
17 8 16 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( 𝐶 / ( i ↑ 𝑘 ) ) = 0 )
18 17 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ 0 ) )
19 re0 ⊢ ( ℜ ‘ 0 ) = 0
20 18 19 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = 0 )
21 20 ifeq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 , 0 ) )
22 ifid ⊢ if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 , 0 ) = 0
23 21 22 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = 0 )
24 6 23 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = 0 )
25 5 24 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
26 25 expr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
27 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
28 26 27 pm2.61d2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
29 iftrue ⊢ ( 𝑥 ∈ 𝐵 → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
30 29 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
31 28 30 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) )
32 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝐴 ⊆ 𝐵 )
33 32 sseld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
34 33 con3dimp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ¬ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ 𝐴 )
35 34 4 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ¬ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0 )
36 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐵 → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0 )
37 36 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ¬ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0 )
38 35 37 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ ¬ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) )
39 31 38 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) )
40 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
41 ifan ⊢ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
42 39 40 41 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
43 42 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
44 43 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
45 44 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
46 3 45 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
47 46 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
48 eqid ⊢ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) )
49 48 dfitg ⊢ ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
50 48 dfitg ⊢ ∫ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
51 47 49 50 3eqtr4g ⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐵 𝐶 d 𝑥 )