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 ⁡ A B = if A ≤ B B − A 0

Proof

Step Hyp Ref Expression
1 iftrue ⊢ A < B → if A < B B − A 0 = B − A
2 1 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → if A < B B − A 0 = B − A
3 volico ⊢ A ∈ ℝ ∧ B ∈ ℝ → vol ⁡ A B = if A < B B − A 0
4 3 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → vol ⁡ A B = if A < B B − A 0
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 → if A ≤ B B − A 0 = B − A
10 2 4 9 3eqtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → vol ⁡ A B = if A ≤ B B − A 0
11 10 adantlr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B ∧ A < B → vol ⁡ A B = if A ≤ B B − A 0
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 → if A < B B − A 0 = 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 → if A < B B − A 0 = B − A
33 3 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A = B → vol ⁡ A B = if A < B B − A 0
34 22 19 eqled ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A = B → A ≤ B
35 34 iftrued ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A = B → if A ≤ B B − A 0 = B − A
36 32 33 35 3eqtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A = B → vol ⁡ A B = if A ≤ B B − A 0
37 12 17 36 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B ∧ ¬ A < B → vol ⁡ A B = if A ≤ B B − A 0
38 11 37 pm2.61dan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → vol ⁡ A B = if A ≤ B B − A 0
39 8 stoic1a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A ≤ B → ¬ A < B
40 39 iffalsed ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A ≤ B → if A < B B − A 0 = 0
41 3 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A ≤ B → vol ⁡ A B = if A < B B − A 0
42 iffalse ⊢ ¬ A ≤ B → if A ≤ B B − A 0 = 0
43 42 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A ≤ B → if A ≤ B B − A 0 = 0
44 40 41 43 3eqtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ ¬ A ≤ B → vol ⁡ A B = if A ≤ B B − A 0
45 38 44 pm2.61dan ⊢ A ∈ ℝ ∧ B ∈ ℝ → vol ⁡ A B = if A ≤ B B − A 0