Metamath Proof Explorer

Theorem volico2

Description: The measure of left-closed right-open interval. (Contributed by Glauco Siliprandi, 3-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 iftrue ⊢ ( 𝐴 < 𝐵 → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
2 1 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
3 volico ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
5 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
6 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
7 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
8 5 6 7 ltled ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
9 8 iftrued ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
10 2 4 9 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
11 10 adantlr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
12 simpll ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
13 12 simpld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
14 12 simprd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
15 simplr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐴 ≤ 𝐵 )
16 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → ¬ 𝐴 < 𝐵 )
17 13 14 15 16 lenlteq ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → 𝐴 = 𝐵 )
18 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → 𝐵 ∈ ℝ )
19 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
20 19 eqcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → 𝐵 = 𝐴 )
21 18 20 eqled ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → 𝐵 ≤ 𝐴 )
22 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ ℝ )
23 18 22 lenltd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → ( 𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵 ) )
24 21 23 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → ¬ 𝐴 < 𝐵 )
25 24 iffalsed ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = 0 )
26 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
27 26 subidd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − 𝐴 ) = 0 )
28 27 eqcomd ⊢ ( 𝐴 ∈ ℝ → 0 = ( 𝐴 − 𝐴 ) )
29 28 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → 0 = ( 𝐴 − 𝐴 ) )
30 oveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 − 𝐴 ) = ( 𝐵 − 𝐴 ) )
31 30 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → ( 𝐴 − 𝐴 ) = ( 𝐵 − 𝐴 ) )
32 25 29 31 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
33 3 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
34 22 19 eqled ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → 𝐴 ≤ 𝐵 )
35 34 iftrued ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
36 32 33 35 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
37 12 17 36 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ¬ 𝐴 < 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
38 11 37 pm2.61dan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
39 8 stoic1a ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ¬ 𝐴 < 𝐵 )
40 39 iffalsed ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 ≤ 𝐵 ) → if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = 0 )
41 3 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 < 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
42 iffalse ⊢ ( ¬ 𝐴 ≤ 𝐵 → if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = 0 )
43 42 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 ≤ 𝐵 ) → if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = 0 )
44 40 41 43 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
45 38 44 pm2.61dan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 [,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )