Metamath Proof Explorer

Theorem volico

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

Ref Expression
Assertion volico ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )

Proof

Step Hyp Ref Expression
1 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ* )
3 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
4 3 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ* )
5 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
6 snunioo1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) = ( 𝐴 [,) 𝐵 ) )
7 2 4 5 6 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) = ( 𝐴 [,) 𝐵 ) )
8 7 eqcomd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 [,) 𝐵 ) = ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) )
9 8 fveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) ) )
10 ioombl ⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
11 10 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
12 snmbl ⊢ ( 𝐴 ∈ ℝ → { 𝐴 } ∈ dom vol )
13 12 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → { 𝐴 } ∈ dom vol )
14 lbioo ⊢ ¬ 𝐴 ∈ ( 𝐴 (,) 𝐵 )
15 disjsn ⊢ ( ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴 ∈ ( 𝐴 (,) 𝐵 ) )
16 14 15 mpbir ⊢ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 } ) = ∅
17 16 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 } ) = ∅ )
18 ioovolcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )
19 18 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ )
20 volsn ⊢ ( 𝐴 ∈ ℝ → ( vol ‘ { 𝐴 } ) = 0 )
21 0red ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
22 20 21 eqeltrd ⊢ ( 𝐴 ∈ ℝ → ( vol ‘ { 𝐴 } ) ∈ ℝ )
23 22 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ { 𝐴 } ) ∈ ℝ )
24 volun ⊢ ( ( ( ( 𝐴 (,) 𝐵 ) ∈ dom vol ∧ { 𝐴 } ∈ dom vol ∧ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 } ) = ∅ ) ∧ ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) ∈ ℝ ∧ ( vol ‘ { 𝐴 } ) ∈ ℝ ) ) → ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) ) = ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐴 } ) ) )
25 11 13 17 19 23 24 syl32anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 } ) ) = ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐴 } ) ) )
26 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
27 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
28 26 27 5 ltled ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
29 volioo ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
30 26 27 28 29 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
31 20 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ { 𝐴 } ) = 0 )
32 30 31 oveq12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐴 } ) ) = ( ( 𝐵 − 𝐴 ) + 0 ) )
33 27 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℂ )
34 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
35 34 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℂ )
36 33 35 subcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℂ )
37 36 addridd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 − 𝐴 ) + 0 ) = ( 𝐵 − 𝐴 ) )
38 32 37 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ( vol ‘ ( 𝐴 (,) 𝐵 ) ) + ( vol ‘ { 𝐴 } ) ) = ( 𝐵 − 𝐴 ) )
39 9 25 38 3eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
40 39 3expa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
41 iftrue ⊢ ( 𝐴 < 𝐵 → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
42 41 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
43 40 42 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
44 simpl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
45 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 < 𝐵 ) → ¬ 𝐴 < 𝐵 )
46 44 simprd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
47 44 simpld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
48 46 47 lenltd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
49 45 48 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐵 ≤ 𝐴 )
50 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ≤ 𝐴 ) → 𝐵 ≤ 𝐴 )
51 1 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ≤ 𝐴 ) → 𝐴 ∈ ℝ* )
52 3 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ≤ 𝐴 ) → 𝐵 ∈ ℝ* )
53 ico0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
54 51 52 53 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ≤ 𝐴 ) → ( ( 𝐴 [,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
55 50 54 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ≤ 𝐴 ) → ( 𝐴 [,) 𝐵 ) = ∅ )
56 55 fveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ≤ 𝐴 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = ( vol ‘ ∅ ) )
57 vol0 ⊢ ( vol ‘ ∅ ) = 0
58 57 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ≤ 𝐴 ) → ( vol ‘ ∅ ) = 0 )
59 56 58 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 ≤ 𝐴 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = 0 )
60 44 49 59 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = 0 )
61 iffalse ⊢ ( ¬ 𝐴 < 𝐵 → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = 0 )
62 61 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 < 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = 0 )
63 60 62 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
64 43 63 pm2.61dan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )