itgsplit - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > itgsplit		Structured version Visualization version GIF version

Theorem itgsplit 26136

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

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

**Assertion**
Ref	Expression
itgsplit	⊢ (𝜑 → ∫𝑈𝐶 d𝑥 = (∫𝐴𝐶 d𝑥 + ∫𝐵𝐶 d𝑥))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵 𝜑,𝑥 𝑥,𝑈 𝑥,𝑉 Allowed substitution hint: 𝐶(𝑥)

Proof of Theorem itgsplit Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		itgsplit.a	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹)
2		iblmbf 26068	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝐿¹ → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
3	1, 2	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ MblFn)
4		ssun1 4124	. . . . . . . . . . . 12 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
5		itgsplit.u	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = (𝐴 ∪ 𝐵))
6	4, 5	sseqtrrid 3974	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ 𝑈)
7	6	sselda 3931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑈)
8		itgsplit.c	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ 𝑉)
9	7, 8	syldan 603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉)
10	3, 9	mbfdm2 25938	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ dom vol)
11	10	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝐴 ∈ dom vol)
12		itgsplit.b	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿¹)
13		iblmbf 26068	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐵 ↦ 𝐶) ∈ 𝐿¹ → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn)
14	12, 13	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ MblFn)
15		ssun2 4125	. . . . . . . . . . . 12 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
16	15, 5	sseqtrrid 3974	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ⊆ 𝑈)
17	16	sselda 3931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝑈)
18	17, 8	syldan 603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ 𝑉)
19	14, 18	mbfdm2 25938	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ dom vol)
20	19	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝐵 ∈ dom vol)
21		itgsplit.i	. . . . . . . 8 ⊢ (𝜑 → (vol*‘(𝐴 ∩ 𝐵)) = 0)
22	21	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (vol*‘(𝐴 ∩ 𝐵)) = 0)
23	5	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝑈 = (𝐴 ∪ 𝐵))
24	5	eleq2d 2847	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑥 ∈ 𝑈 ↔ 𝑥 ∈ (𝐴 ∪ 𝐵)))
25		elun 4100	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
26	24, 25	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑥 ∈ 𝑈 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
27	26	biimpa 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
28	3, 9	mbfmptcl 25937	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ)
29	14, 18	mbfmptcl 25937	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ)
30	28, 29	jaodan 972	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) → 𝐶 ∈ ℂ)
31	27, 30	syldan 603	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ)
32	31	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → 𝐶 ∈ ℂ)
33		ax-icn 11240	. . . . . . . . . . . . . 14 ⊢ i ∈ ℂ
34		elfznn0 13734	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...3) → 𝑘 ∈ ℕ₀)
35	34	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝑘 ∈ ℕ₀)
36		expcl 14202	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (i↑𝑘) ∈ ℂ)
37	33, 35, 36	sylancr 599	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (i↑𝑘) ∈ ℂ)
38	37	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (i↑𝑘) ∈ ℂ)
39		ine0 11732	. . . . . . . . . . . . . 14 ⊢ i ≠ 0
40		elfzelz 13637	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...3) → 𝑘 ∈ ℤ)
41	40	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → 𝑘 ∈ ℤ)
42		expne0i 14217	. . . . . . . . . . . . . 14 ⊢ ((i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ) → (i↑𝑘) ≠ 0)
43	33, 39, 41, 42	mp3an12i 1494	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (i↑𝑘) ≠ 0)
44	43	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (i↑𝑘) ≠ 0)
45	32, 38, 44	divcld 12074	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (𝐶 / (i↑𝑘)) ∈ ℂ)
46	45	recld 15341	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → (ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ)
47		0re 11291	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
48		ifcl 4528	. . . . . . . . . 10 ⊢ (((ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ ℝ)
49	46, 47, 48	sylancl 598	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ ℝ)
50	49	rexrd 11340	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ ℝ^*)
51		max1 13296	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ (ℜ‘(𝐶 / (i↑𝑘))) ∈ ℝ) → 0 ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
52	47, 46, 51	sylancr 599	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → 0 ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0))
53		elxrge0 13569	. . . . . . . 8 ⊢ (if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ (0[,]+∞) ↔ (if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ ℝ^* ∧ 0 ≤ if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
54	50, 52, 53	sylanbrc 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...3)) ∧ 𝑥 ∈ 𝑈) → if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0) ∈ (0[,]+∞))
55		ifan 4536	. . . . . . . 8 ⊢ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)
56	55	mpteq2i 5201	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐴, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))
57		ifan 4536	. . . . . . . 8 ⊢ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)
58	57	mpteq2i 5201	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐵, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))
59		ifan 4536	. . . . . . . 8 ⊢ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0) = if(𝑥 ∈ 𝑈, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0)
60	59	mpteq2i 5201	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑈, if(0 ≤ (ℜ‘(𝐶 / (i↑𝑘))), (ℜ‘(𝐶 / (i↑𝑘))), 0), 0))
61		eqidd 2762	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
62		eqidd 2762	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘))))
63	61, 62, 1, 9	iblitg 26069	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)
64	40, 63	sylan2 605	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)
65		eqidd 2762	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))
66		eqidd 2762	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘))))
67	65, 66, 12, 18	iblitg 26069	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)
68	40, 67	sylan2 605	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℝ)
69	11, 20, 22, 23, 54, 56, 58, 60, 64, 68	itg2split 26050	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))))
70	69	oveq2d 7428	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) = ((i↑𝑘) · ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))))
71	63	recnd 11318	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ℤ) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℂ)
72	40, 71	sylan2 605	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℂ)
73	68	recnd 11318	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) ∈ ℂ)
74	37, 72, 73	adddid 11314	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((i↑𝑘) · ((∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))) = (((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) + ((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))))
75	70, 74	eqtrd 2796	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) = (((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) + ((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))))
76	75	sumeq2dv 15849	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) = Σ𝑘 ∈ (0...3)(((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) + ((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))))
77		fzfid 14096	. . . 4 ⊢ (𝜑 → (0...3) ∈ Fin)
78	37, 72	mulcld 11310	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) ∈ ℂ)
79	37, 73	mulcld 11310	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...3)) → ((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) ∈ ℂ)
80	77, 78, 79	fsumadd 15886	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ (0...3)(((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) + ((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))) = (Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) + Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))))
81	76, 80	eqtrd 2796	. 2 ⊢ (𝜑 → Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) = (Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) + Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))))
82		eqid 2761	. . 3 ⊢ (ℜ‘(𝐶 / (i↑𝑘))) = (ℜ‘(𝐶 / (i↑𝑘)))
83	82	dfitg 26070	. 2 ⊢ ∫𝑈𝐶 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝑈 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))
84	82	dfitg 26070	. . 3 ⊢ ∫𝐴𝐶 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))
85	82	dfitg 26070	. . 3 ⊢ ∫𝐵𝐶 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0))))
86	84, 85	oveq12i 7424	. 2 ⊢ (∫𝐴𝐶 d𝑥 + ∫𝐵𝐶 d𝑥) = (Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))) + Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫₂‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐵 ∧ 0 ≤ (ℜ‘(𝐶 / (i↑𝑘)))), (ℜ‘(𝐶 / (i↑𝑘))), 0)))))
87	81, 83, 86	3eqtr4g 2821	1 ⊢ (𝜑 → ∫𝑈𝐶 d𝑥 = (∫𝐴𝐶 d𝑥 + ∫𝐵𝐶 d𝑥))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∪ cun 3897 ∩ cin 3898 ifcif 4482 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5651 ‘cfv 6531 (class class class)co 7412 ℂcc 11179 ℝcr 11180 0cc0 11181 ici 11183 + caddc 11184 · cmul 11186 +∞cpnf 11321 ℝ^*cxr 11323 ≤ cle 11325 / cdiv 11954 3c3 12379 ℕ₀cn0 12587 ℤcz 12674 [,]cicc 13460 ...cfz 13620 ↑cexp 14184 ℜcre 15244 Σcsu 15833 vol*covol 25763 volcvol 25764 MblFncmbf 25915 ∫₂citg2 25917 𝐿¹cibl 25918 ∫citg 25919

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-inf2 9626 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259 ax-addf 11260

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-disj 5071 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7682 df-ofr 7683 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-2o 8461 df-er 8701 df-map 8833 df-pm 8834 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-fi 9387 df-sup 9418 df-inf 9419 df-oi 9488 df-dju 9963 df-card 10001 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-4 12388 df-n0 12588 df-z 12675 df-uz 12947 df-q 13057 df-rp 13102 df-xneg 13222 df-xadd 13223 df-xmul 13224 df-ioo 13461 df-ico 13463 df-icc 13464 df-fz 13621 df-fzo 13769 df-fl 13912 df-mod 13990 df-seq 14125 df-exp 14185 df-hash 14455 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-clim 15635 df-sum 15834 df-rest 17573 df-topgen 17594 df-psmet 21650 df-xmet 21651 df-met 21652 df-bl 21653 df-mopn 21654 df-top 23192 df-topon 23209 df-bases 23244 df-cmp 23685 df-ovol 25765 df-vol 25766 df-mbf 25920 df-itg1 25921 df-itg2 25922 df-ibl 25923 df-itg 25924

This theorem is used by: itgspliticc 26137 itgsplitioo 26138

W3C validator