Metamath Proof Explorer

Theorem volioore

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

Ref Expression
Assertion volioore ⊢ A ∈ ℝ ∧ B ∈ ℝ → vol ⁡ A B = if A ≤ B B − A 0

Proof

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