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⁡AB=ifA≤BB−A0

Proof

Step Hyp Ref Expression
1 volioo ⊢A∈ℝ∧B∈ℝ∧A≤B→vol⁡AB=B−A
2 1 3expa ⊢A∈ℝ∧B∈ℝ∧A≤B→vol⁡AB=B−A
3 iftrue ⊢A≤B→ifA≤BB−A0=B−A
4 3 adantl ⊢A∈ℝ∧B∈ℝ∧A≤B→ifA≤BB−A0=B−A
5 2 4 eqtr4d ⊢A∈ℝ∧B∈ℝ∧A≤B→vol⁡AB=ifA≤BB−A0
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∈ℝ*→AB=∅↔B≤A
22 19 20 21 syl2anc ⊢A∈ℝ∧B∈ℝ→AB=∅↔B≤A
23 22 adantr ⊢A∈ℝ∧B∈ℝ∧B<A→AB=∅↔B≤A
24 18 23 mpbird ⊢A∈ℝ∧B∈ℝ∧B<A→AB=∅
25 24 fveq2d ⊢A∈ℝ∧B∈ℝ∧B<A→vol⁡AB=vol⁡∅
26 10 biimpa ⊢A∈ℝ∧B∈ℝ∧B<A→¬A≤B
27 26 iffalsed ⊢A∈ℝ∧B∈ℝ∧B<A→ifA≤BB−A0=0
28 14 25 27 3eqtr4d ⊢A∈ℝ∧B∈ℝ∧B<A→vol⁡AB=ifA≤BB−A0
29 6 12 28 syl2anc ⊢A∈ℝ∧B∈ℝ∧¬A≤B→vol⁡AB=ifA≤BB−A0
30 5 29 pm2.61dan ⊢A∈ℝ∧B∈ℝ→vol⁡AB=ifA≤BB−A0