Metamath Proof Explorer


Theorem ovolioo

Description: The measure of an open interval. (Contributed by Mario Carneiro, 2-Sep-2014)

Ref Expression
Assertion ovolioo A B A B vol * A B = B A

Proof

Step Hyp Ref Expression
1 ioombl A B dom vol
2 mblvol A B dom vol vol A B = vol * A B
3 1 2 ax-mp vol A B = vol * A B
4 iccmbl A B A B dom vol
5 mblvol A B dom vol vol A B = vol * A B
6 4 5 syl A B vol A B = vol * A B
7 6 3adant3 A B A B vol A B = vol * A B
8 1 a1i A B A B A B dom vol
9 prssi A B A B
10 9 3adant3 A B A B A B
11 prfi A B Fin
12 ovolfi A B Fin A B vol * A B = 0
13 11 10 12 sylancr A B A B vol * A B = 0
14 nulmbl A B vol * A B = 0 A B dom vol
15 10 13 14 syl2anc A B A B A B dom vol
16 df-pr A B = A B
17 16 ineq2i A B A B = A B A B
18 indi A B A B = A B A A B B
19 17 18 eqtri A B A B = A B A A B B
20 simp1 A B A B A
21 20 ltnrd A B A B ¬ A < A
22 eliooord A A B A < A A < B
23 22 simpld A A B A < A
24 21 23 nsyl A B A B ¬ A A B
25 disjsn A B A = ¬ A A B
26 24 25 sylibr A B A B A B A =
27 simp2 A B A B B
28 27 ltnrd A B A B ¬ B < B
29 eliooord B A B A < B B < B
30 29 simprd B A B B < B
31 28 30 nsyl A B A B ¬ B A B
32 disjsn A B B = ¬ B A B
33 31 32 sylibr A B A B A B B =
34 26 33 uneq12d A B A B A B A A B B =
35 un0 =
36 34 35 eqtrdi A B A B A B A A B B =
37 19 36 syl5eq A B A B A B A B =
38 ioossicc A B A B
39 iccssre A B A B
40 39 3adant3 A B A B A B
41 ovolicc A B A B vol * A B = B A
42 27 20 resubcld A B A B B A
43 41 42 eqeltrd A B A B vol * A B
44 ovolsscl A B A B A B vol * A B vol * A B
45 38 40 43 44 mp3an2i A B A B vol * A B
46 3 45 eqeltrid A B A B vol A B
47 mblvol A B dom vol vol A B = vol * A B
48 15 47 syl A B A B vol A B = vol * A B
49 48 13 eqtrd A B A B vol A B = 0
50 0re 0
51 49 50 eqeltrdi A B A B vol A B
52 volun A B dom vol A B dom vol A B A B = vol A B vol A B vol A B A B = vol A B + vol A B
53 8 15 37 46 51 52 syl32anc A B A B vol A B A B = vol A B + vol A B
54 rexr A A *
55 rexr B B *
56 id A B A B
57 prunioo A * B * A B A B A B = A B
58 54 55 56 57 syl3an A B A B A B A B = A B
59 58 fveq2d A B A B vol A B A B = vol A B
60 49 oveq2d A B A B vol A B + vol A B = vol A B + 0
61 46 recnd A B A B vol A B
62 61 addid1d A B A B vol A B + 0 = vol A B
63 60 62 eqtrd A B A B vol A B + vol A B = vol A B
64 53 59 63 3eqtr3d A B A B vol A B = vol A B
65 7 64 41 3eqtr3d A B A B vol A B = B A
66 3 65 eqtr3id A B A B vol * A B = B A