Metamath Proof Explorer

Theorem volioore

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

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

Proof

Step Hyp Ref Expression
1 volioo ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
2 1 3expa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
3 iftrue ⊢ ( 𝐴 ≤ 𝐵 → if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
4 3 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = ( 𝐵 − 𝐴 ) )
5 2 4 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
6 simpl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
7 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ¬ 𝐴 ≤ 𝐵 )
8 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
9 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
10 8 9 ltnled ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < 𝐴 ↔ ¬ 𝐴 ≤ 𝐵 ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( 𝐵 < 𝐴 ↔ ¬ 𝐴 ≤ 𝐵 ) )
12 7 11 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 ≤ 𝐵 ) → 𝐵 < 𝐴 )
13 vol0 ⊢ ( vol ‘ ∅ ) = 0
14 13 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( vol ‘ ∅ ) = 0 )
15 8 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → 𝐵 ∈ ℝ )
16 9 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → 𝐴 ∈ ℝ )
17 simpr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → 𝐵 < 𝐴 )
18 15 16 17 ltled ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → 𝐵 ≤ 𝐴 )
19 9 rexrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ* )
20 8 rexrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ* )
21 ioo0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
22 19 20 21 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
23 22 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( ( 𝐴 (,) 𝐵 ) = ∅ ↔ 𝐵 ≤ 𝐴 ) )
24 18 23 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( 𝐴 (,) 𝐵 ) = ∅ )
25 24 fveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = ( vol ‘ ∅ ) )
26 10 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ¬ 𝐴 ≤ 𝐵 )
27 26 iffalsed ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) = 0 )
28 14 25 27 3eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
29 6 12 28 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 ≤ 𝐵 ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )
30 5 29 pm2.61dan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( vol ‘ ( 𝐴 (,) 𝐵 ) ) = if ( 𝐴 ≤ 𝐵 , ( 𝐵 − 𝐴 ) , 0 ) )