# Metamath Proof Explorer

## Theorem volioc

Description: The measure of a left-open right-closed interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion volioc ${⊢}\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 vol0 ${⊢}vol\left(\varnothing \right)=0$
2 oveq2 ${⊢}{A}={B}\to \left({A},{A}\right]=\left({A},{B}\right]$
3 2 eqcomd ${⊢}{A}={B}\to \left({A},{B}\right]=\left({A},{A}\right]$
4 leid ${⊢}{A}\in ℝ\to {A}\le {A}$
5 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
6 ioc0 ${⊢}\left({A}\in {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left(\left({A},{A}\right]=\varnothing ↔{A}\le {A}\right)$
7 5 5 6 syl2anc ${⊢}{A}\in ℝ\to \left(\left({A},{A}\right]=\varnothing ↔{A}\le {A}\right)$
8 4 7 mpbird ${⊢}{A}\in ℝ\to \left({A},{A}\right]=\varnothing$
9 3 8 sylan9eqr ${⊢}\left({A}\in ℝ\wedge {A}={B}\right)\to \left({A},{B}\right]=\varnothing$
10 9 fveq2d ${⊢}\left({A}\in ℝ\wedge {A}={B}\right)\to vol\left(\left({A},{B}\right]\right)=vol\left(\varnothing \right)$
11 eqcom ${⊢}{A}={B}↔{B}={A}$
12 11 biimpi ${⊢}{A}={B}\to {B}={A}$
13 12 adantl ${⊢}\left({A}\in ℝ\wedge {A}={B}\right)\to {B}={A}$
14 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
15 14 adantr ${⊢}\left({A}\in ℝ\wedge {A}={B}\right)\to {A}\in ℂ$
16 13 15 eqeltrd ${⊢}\left({A}\in ℝ\wedge {A}={B}\right)\to {B}\in ℂ$
17 16 13 subeq0bd ${⊢}\left({A}\in ℝ\wedge {A}={B}\right)\to {B}-{A}=0$
18 1 10 17 3eqtr4a ${⊢}\left({A}\in ℝ\wedge {A}={B}\right)\to vol\left(\left({A},{B}\right]\right)={B}-{A}$
19 18 3ad2antl1 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\wedge {A}={B}\right)\to vol\left(\left({A},{B}\right]\right)={B}-{A}$
20 simpl1 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\wedge ¬{A}={B}\right)\to {A}\in ℝ$
21 simpl2 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\wedge ¬{A}={B}\right)\to {B}\in ℝ$
22 simpl3 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\wedge ¬{A}={B}\right)\to {A}\le {B}$
23 eqcom ${⊢}{B}={A}↔{A}={B}$
24 23 biimpi ${⊢}{B}={A}\to {A}={B}$
25 24 necon3bi ${⊢}¬{A}={B}\to {B}\ne {A}$
26 25 adantl ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\wedge ¬{A}={B}\right)\to {B}\ne {A}$
27 20 21 22 26 leneltd ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\wedge ¬{A}={B}\right)\to {A}<{B}$
28 5 3ad2ant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {A}\in {ℝ}^{*}$
29 rexr ${⊢}{B}\in ℝ\to {B}\in {ℝ}^{*}$
30 29 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}\in {ℝ}^{*}$
31 simp3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {A}<{B}$
32 ioounsn ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\to \left({A},{B}\right)\cup \left\{{B}\right\}=\left({A},{B}\right]$
33 28 30 31 32 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({A},{B}\right)\cup \left\{{B}\right\}=\left({A},{B}\right]$
34 33 eqcomd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({A},{B}\right]=\left({A},{B}\right)\cup \left\{{B}\right\}$
35 34 fveq2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to vol\left(\left({A},{B}\right]\right)=vol\left(\left({A},{B}\right)\cup \left\{{B}\right\}\right)$
36 ioombl ${⊢}\left({A},{B}\right)\in \mathrm{dom}vol$
37 36 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({A},{B}\right)\in \mathrm{dom}vol$
38 snmbl ${⊢}{B}\in ℝ\to \left\{{B}\right\}\in \mathrm{dom}vol$
39 38 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left\{{B}\right\}\in \mathrm{dom}vol$
40 ubioo ${⊢}¬{B}\in \left({A},{B}\right)$
41 disjsn ${⊢}\left({A},{B}\right)\cap \left\{{B}\right\}=\varnothing ↔¬{B}\in \left({A},{B}\right)$
42 40 41 mpbir ${⊢}\left({A},{B}\right)\cap \left\{{B}\right\}=\varnothing$
43 42 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to \left({A},{B}\right)\cap \left\{{B}\right\}=\varnothing$
44 ioovolcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to vol\left(\left({A},{B}\right)\right)\in ℝ$
45 44 3adant3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to vol\left(\left({A},{B}\right)\right)\in ℝ$
46 volsn ${⊢}{B}\in ℝ\to vol\left(\left\{{B}\right\}\right)=0$
47 0red ${⊢}{B}\in ℝ\to 0\in ℝ$
48 46 47 eqeltrd ${⊢}{B}\in ℝ\to vol\left(\left\{{B}\right\}\right)\in ℝ$
49 48 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to vol\left(\left\{{B}\right\}\right)\in ℝ$
50 volun ${⊢}\left(\left(\left({A},{B}\right)\in \mathrm{dom}vol\wedge \left\{{B}\right\}\in \mathrm{dom}vol\wedge \left({A},{B}\right)\cap \left\{{B}\right\}=\varnothing \right)\wedge \left(vol\left(\left({A},{B}\right)\right)\in ℝ\wedge vol\left(\left\{{B}\right\}\right)\in ℝ\right)\right)\to vol\left(\left({A},{B}\right)\cup \left\{{B}\right\}\right)=vol\left(\left({A},{B}\right)\right)+vol\left(\left\{{B}\right\}\right)$
51 37 39 43 45 49 50 syl32anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to vol\left(\left({A},{B}\right)\cup \left\{{B}\right\}\right)=vol\left(\left({A},{B}\right)\right)+vol\left(\left\{{B}\right\}\right)$
52 simp1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {A}\in ℝ$
53 simp2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}\in ℝ$
54 52 53 31 ltled ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {A}\le {B}$
55 volioo ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to vol\left(\left({A},{B}\right)\right)={B}-{A}$
56 52 53 54 55 syl3anc ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to vol\left(\left({A},{B}\right)\right)={B}-{A}$
57 46 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to vol\left(\left\{{B}\right\}\right)=0$
58 56 57 oveq12d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to vol\left(\left({A},{B}\right)\right)+vol\left(\left\{{B}\right\}\right)={B}-{A}+0$
59 53 recnd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}\in ℂ$
60 14 3ad2ant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {A}\in ℂ$
61 59 60 subcld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}-{A}\in ℂ$
62 61 addid1d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to {B}-{A}+0={B}-{A}$
63 58 62 eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to vol\left(\left({A},{B}\right)\right)+vol\left(\left\{{B}\right\}\right)={B}-{A}$
64 35 51 63 3eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}<{B}\right)\to vol\left(\left({A},{B}\right]\right)={B}-{A}$
65 20 21 27 64 syl3anc ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\wedge ¬{A}={B}\right)\to vol\left(\left({A},{B}\right]\right)={B}-{A}$
66 19 65 pm2.61dan ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to vol\left(\left({A},{B}\right]\right)={B}-{A}$