# Metamath Proof Explorer

## Theorem ovolicc

Description: The measure of a closed interval. (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion ovolicc $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → vol * ⁡ A B = B − A$

### Proof

Step Hyp Ref Expression
1 iccssre $⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ⊆ ℝ$
2 1 3adant3 $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A B ⊆ ℝ$
3 ovolcl $⊢ A B ⊆ ℝ → vol * ⁡ A B ∈ ℝ *$
4 2 3 syl $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → vol * ⁡ A B ∈ ℝ *$
5 simp2 $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B ∈ ℝ$
6 simp1 $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ∈ ℝ$
7 5 6 resubcld $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B − A ∈ ℝ$
8 7 rexrd $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B − A ∈ ℝ *$
9 simp3 $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → A ≤ B$
10 eqeq1 $⊢ m = n → m = 1 ↔ n = 1$
11 10 ifbid $⊢ m = n → if m = 1 A B 0 0 = if n = 1 A B 0 0$
12 11 cbvmptv $⊢ m ∈ ℕ ⟼ if m = 1 A B 0 0 = n ∈ ℕ ⟼ if n = 1 A B 0 0$
13 6 5 9 12 ovolicc1 $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → vol * ⁡ A B ≤ B − A$
14 eqeq1 $⊢ z = y → z = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ↔ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <$
15 14 anbi2d $⊢ z = y → A B ⊆ ⋃ ran ⁡ . ∘ f ∧ z = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ↔ A B ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <$
16 15 rexbidv $⊢ z = y → ∃ f ∈ ≤ ∩ ℝ 2 ℕ A B ⊆ ⋃ ran ⁡ . ∘ f ∧ z = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < ↔ ∃ f ∈ ≤ ∩ ℝ 2 ℕ A B ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <$
17 16 cbvrabv $⊢ z ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ A B ⊆ ⋃ ran ⁡ . ∘ f ∧ z = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * < = y ∈ ℝ * | ∃ f ∈ ≤ ∩ ℝ 2 ℕ A B ⊆ ⋃ ran ⁡ . ∘ f ∧ y = sup ran ⁡ seq 1 + abs ∘ − ∘ f ℝ * <$
18 6 5 9 17 ovolicc2 $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B − A ≤ vol * ⁡ A B$
19 4 8 13 18 xrletrid $⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → vol * ⁡ A B = B − A$