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

Metamath Proof Explorer

Theorem itgsplitioo

Description: The S. integral splits on open intervals with matching endpoints. (Contributed by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses itgsplitioo.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
itgsplitioo.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
itgsplitioo.3 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐶 ) )
itgsplitioo.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐶 ) ) → 𝐷 ∈ ℂ )
itgsplitioo.5 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 )
itgsplitioo.6 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝐷 ) ∈ 𝐿1 )
Assertion itgsplitioo ( 𝜑 → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 itgsplitioo.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 itgsplitioo.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3 itgsplitioo.3 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐶 ) )
4 itgsplitioo.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐶 ) ) → 𝐷 ∈ ℂ )
5 itgsplitioo.5 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 )
6 itgsplitioo.6 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝐷 ) ∈ 𝐿1 )
7 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
8 1 2 7 syl2anc ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) )
9 3 8 mpbid ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) )
10 9 simp2d ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
11 9 simp1d ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
12 1 11 leloed ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) ) )
13 10 12 mpbid ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ) )
14 13 ord ⊢ ( 𝜑 → ( ¬ 𝐴 < 𝐵 → 𝐴 = 𝐵 ) )
15 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
16 iooss1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝐴 (,) 𝐶 ) )
17 15 10 16 syl2anc ⊢ ( 𝜑 → ( 𝐵 (,) 𝐶 ) ⊆ ( 𝐴 (,) 𝐶 ) )
18 17 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐶 ) )
19 18 4 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ) → 𝐷 ∈ ℂ )
20 19 6 itgcl ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ∈ ℂ )
21 20 addlidd ⊢ ( 𝜑 → ( 0 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 )
22 21 eqcomd ⊢ ( 𝜑 → ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 = ( 0 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )
23 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐶 ) )
24 itgeq1 ⊢ ( ( 𝐴 (,) 𝐶 ) = ( 𝐵 (,) 𝐶 ) → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 )
25 23 24 syl ⊢ ( 𝐴 = 𝐵 → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 )
26 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,) 𝐵 ) = ( 𝐵 (,) 𝐵 ) )
27 iooid ⊢ ( 𝐵 (,) 𝐵 ) = ∅
28 26 27 eqtrdi ⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,) 𝐵 ) = ∅ )
29 itgeq1 ⊢ ( ( 𝐴 (,) 𝐵 ) = ∅ → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ∫ ∅ 𝐷 d 𝑥 )
30 28 29 syl ⊢ ( 𝐴 = 𝐵 → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ∫ ∅ 𝐷 d 𝑥 )
31 itg0 ⊢ ∫ ∅ 𝐷 d 𝑥 = 0
32 30 31 eqtrdi ⊢ ( 𝐴 = 𝐵 → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = 0 )
33 32 oveq1d ⊢ ( 𝐴 = 𝐵 → ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) = ( 0 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )
34 25 33 eqeq12d ⊢ ( 𝐴 = 𝐵 → ( ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) ↔ ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 = ( 0 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) ) )
35 22 34 syl5ibrcom ⊢ ( 𝜑 → ( 𝐴 = 𝐵 → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) ) )
36 14 35 syld ⊢ ( 𝜑 → ( ¬ 𝐴 < 𝐵 → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) ) )
37 9 simp3d ⊢ ( 𝜑 → 𝐵 ≤ 𝐶 )
38 11 2 leloed ⊢ ( 𝜑 → ( 𝐵 ≤ 𝐶 ↔ ( 𝐵 < 𝐶 ∨ 𝐵 = 𝐶 ) ) )
39 37 38 mpbid ⊢ ( 𝜑 → ( 𝐵 < 𝐶 ∨ 𝐵 = 𝐶 ) )
40 39 ord ⊢ ( 𝜑 → ( ¬ 𝐵 < 𝐶 → 𝐵 = 𝐶 ) )
41 2 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
42 iooss2 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐵 ≤ 𝐶 ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐶 ) )
43 41 37 42 syl2anc ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐶 ) )
44 43 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐶 ) )
45 44 4 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐷 ∈ ℂ )
46 45 5 itgcl ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 ∈ ℂ )
47 46 addridd ⊢ ( 𝜑 → ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + 0 ) = ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 )
48 47 eqcomd ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + 0 ) )
49 oveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐴 (,) 𝐵 ) = ( 𝐴 (,) 𝐶 ) )
50 itgeq1 ⊢ ( ( 𝐴 (,) 𝐵 ) = ( 𝐴 (,) 𝐶 ) → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 )
51 49 50 syl ⊢ ( 𝐵 = 𝐶 → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 )
52 oveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐵 (,) 𝐵 ) = ( 𝐵 (,) 𝐶 ) )
53 27 52 eqtr3id ⊢ ( 𝐵 = 𝐶 → ∅ = ( 𝐵 (,) 𝐶 ) )
54 itgeq1 ⊢ ( ∅ = ( 𝐵 (,) 𝐶 ) → ∫ ∅ 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 )
55 53 54 syl ⊢ ( 𝐵 = 𝐶 → ∫ ∅ 𝐷 d 𝑥 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 )
56 31 55 eqtr3id ⊢ ( 𝐵 = 𝐶 → 0 = ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 )
57 56 oveq2d ⊢ ( 𝐵 = 𝐶 → ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + 0 ) = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )
58 51 57 eqeq12d ⊢ ( 𝐵 = 𝐶 → ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + 0 ) ↔ ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) ) )
59 48 58 syl5ibcom ⊢ ( 𝜑 → ( 𝐵 = 𝐶 → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) ) )
60 40 59 syld ⊢ ( 𝜑 → ( ¬ 𝐵 < 𝐶 → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) ) )
61 indir ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∩ ( 𝐵 (,) 𝐶 ) ) = ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 (,) 𝐶 ) ) ∪ ( { 𝐵 } ∩ ( 𝐵 (,) 𝐶 ) ) )
62 11 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
63 15 62 jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
64 63 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
65 62 41 jca ⊢ ( 𝜑 → ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) )
66 65 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) )
67 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ∈ ℝ )
68 67 leidd ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ≤ 𝐵 )
69 ioodisj ⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ) ∧ 𝐵 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 (,) 𝐶 ) ) = ∅ )
70 64 66 68 69 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 (,) 𝐶 ) ) = ∅ )
71 incom ⊢ ( { 𝐵 } ∩ ( 𝐵 (,) 𝐶 ) ) = ( ( 𝐵 (,) 𝐶 ) ∩ { 𝐵 } )
72 67 ltnrd ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ¬ 𝐵 < 𝐵 )
73 eliooord ⊢ ( 𝐵 ∈ ( 𝐵 (,) 𝐶 ) → ( 𝐵 < 𝐵 ∧ 𝐵 < 𝐶 ) )
74 73 simpld ⊢ ( 𝐵 ∈ ( 𝐵 (,) 𝐶 ) → 𝐵 < 𝐵 )
75 72 74 nsyl ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ¬ 𝐵 ∈ ( 𝐵 (,) 𝐶 ) )
76 disjsn ⊢ ( ( ( 𝐵 (,) 𝐶 ) ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ ( 𝐵 (,) 𝐶 ) )
77 75 76 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐵 (,) 𝐶 ) ∩ { 𝐵 } ) = ∅ )
78 71 77 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( { 𝐵 } ∩ ( 𝐵 (,) 𝐶 ) ) = ∅ )
79 70 78 uneq12d ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 (,) 𝐶 ) ) ∪ ( { 𝐵 } ∩ ( 𝐵 (,) 𝐶 ) ) ) = ( ∅ ∪ ∅ ) )
80 un0 ⊢ ( ∅ ∪ ∅ ) = ∅
81 79 80 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 (,) 𝐶 ) ) ∪ ( { 𝐵 } ∩ ( 𝐵 (,) 𝐶 ) ) ) = ∅ )
82 61 81 eqtrid ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∩ ( 𝐵 (,) 𝐶 ) ) = ∅ )
83 82 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( vol* ‘ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∩ ( 𝐵 (,) 𝐶 ) ) ) = ( vol* ‘ ∅ ) )
84 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
85 83 84 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( vol* ‘ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∩ ( 𝐵 (,) 𝐶 ) ) ) = 0 )
86 15 62 41 3jca ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) )
87 ioojoin ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) )
88 86 87 sylan ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) )
89 88 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝐴 (,) 𝐶 ) = ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) 𝐶 ) ) )
90 4 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) ∧ 𝑥 ∈ ( 𝐴 (,) 𝐶 ) ) → 𝐷 ∈ ℂ )
91 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 )
92 ssun1 ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } )
93 92 a1i ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) )
94 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
95 94 a1i ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
96 67 snssd ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → { 𝐵 } ⊆ ℝ )
97 95 96 unssd ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ⊆ ℝ )
98 uncom ⊢ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( { 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) )
99 98 difeq1i ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( ( { 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) ∖ ( 𝐴 (,) 𝐵 ) )
100 difun2 ⊢ ( ( { 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( { 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) )
101 99 100 eqtri ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( { 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) )
102 difss ⊢ ( { 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐵 }
103 101 102 eqsstri ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐵 }
104 ovolsn ⊢ ( 𝐵 ∈ ℝ → ( vol* ‘ { 𝐵 } ) = 0 )
105 67 104 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( vol* ‘ { 𝐵 } ) = 0 )
106 ovolssnul ⊢ ( ( ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∖ ( 𝐴 (,) 𝐵 ) ) ⊆ { 𝐵 } ∧ { 𝐵 } ⊆ ℝ ∧ ( vol* ‘ { 𝐵 } ) = 0 ) → ( vol* ‘ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∖ ( 𝐴 (,) 𝐵 ) ) ) = 0 )
107 103 96 105 106 mp3an2i ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( vol* ‘ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∖ ( 𝐴 (,) 𝐵 ) ) ) = 0 )
108 ssun1 ⊢ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ⊆ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) 𝐶 ) )
109 108 88 sseqtrid ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ⊆ ( 𝐴 (,) 𝐶 ) )
110 109 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) ∧ 𝑥 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐶 ) )
111 110 90 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) ∧ 𝑥 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) → 𝐷 ∈ ℂ )
112 93 97 107 111 itgss3 ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ↦ 𝐷 ) ∈ 𝐿1 ) ∧ ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ∫ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) 𝐷 d 𝑥 ) )
113 112 simpld ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ 𝐷 ) ∈ 𝐿1 ↔ ( 𝑥 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ↦ 𝐷 ) ∈ 𝐿1 ) )
114 91 113 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝑥 ∈ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ↦ 𝐷 ) ∈ 𝐿1 )
115 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( 𝑥 ∈ ( 𝐵 (,) 𝐶 ) ↦ 𝐷 ) ∈ 𝐿1 )
116 85 89 90 114 115 itgsplit ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )
117 112 simprd ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 = ∫ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) 𝐷 d 𝑥 )
118 117 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) = ( ∫ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )
119 116 118 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )
120 119 ex ⊢ ( 𝜑 → ( ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) ) )
121 36 60 120 ecased ⊢ ( 𝜑 → ∫ ( 𝐴 (,) 𝐶 ) 𝐷 d 𝑥 = ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 d 𝑥 + ∫ ( 𝐵 (,) 𝐶 ) 𝐷 d 𝑥 ) )