Metamath Proof Explorer

Theorem ovolicc

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

		Ref	Expression
	Assertion	ovolicc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ([A, B]) = B - A$

Proof

Step	Hyp	Ref	Expression
1		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
2	1	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to [A, B] \subseteq ℝ$
3		ovolcl	$⊢ [A, B] \subseteq ℝ \to {vol}^{} ([A, B]) \in ℝ^{}$
4	2 3	syl	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{} ([A, B]) \in ℝ^{}$
5		simp2	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to B \in ℝ$
6		simp1	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to A \in ℝ$
7	5 6	resubcld	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to B - A \in ℝ$
8	7	rexrd	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to B - A \in ℝ^{*}$
9		simp3	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to A \leq B$
10		eqeq1	$⊢ m = n \to (m = 1 \leftrightarrow n = 1)$
11	10	ifbid	$⊢ m = n \to if (m = 1, ⟨A, B⟩, ⟨0, 0⟩) = if (n = 1, ⟨A, B⟩, ⟨0, 0⟩)$
12	11	cbvmptv	$⊢ (m \in ℕ ⟼ if (m = 1, ⟨A, B⟩, ⟨0, 0⟩)) = (n \in ℕ ⟼ if (n = 1, ⟨A, B⟩, ⟨0, 0⟩))$
13	6 5 9 12	ovolicc1	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ([A, B]) \leq B - A$
14		eqeq1	$⊢ z = y \to (z = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leftrightarrow y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))$
15	14	anbi2d	$⊢ z = y \to (([A, B] \subseteq ⋃ ran ((.) \circ f) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \leftrightarrow ([A, B] \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)))$
16	15	rexbidv	$⊢ z = y \to (\exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) ([A, B] \subseteq ⋃ ran ((.) \circ f) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \leftrightarrow \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) ([A, B] \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)))$
17	16	cbvrabv	$⊢ \{z \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) ([A, B] \subseteq ⋃ ran ((.) \circ f) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) ([A, B] \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
18	6 5 9 17	ovolicc2	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to B - A \leq {vol}^{*} ([A, B])$
19	4 8 13 18	xrletrid	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ([A, B]) = B - A$