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 φ A
itgsplitioo.2 φ C
itgsplitioo.3 φ B A C
itgsplitioo.4 φ x A C D
itgsplitioo.5 φ x A B D 𝐿 1
itgsplitioo.6 φ x B C D 𝐿 1
Assertion itgsplitioo φ A C D dx = A B D dx + B C D dx

Proof

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