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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,] 𝐵 ) ) = ( 𝐵 − 𝐴 ) )

Proof

Step Hyp Ref Expression
1 vol0 ⊢ ( vol ‘ ∅ ) = 0
2 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,] 𝐴 ) = ( 𝐴 (,] 𝐵 ) )
3 2 eqcomd ⊢ ( 𝐴 = 𝐵 → ( 𝐴 (,] 𝐵 ) = ( 𝐴 (,] 𝐴 ) )
4 leid ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ 𝐴 )
5 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
6 ioc0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( ( 𝐴 (,] 𝐴 ) = ∅ ↔ 𝐴 ≤ 𝐴 ) )
7 5 5 6 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 (,] 𝐴 ) = ∅ ↔ 𝐴 ≤ 𝐴 ) )
8 4 7 mpbird ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 (,] 𝐴 ) = ∅ )
9 3 8 sylan9eqr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 𝐵 ) → ( 𝐴 (,] 𝐵 ) = ∅ )
10 9 fveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 𝐵 ) → ( vol ‘ ( 𝐴 (,] 𝐵 ) ) = ( vol ‘ ∅ ) )
11 eqcom ⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
12 11 biimpi ⊢ ( 𝐴 = 𝐵 → 𝐵 = 𝐴 )
13 12 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 𝐵 ) → 𝐵 = 𝐴 )
14 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
15 14 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ ℂ )
16 13 15 eqeltrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ ℂ )
17 16 13 subeq0bd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 𝐵 ) → ( 𝐵 − 𝐴 ) = 0 )
18 1 10 17 3eqtr4a ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 𝐵 ) → ( vol ‘ ( 𝐴 (,] 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
19 18 3ad2antl1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ 𝐴 = 𝐵 ) → ( vol ‘ ( 𝐴 (,] 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
20 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ∈ ℝ )
21 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 ∈ ℝ )
22 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ≤ 𝐵 )
23 eqcom ⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
24 23 biimpi ⊢ ( 𝐵 = 𝐴 → 𝐴 = 𝐵 )
25 24 necon3bi ⊢ ( ¬ 𝐴 = 𝐵 → 𝐵 ≠ 𝐴 )
26 25 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 ≠ 𝐴 )
27 20 21 22 26 leneltd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 < 𝐵 )
28 5 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ* )
29 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
30 29 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ* )
31 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
32 ioounsn ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
33 28 30 31 32 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
34 33 eqcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 (,] 𝐵 ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) )
35 34 fveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 (,] 𝐵 ) ) = ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) )
36 ioombl ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
37 36 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
38 snmbl ⊢ ( 𝐵 ∈ ℝ → { 𝐵 } ∈ dom vol )
39 38 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → { 𝐵 } ∈ dom vol )
40 ubioo ⊢ ¬ 𝐵 ∈ ( 𝐴 (,) 𝐵 )
41 disjsn ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ ( 𝐴 (,) 𝐵 ) )
42 40 41 mpbir ⊢ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐵 } ) = ∅
43 42 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐵 } ) = ∅ )
44 ioovolcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )
45 44 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )
46 volsn ⊢ ( 𝐵 ∈ ℝ → ( vol ‘ { 𝐵 } ) = 0 )
47 0red ⊢ ( 𝐵 ∈ ℝ → 0 ∈ ℝ )
48 46 47 eqeltrd ⊢ ( 𝐵 ∈ ℝ → ( vol ‘ { 𝐵 } ) ∈ ℝ )
49 48 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ { 𝐵 } ) ∈ ℝ )
50 volun ⊢ ( ( ( ( 𝐴 (,) 𝐵 ) ∈ dom vol ∧ { 𝐵 } ∈ dom vol ∧ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐵 } ) = ∅ ) ∧ ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ∧ ( vol ‘ { 𝐵 } ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) = ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐵 } ) ) )
51 37 39 43 45 49 50 syl32anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ) = ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐵 } ) ) )
52 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
53 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
54 52 53 31 ltled ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
55 volioo ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
56 52 53 54 55 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
57 46 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ { 𝐵 } ) = 0 )
58 56 57 oveq12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐵 } ) ) = ( ( 𝐵 − 𝐴 ) + 0 ) )
59 53 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℂ )
60 14 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℂ )
61 59 60 subcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
62 61 addid1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 − 𝐴 ) + 0 ) = ( 𝐵 − 𝐴 ) )
63 58 62 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐵 } ) ) = ( 𝐵 − 𝐴 ) )
64 35 51 63 3eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 (,] 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
65 20 21 27 64 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 = 𝐵 ) → ( vol ‘ ( 𝐴 (,] 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
66 19 65 pm2.61dan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,] 𝐵 ) ) = ( 𝐵 − 𝐴 ) )