ovolmge0

Description: The set M is composed of nonnegative extended real numbers. (Contributed by Mario Carneiro, 16-Mar-2014)

		Ref	Expression
	Hypothesis	elovolm.1	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
	Assertion	ovolmge0	$⊢ B \in M \to 0 \leq B$

Proof

Step	Hyp	Ref	Expression
1		elovolm.1	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
2	1	elovolm	$⊢ B \in M \leftrightarrow \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land B = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))$
3		elovolmlem	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow f : ℕ ⟶ \leq \cap ℝ^{2}$
4		eqid	$⊢ (abs \circ -) \circ f = (abs \circ -) \circ f$
5		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
6	4 5	ovolsf	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞)$
7		1nn	$⊢ 1 \in ℕ$
8		ffvelcdm	$⊢ (seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ [0, +∞) \land 1 \in ℕ) \to seq 1 (+ ((abs \circ -) \circ f)) (1) \in [0, +∞)$
9	6 7 8	sylancl	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ f)) (1) \in [0, +∞)$
10		elrege0	$⊢ seq 1 (+ ((abs \circ -) \circ f)) (1) \in [0, +∞) \leftrightarrow (seq 1 (+ ((abs \circ -) \circ f)) (1) \in ℝ \land 0 \leq seq 1 (+ ((abs \circ -) \circ f)) (1))$
11	10	simprbi	$⊢ seq 1 (+ ((abs \circ -) \circ f)) (1) \in [0, +∞) \to 0 \leq seq 1 (+ ((abs \circ -) \circ f)) (1)$
12	9 11	syl	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to 0 \leq seq 1 (+ ((abs \circ -) \circ f)) (1)$
13	6	frnd	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq [0, +∞)$
14		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
15	13 14	sstrdi	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{*}$
16	6	ffnd	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ f)) Fn ℕ$
17		fnfvelrn	$⊢ (seq 1 (+ ((abs \circ -) \circ f)) Fn ℕ \land 1 \in ℕ) \to seq 1 (+ ((abs \circ -) \circ f)) (1) \in ran seq 1 (+ ((abs \circ -) \circ f))$
18	16 7 17	sylancl	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ f)) (1) \in ran seq 1 (+ ((abs \circ -) \circ f))$
19		supxrub	$⊢ (ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{} \land seq 1 (+ ((abs \circ -) \circ f)) (1) \in ran seq 1 (+ ((abs \circ -) \circ f))) \to seq 1 (+ ((abs \circ -) \circ f)) (1) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)$
20	15 18 19	syl2anc	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ f)) (1) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
21		0xr	$⊢ 0 \in ℝ^{*}$
22	14 9	sselid	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ f)) (1) \in ℝ^{*}$
23		supxrcl	$⊢ ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{} \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{*}$
24	15 23	syl	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{}$
25		xrletr	$⊢ (0 \in ℝ^{} \land seq 1 (+ ((abs \circ -) \circ f)) (1) \in ℝ^{} \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \in ℝ^{}) \to ((0 \leq seq 1 (+ ((abs \circ -) \circ f)) (1) \land seq 1 (+ ((abs \circ -) \circ f)) (1) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to 0 \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))$
26	21 22 24 25	mp3an2i	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to ((0 \leq seq 1 (+ ((abs \circ -) \circ f)) (1) \land seq 1 (+ ((abs \circ -) \circ f)) (1) \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \to 0 \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))$
27	12 20 26	mp2and	$⊢ f : ℕ ⟶ \leq \cap ℝ^{2} \to 0 \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
28	3 27	sylbi	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to 0 \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
29		breq2	$⊢ B = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \to (0 \leq B \leftrightarrow 0 \leq sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))$
30	28 29	syl5ibrcom	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (B = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <) \to 0 \leq B)$
31	30	adantld	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to ((A \subseteq ⋃ ran ((.) \circ f) \land B = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)) \to 0 \leq B)$
32	31	rexlimiv	$⊢ \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land B = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)) \to 0 \leq B$
33	2 32	sylbi	$⊢ B \in M \to 0 \leq B$

Metamath Proof Explorer

Theorem ovolmge0

Proof