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

Metamath Proof Explorer

Theorem itgsplit

Description: The S. integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itgsplit.i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = 0 )
itgsplit.u ⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
itgsplit.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ 𝑉 )
itgsplit.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
itgsplit.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 )
Assertion itgsplit ( 𝜑 → ∫ 𝑈 𝐶 d 𝑥 = ( ∫ 𝐴 𝐶 d 𝑥 + ∫ 𝐵 𝐶 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 itgsplit.i ⊢ ( 𝜑 → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = 0 )
2 itgsplit.u ⊢ ( 𝜑 → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
3 itgsplit.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ 𝑉 )
4 itgsplit.a ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5 itgsplit.b ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 )
6 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
7 4 6 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
8 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
9 8 2 sseqtrrid ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
10 9 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑈 )
11 10 3 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
12 7 11 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝐴 ∈ dom vol )
14 iblmbf ⊢ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn )
15 5 14 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn )
16 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
17 16 2 sseqtrrid ⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
18 17 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝑈 )
19 18 3 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
20 15 19 mbfdm2 ⊢ ( 𝜑 → 𝐵 ∈ dom vol )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝐵 ∈ dom vol )
22 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( vol* ‘ ( 𝐴 ∩ 𝐵 ) ) = 0 )
23 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝑈 = ( 𝐴 ∪ 𝐵 ) )
24 2 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 ↔ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ) )
25 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
26 24 25 bitrdi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ) )
27 26 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
28 7 11 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
29 15 19 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
30 28 29 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ) → 𝐶 ∈ ℂ )
31 27 30 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
32 31 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ℂ )
33 ax-icn ⊢ i ∈ ℂ
34 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℕ0 )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝑘 ∈ ℕ0 )
36 expcl ⊢ ( ( i ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( i ↑ 𝑘 ) ∈ ℂ )
37 33 35 36 sylancr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( i ↑ 𝑘 ) ∈ ℂ )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝑈 ) → ( i ↑ 𝑘 ) ∈ ℂ )
39 ine0 ⊢ i ≠ 0
40 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝑘 ∈ ℤ )
42 expne0i ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 )
43 33 39 41 42 mp3an12i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( i ↑ 𝑘 ) ≠ 0 )
44 43 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝑈 ) → ( i ↑ 𝑘 ) ≠ 0 )
45 32 38 44 divcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝐶 / ( i ↑ 𝑘 ) ) ∈ ℂ )
46 45 recld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝑈 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ∈ ℝ )
47 0re ⊢ 0 ∈ ℝ
48 ifcl ⊢ ( ( ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
49 46 47 48 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝑈 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
50 49 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝑈 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* )
51 max1 ⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
52 47 46 51 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝑈 ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
53 elxrge0 ⊢ ( if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) ↔ ( if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* ∧ 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
54 50 52 53 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝑈 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
55 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
56 55 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) )
57 ifan ⊢ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
58 57 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) )
59 ifan ⊢ if ( ( 𝑥 ∈ 𝑈 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝑈 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
60 59 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝑈 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑈 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) )
61 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
62 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) )
63 61 62 4 11 iblitg ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
64 40 63 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
65 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
66 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) )
67 65 66 5 19 iblitg ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
68 40 67 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
69 13 21 22 23 54 56 58 60 64 68 itg2split ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝑈 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
70 69 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝑈 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ) )
71 63 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℂ )
72 40 71 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℂ )
73 68 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℂ )
74 37 72 73 adddid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( i ↑ 𝑘 ) · ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ) = ( ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) + ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ) )
75 70 74 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝑈 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) + ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ) )
76 75 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝑈 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) + ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ) )
77 fzfid ⊢ ( 𝜑 → ( 0 ... 3 ) ∈ Fin )
78 37 72 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ∈ ℂ )
79 37 73 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ∈ ℂ )
80 77 78 79 fsumadd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) + ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) + Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ) )
81 76 80 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝑈 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) + Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) ) )
82 eqid ⊢ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) )
83 82 dfitg ⊢ ∫ 𝑈 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝑈 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
84 82 dfitg ⊢ ∫ 𝐴 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
85 82 dfitg ⊢ ∫ 𝐵 𝐶 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
86 84 85 oveq12i ⊢ ( ∫ 𝐴 𝐶 d 𝑥 + ∫ 𝐵 𝐶 d 𝑥 ) = ( Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) + Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) )
87 81 83 86 3eqtr4g ⊢ ( 𝜑 → ∫ 𝑈 𝐶 d 𝑥 = ( ∫ 𝐴 𝐶 d 𝑥 + ∫ 𝐵 𝐶 d 𝑥 ) )