Metamath Proof Explorer

Theorem itgspliticc

Description: The S. integral splits on closed intervals with matching endpoints. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses itgspliticc.1 ⊢ φ → A ∈ ℝ
itgspliticc.2 ⊢ φ → C ∈ ℝ
itgspliticc.3 ⊢ φ → B ∈ A C
itgspliticc.4 ⊢ φ ∧ x ∈ A C → D ∈ V
itgspliticc.5 ⊢ φ → x ∈ A B ⟼ D ∈ 𝐿 1
itgspliticc.6 ⊢ φ → x ∈ B C ⟼ D ∈ 𝐿 1
Assertion itgspliticc ⊢ φ → ∫ A C D dx = ∫ A B D dx + ∫ B C D dx

Proof

Step Hyp Ref Expression
1 itgspliticc.1 ⊢ φ → A ∈ ℝ
2 itgspliticc.2 ⊢ φ → C ∈ ℝ
3 itgspliticc.3 ⊢ φ → B ∈ A C
4 itgspliticc.4 ⊢ φ ∧ x ∈ A C → D ∈ V
5 itgspliticc.5 ⊢ φ → x ∈ A B ⟼ D ∈ 𝐿 1
6 itgspliticc.6 ⊢ φ → x ∈ B C ⟼ D ∈ 𝐿 1
7 1 rexrd ⊢ φ → A ∈ ℝ *
8 elicc2 ⊢ A ∈ ℝ ∧ C ∈ ℝ → B ∈ A C ↔ B ∈ ℝ ∧ A ≤ B ∧ B ≤ C
9 1 2 8 syl2anc ⊢ φ → B ∈ A C ↔ B ∈ ℝ ∧ A ≤ B ∧ B ≤ C
10 3 9 mpbid ⊢ φ → B ∈ ℝ ∧ A ≤ B ∧ B ≤ C
11 10 simp1d ⊢ φ → B ∈ ℝ
12 11 rexrd ⊢ φ → B ∈ ℝ *
13 2 rexrd ⊢ φ → C ∈ ℝ *
14 df-icc ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x ≤ z ∧ z ≤ y
15 xrmaxle ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ z ∈ ℝ * → if A ≤ B B A ≤ z ↔ A ≤ z ∧ B ≤ z
16 xrlemin ⊢ z ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → z ≤ if B ≤ C B C ↔ z ≤ B ∧ z ≤ C
17 14 15 16 ixxin ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A B ∩ B C = if A ≤ B B A if B ≤ C B C
18 7 12 12 13 17 syl22anc ⊢ φ → A B ∩ B C = if A ≤ B B A if B ≤ C B C
19 10 simp2d ⊢ φ → A ≤ B
20 19 iftrued ⊢ φ → if A ≤ B B A = B
21 10 simp3d ⊢ φ → B ≤ C
22 21 iftrued ⊢ φ → if B ≤ C B C = B
23 20 22 oveq12d ⊢ φ → if A ≤ B B A if B ≤ C B C = B B
24 iccid ⊢ B ∈ ℝ * → B B = B
25 12 24 syl ⊢ φ → B B = B
26 18 23 25 3eqtrd ⊢ φ → A B ∩ B C = B
27 26 fveq2d ⊢ φ → vol * ⁡ A B ∩ B C = vol * ⁡ B
28 ovolsn ⊢ B ∈ ℝ → vol * ⁡ B = 0
29 11 28 syl ⊢ φ → vol * ⁡ B = 0
30 27 29 eqtrd ⊢ φ → vol * ⁡ A B ∩ B C = 0
31 iccsplit ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ B ∈ A C → A C = A B ∪ B C
32 1 2 3 31 syl3anc ⊢ φ → A C = A B ∪ B C
33 30 32 4 5 6 itgsplit ⊢ φ → ∫ A C D dx = ∫ A B D dx + ∫ B C D dx