Metamath Proof Explorer

Theorem ovolge0

Description: The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014)

		Ref	Expression
	Assertion	ovolge0	$⊢ A \subseteq ℝ \to 0 \leq {vol}^{*} (A)$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$⊢ \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} \subseteq ℝ^{*}$
2		0xr	$⊢ 0 \in ℝ^{*}$
3		infxrgelb	$⊢ (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} \subseteq ℝ^{} \land 0 \in ℝ^{}) \to (0 \leq sup (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <) \leftrightarrow \forall x \in \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))\} 0 \leq x)$
4	1 2 3	mp2an	$⊢ 0 \leq sup (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <) \leftrightarrow \forall x \in \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))\} 0 \leq x$
5		eqid	$⊢ \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
6	5	ovolmge0	$⊢ x \in \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} \to 0 \leq x$
7	4 6	mprgbir	$⊢ 0 \leq sup (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{*} <)$
8	5	ovolval	$⊢ A \subseteq ℝ \to {vol}^{} (A) = sup (\{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\} ℝ^{} <)$
9	7 8	breqtrrid	$⊢ A \subseteq ℝ \to 0 \leq {vol}^{*} (A)$