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 ⊢A∈ℝ∧B∈ℝ→vol⁡AB=ifA≤BB−A0

Proof

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