# Metamath Proof Explorer

## Theorem ditgsplit

Description: This theorem is the raison d'être for the directed integral, because unlike itgspliticc , there is no constraint on the ordering of the points A , B , C in the domain. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Hypotheses ditgsplit.x ${⊢}{\phi }\to {X}\in ℝ$
ditgsplit.y ${⊢}{\phi }\to {Y}\in ℝ$
ditgsplit.a ${⊢}{\phi }\to {A}\in \left[{X},{Y}\right]$
ditgsplit.b ${⊢}{\phi }\to {B}\in \left[{X},{Y}\right]$
ditgsplit.c ${⊢}{\phi }\to {C}\in \left[{X},{Y}\right]$
ditgsplit.d ${⊢}\left({\phi }\wedge {x}\in \left({X},{Y}\right)\right)\to {D}\in {V}$
ditgsplit.i ${⊢}{\phi }\to \left({x}\in \left({X},{Y}\right)⟼{D}\right)\in {𝐿}^{1}$
Assertion ditgsplit ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$

### Proof

Step Hyp Ref Expression
1 ditgsplit.x ${⊢}{\phi }\to {X}\in ℝ$
2 ditgsplit.y ${⊢}{\phi }\to {Y}\in ℝ$
3 ditgsplit.a ${⊢}{\phi }\to {A}\in \left[{X},{Y}\right]$
4 ditgsplit.b ${⊢}{\phi }\to {B}\in \left[{X},{Y}\right]$
5 ditgsplit.c ${⊢}{\phi }\to {C}\in \left[{X},{Y}\right]$
6 ditgsplit.d ${⊢}\left({\phi }\wedge {x}\in \left({X},{Y}\right)\right)\to {D}\in {V}$
7 ditgsplit.i ${⊢}{\phi }\to \left({x}\in \left({X},{Y}\right)⟼{D}\right)\in {𝐿}^{1}$
8 elicc2 ${⊢}\left({X}\in ℝ\wedge {Y}\in ℝ\right)\to \left({A}\in \left[{X},{Y}\right]↔\left({A}\in ℝ\wedge {X}\le {A}\wedge {A}\le {Y}\right)\right)$
9 1 2 8 syl2anc ${⊢}{\phi }\to \left({A}\in \left[{X},{Y}\right]↔\left({A}\in ℝ\wedge {X}\le {A}\wedge {A}\le {Y}\right)\right)$
10 3 9 mpbid ${⊢}{\phi }\to \left({A}\in ℝ\wedge {X}\le {A}\wedge {A}\le {Y}\right)$
11 10 simp1d ${⊢}{\phi }\to {A}\in ℝ$
12 elicc2 ${⊢}\left({X}\in ℝ\wedge {Y}\in ℝ\right)\to \left({B}\in \left[{X},{Y}\right]↔\left({B}\in ℝ\wedge {X}\le {B}\wedge {B}\le {Y}\right)\right)$
13 1 2 12 syl2anc ${⊢}{\phi }\to \left({B}\in \left[{X},{Y}\right]↔\left({B}\in ℝ\wedge {X}\le {B}\wedge {B}\le {Y}\right)\right)$
14 4 13 mpbid ${⊢}{\phi }\to \left({B}\in ℝ\wedge {X}\le {B}\wedge {B}\le {Y}\right)$
15 14 simp1d ${⊢}{\phi }\to {B}\in ℝ$
16 11 adantr ${⊢}\left({\phi }\wedge {A}\le {B}\right)\to {A}\in ℝ$
17 elicc2 ${⊢}\left({X}\in ℝ\wedge {Y}\in ℝ\right)\to \left({C}\in \left[{X},{Y}\right]↔\left({C}\in ℝ\wedge {X}\le {C}\wedge {C}\le {Y}\right)\right)$
18 1 2 17 syl2anc ${⊢}{\phi }\to \left({C}\in \left[{X},{Y}\right]↔\left({C}\in ℝ\wedge {X}\le {C}\wedge {C}\le {Y}\right)\right)$
19 5 18 mpbid ${⊢}{\phi }\to \left({C}\in ℝ\wedge {X}\le {C}\wedge {C}\le {Y}\right)$
20 19 simp1d ${⊢}{\phi }\to {C}\in ℝ$
21 20 adantr ${⊢}\left({\phi }\wedge {A}\le {B}\right)\to {C}\in ℝ$
22 15 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {A}\le {C}\right)\to {B}\in ℝ$
23 20 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {A}\le {C}\right)\to {C}\in ℝ$
24 biid ${⊢}\left({A}\le {B}\wedge {B}\le {C}\right)↔\left({A}\le {B}\wedge {B}\le {C}\right)$
25 1 2 3 4 5 6 7 24 ditgsplitlem ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {B}\le {C}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
26 25 adantlr ${⊢}\left(\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {A}\le {C}\right)\wedge {B}\le {C}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
27 biid ${⊢}\left({A}\le {C}\wedge {C}\le {B}\right)↔\left({A}\le {C}\wedge {C}\le {B}\right)$
28 1 2 3 5 4 6 7 27 ditgsplitlem ${⊢}\left(\left({\phi }\wedge {A}\le {C}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}$
29 28 oveq1d ${⊢}\left(\left({\phi }\wedge {A}\le {C}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
30 1 2 3 5 6 7 ditgcl ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}\in ℂ$
31 1 2 5 4 6 7 ditgcl ${⊢}{\phi }\to {\int }_{{C}}^{{B}}{D}d{x}\in ℂ$
32 1 2 4 5 6 7 ditgcl ${⊢}{\phi }\to {\int }_{{B}}^{{C}}{D}d{x}\in ℂ$
33 30 31 32 addassd ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
34 1 2 5 4 6 7 ditgswap ${⊢}{\phi }\to {\int }_{{B}}^{{C}}{D}d{x}=-{\int }_{{C}}^{{B}}{D}d{x}$
35 34 oveq2d ${⊢}{\phi }\to {\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{C}}^{{B}}{D}d{x}+\left(-{\int }_{{C}}^{{B}}{D}d{x}\right)$
36 31 negidd ${⊢}{\phi }\to {\int }_{{C}}^{{B}}{D}d{x}+\left(-{\int }_{{C}}^{{B}}{D}d{x}\right)=0$
37 35 36 eqtrd ${⊢}{\phi }\to {\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}=0$
38 37 oveq2d ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}+0$
39 30 addid1d ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}+0={\int }_{{A}}^{{C}}{D}d{x}$
40 33 38 39 3eqtrd ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}$
41 40 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\le {C}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}$
42 29 41 eqtr2d ${⊢}\left(\left({\phi }\wedge {A}\le {C}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
43 42 adantllr ${⊢}\left(\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {A}\le {C}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
44 22 23 26 43 lecasei ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {A}\le {C}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
45 40 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {C}\le {A}\right)\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}$
46 ancom ${⊢}\left({A}\le {B}\wedge {C}\le {A}\right)↔\left({C}\le {A}\wedge {A}\le {B}\right)$
47 1 2 5 3 4 6 7 46 ditgsplitlem ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {C}\le {A}\right)\to {\int }_{{C}}^{{B}}{D}d{x}={\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}$
48 47 oveq2d ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {C}\le {A}\right)\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}$
49 1 2 3 5 6 7 ditgswap ${⊢}{\phi }\to {\int }_{{C}}^{{A}}{D}d{x}=-{\int }_{{A}}^{{C}}{D}d{x}$
50 49 oveq2d ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}+\left(-{\int }_{{A}}^{{C}}{D}d{x}\right)$
51 30 negidd ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}+\left(-{\int }_{{A}}^{{C}}{D}d{x}\right)=0$
52 50 51 eqtrd ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}=0$
53 52 oveq1d ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}=0+{\int }_{{A}}^{{B}}{D}d{x}$
54 1 2 5 3 6 7 ditgcl ${⊢}{\phi }\to {\int }_{{C}}^{{A}}{D}d{x}\in ℂ$
55 1 2 3 4 6 7 ditgcl ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}\in ℂ$
56 30 54 55 addassd ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}$
57 55 addid2d ${⊢}{\phi }\to 0+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}$
58 53 56 57 3eqtr3d ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}$
59 58 ad2antrr ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {C}\le {A}\right)\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}$
60 48 59 eqtrd ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {C}\le {A}\right)\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}$
61 60 oveq1d ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {C}\le {A}\right)\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
62 45 61 eqtr3d ${⊢}\left(\left({\phi }\wedge {A}\le {B}\right)\wedge {C}\le {A}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
63 16 21 44 62 lecasei ${⊢}\left({\phi }\wedge {A}\le {B}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
64 11 adantr ${⊢}\left({\phi }\wedge {B}\le {A}\right)\to {A}\in ℝ$
65 20 adantr ${⊢}\left({\phi }\wedge {B}\le {A}\right)\to {C}\in ℝ$
66 biid ${⊢}\left({B}\le {A}\wedge {A}\le {C}\right)↔\left({B}\le {A}\wedge {A}\le {C}\right)$
67 1 2 4 3 5 6 7 66 ditgsplitlem ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {A}\le {C}\right)\to {\int }_{{B}}^{{C}}{D}d{x}={\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}$
68 67 oveq2d ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {A}\le {C}\right)\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}$
69 1 2 3 4 6 7 ditgswap ${⊢}{\phi }\to {\int }_{{B}}^{{A}}{D}d{x}=-{\int }_{{A}}^{{B}}{D}d{x}$
70 69 oveq2d ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+\left(-{\int }_{{A}}^{{B}}{D}d{x}\right)$
71 55 negidd ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}+\left(-{\int }_{{A}}^{{B}}{D}d{x}\right)=0$
72 70 71 eqtrd ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}=0$
73 72 oveq1d ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}=0+{\int }_{{A}}^{{C}}{D}d{x}$
74 1 2 4 3 6 7 ditgcl ${⊢}{\phi }\to {\int }_{{B}}^{{A}}{D}d{x}\in ℂ$
75 55 74 30 addassd ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}$
76 30 addid2d ${⊢}{\phi }\to 0+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}$
77 73 75 76 3eqtr3d ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}$
78 77 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {A}\le {C}\right)\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}$
79 68 78 eqtr2d ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {A}\le {C}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
80 15 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {A}\right)\to {B}\in ℝ$
81 20 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {A}\right)\to {C}\in ℝ$
82 ancom ${⊢}\left({C}\le {A}\wedge {B}\le {C}\right)↔\left({B}\le {C}\wedge {C}\le {A}\right)$
83 1 2 4 5 3 6 7 82 ditgsplitlem ${⊢}\left(\left({\phi }\wedge {C}\le {A}\right)\wedge {B}\le {C}\right)\to {\int }_{{B}}^{{A}}{D}d{x}={\int }_{{B}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}$
84 83 oveq1d ${⊢}\left(\left({\phi }\wedge {C}\le {A}\right)\wedge {B}\le {C}\right)\to {\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{B}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}$
85 32 54 30 addassd ${⊢}{\phi }\to {\int }_{{B}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{B}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}$
86 1 2 5 3 6 7 ditgswap ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}=-{\int }_{{C}}^{{A}}{D}d{x}$
87 86 oveq2d ${⊢}{\phi }\to {\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{C}}^{{A}}{D}d{x}+\left(-{\int }_{{C}}^{{A}}{D}d{x}\right)$
88 54 negidd ${⊢}{\phi }\to {\int }_{{C}}^{{A}}{D}d{x}+\left(-{\int }_{{C}}^{{A}}{D}d{x}\right)=0$
89 87 88 eqtrd ${⊢}{\phi }\to {\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}=0$
90 89 oveq2d ${⊢}{\phi }\to {\int }_{{B}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{B}}^{{C}}{D}d{x}+0$
91 32 addid1d ${⊢}{\phi }\to {\int }_{{B}}^{{C}}{D}d{x}+0={\int }_{{B}}^{{C}}{D}d{x}$
92 85 90 91 3eqtrd ${⊢}{\phi }\to {\int }_{{B}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{B}}^{{C}}{D}d{x}$
93 92 ad2antrr ${⊢}\left(\left({\phi }\wedge {C}\le {A}\right)\wedge {B}\le {C}\right)\to {\int }_{{B}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{B}}^{{C}}{D}d{x}$
94 84 93 eqtr2d ${⊢}\left(\left({\phi }\wedge {C}\le {A}\right)\wedge {B}\le {C}\right)\to {\int }_{{B}}^{{C}}{D}d{x}={\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}$
95 94 oveq2d ${⊢}\left(\left({\phi }\wedge {C}\le {A}\right)\wedge {B}\le {C}\right)\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}$
96 77 ad2antrr ${⊢}\left(\left({\phi }\wedge {C}\le {A}\right)\wedge {B}\le {C}\right)\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}$
97 95 96 eqtr2d ${⊢}\left(\left({\phi }\wedge {C}\le {A}\right)\wedge {B}\le {C}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
98 97 adantllr ${⊢}\left(\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {A}\right)\wedge {B}\le {C}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
99 ancom ${⊢}\left({B}\le {A}\wedge {C}\le {B}\right)↔\left({C}\le {B}\wedge {B}\le {A}\right)$
100 1 2 5 4 3 6 7 99 ditgsplitlem ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{C}}^{{A}}{D}d{x}={\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}$
101 100 oveq1d ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}$
102 31 74 55 addassd ${⊢}{\phi }\to {\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}$
103 1 2 4 3 6 7 ditgswap ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{D}d{x}=-{\int }_{{B}}^{{A}}{D}d{x}$
104 103 oveq2d ${⊢}{\phi }\to {\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{B}}^{{A}}{D}d{x}+\left(-{\int }_{{B}}^{{A}}{D}d{x}\right)$
105 74 negidd ${⊢}{\phi }\to {\int }_{{B}}^{{A}}{D}d{x}+\left(-{\int }_{{B}}^{{A}}{D}d{x}\right)=0$
106 104 105 eqtrd ${⊢}{\phi }\to {\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}=0$
107 106 oveq2d ${⊢}{\phi }\to {\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{C}}^{{B}}{D}d{x}+0$
108 31 addid1d ${⊢}{\phi }\to {\int }_{{C}}^{{B}}{D}d{x}+0={\int }_{{C}}^{{B}}{D}d{x}$
109 102 107 108 3eqtrd ${⊢}{\phi }\to {\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{C}}^{{B}}{D}d{x}$
110 109 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{C}}^{{B}}{D}d{x}$
111 101 110 eqtr2d ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{C}}^{{B}}{D}d{x}={\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}$
112 111 oveq2d ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}$
113 58 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{A}}{D}d{x}+{\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}$
114 112 113 eqtr2d ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{B}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}$
115 114 oveq1d ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
116 40 ad2antrr ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{C}}{D}d{x}+{\int }_{{C}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}={\int }_{{A}}^{{C}}{D}d{x}$
117 115 116 eqtr2d ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
118 117 adantlr ${⊢}\left(\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {A}\right)\wedge {C}\le {B}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
119 80 81 98 118 lecasei ${⊢}\left(\left({\phi }\wedge {B}\le {A}\right)\wedge {C}\le {A}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
120 64 65 79 119 lecasei ${⊢}\left({\phi }\wedge {B}\le {A}\right)\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$
121 11 15 63 120 lecasei ${⊢}{\phi }\to {\int }_{{A}}^{{C}}{D}d{x}={\int }_{{A}}^{{B}}{D}d{x}+{\int }_{{B}}^{{C}}{D}d{x}$