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 addid2d ( 𝜑 → ( 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 addid1d ( 𝜑 → ( ∫ ( 𝐴 (,) 𝐵 ) 𝐷 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 syl5eq ( ( 𝜑 ∧ ( 𝐴 < 𝐵𝐵 < 𝐶 ) ) → ( { 𝐵 } ∩ ( 𝐵 (,) 𝐶 ) ) = ∅ )
79 70 78 uneq12d ( ( 𝜑 ∧ ( 𝐴 < 𝐵𝐵 < 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 (,) 𝐶 ) ) ∪ ( { 𝐵 } ∩ ( 𝐵 (,) 𝐶 ) ) ) = ( ∅ ∪ ∅ ) )
80 un0 ( ∅ ∪ ∅ ) = ∅
81 79 80 eqtrdi ( ( 𝜑 ∧ ( 𝐴 < 𝐵𝐵 < 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 (,) 𝐶 ) ) ∪ ( { 𝐵 } ∩ ( 𝐵 (,) 𝐶 ) ) ) = ∅ )
82 61 81 syl5eq ( ( 𝜑 ∧ ( 𝐴 < 𝐵𝐵 < 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∩ ( 𝐵 (,) 𝐶 ) ) = ∅ )
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 𝑥 ) )