# Metamath Proof Explorer

## Theorem ovolioo

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

Ref Expression
Assertion ovolioo ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to {vol}^{*}\left(\left({A},{B}\right)\right)={B}-{A}$

### Proof

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