ovolgelb

Description: The outer volume is the greatest lower bound on the sum of all interval coverings of A . (Contributed by Mario Carneiro, 15-Jun-2014)

		Ref	Expression
	Hypothesis	ovolgelb.1	$⊢ S = seq 1 (+ ((abs \circ -) \circ g))$
	Assertion	ovolgelb	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land sup (ran S ℝ^{} <) \leq {vol}^{*} (A) + B)$

Proof

Step	Hyp	Ref	Expression
1		ovolgelb.1	$⊢ S = seq 1 (+ ((abs \circ -) \circ g))$
2		simp2	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to {vol}^{} (A) \in ℝ$
3		simp3	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ \land B \in ℝ^{+}) \to B \in ℝ^{+}$
4	2 3	ltaddrpd	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to {vol}^{} (A) < {vol}^{*} (A) + B$
5	3	rpred	$⊢ (A \subseteq ℝ \land {vol}^{*} (A) \in ℝ \land B \in ℝ^{+}) \to B \in ℝ$
6	2 5	readdcld	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to {vol}^{} (A) + B \in ℝ$
7	2 6	ltnled	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to ({vol}^{} (A) < {vol}^{} (A) + B \leftrightarrow \neg {vol}^{} (A) + B \leq {vol}^{*} (A))$
8	4 7	mpbid	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to \neg {vol}^{} (A) + B \leq {vol}^{*} (A)$
9		eqid	$⊢ \{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} = \{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\}$
10	9	ovolval	$⊢ A \subseteq ℝ \to {vol}^{} (A) = sup (\{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} ℝ^{} <)$
11	10	3ad2ant1	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to {vol}^{} (A) = sup (\{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} ℝ^{*} <)$
12	11	breq2d	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to ({vol}^{} (A) + B \leq {vol}^{} (A) \leftrightarrow {vol}^{} (A) + B \leq sup (\{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} ℝ^{*} <))$
13		ssrab2	$⊢ \{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} \subseteq ℝ^{*}$
14	6	rexrd	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to {vol}^{} (A) + B \in ℝ^{*}$
15		infxrgelb	$⊢ (\{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} \subseteq ℝ^{} \land {vol}^{} (A) + B \in ℝ^{}) \to ({vol}^{} (A) + B \leq sup (\{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} ℝ^{} <) \leftrightarrow \forall x \in \{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} {vol}^{} (A) + B \leq x)$
16	13 14 15	sylancr	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to ({vol}^{} (A) + B \leq sup (\{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} ℝ^{} <) \leftrightarrow \forall x \in \{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} {vol}^{} (A) + B \leq x)$
17		eqeq1	$⊢ y = x \to (y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leftrightarrow x = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))$
18	1	rneqi	$⊢ ran S = ran seq 1 (+ ((abs \circ -) \circ g))$
19	18	supeq1i	$⊢ sup (ran S ℝ^{} <) = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)$
20	19	eqeq2i	$⊢ x = sup (ran S ℝ^{} <) \leftrightarrow x = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)$
21	17 20	bitr4di	$⊢ y = x \to (y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \leftrightarrow x = sup (ran S ℝ^{} <))$
22	21	anbi2d	$⊢ y = x \to ((A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)))$
23	22	rexbidv	$⊢ y = x \to (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)) \leftrightarrow \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)))$
24	23	ralrab	$⊢ \forall x \in \{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} {vol}^{} (A) + B \leq x \leftrightarrow \forall x \in ℝ^{} (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x)$
25		ralcom	$⊢ \forall x \in ℝ^{} \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) ((A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x) \leftrightarrow \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \forall x \in ℝ^{} ((A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x)$
26		r19.23v	$⊢ \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) ((A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x) \leftrightarrow (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x)$
27	26	ralbii	$⊢ \forall x \in ℝ^{} \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) ((A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x) \leftrightarrow \forall x \in ℝ^{} (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x)$
28		ancomst	$⊢ ((A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x) \leftrightarrow ((x = sup (ran S ℝ^{} <) \land A \subseteq ⋃ ran ((.) \circ g)) \to {vol}^{} (A) + B \leq x)$
29		impexp	$⊢ ((x = sup (ran S ℝ^{} <) \land A \subseteq ⋃ ran ((.) \circ g)) \to {vol}^{} (A) + B \leq x) \leftrightarrow (x = sup (ran S ℝ^{} <) \to (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq x))$
30	28 29	bitri	$⊢ ((A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x) \leftrightarrow (x = sup (ran S ℝ^{} <) \to (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq x))$
31	30	ralbii	$⊢ \forall x \in ℝ^{} ((A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x) \leftrightarrow \forall x \in ℝ^{} (x = sup (ran S ℝ^{} <) \to (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq x))$
32		elovolmlem	$⊢ g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow g : ℕ ⟶ \leq \cap ℝ^{2}$
33		eqid	$⊢ (abs \circ -) \circ g = (abs \circ -) \circ g$
34	33 1	ovolsf	$⊢ g : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
35	32 34	sylbi	$⊢ g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to S : ℕ ⟶ [0, +∞)$
36	35	frnd	$⊢ g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to ran S \subseteq [0, +∞)$
37		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
38	36 37	sstrdi	$⊢ g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to ran S \subseteq ℝ^{*}$
39		supxrcl	$⊢ ran S \subseteq ℝ^{} \to sup (ran S ℝ^{} <) \in ℝ^{*}$
40	38 39	syl	$⊢ g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to sup (ran S ℝ^{} <) \in ℝ^{}$
41		breq2	$⊢ x = sup (ran S ℝ^{} <) \to ({vol}^{} (A) + B \leq x \leftrightarrow {vol}^{} (A) + B \leq sup (ran S ℝ^{} <))$
42	41	imbi2d	$⊢ x = sup (ran S ℝ^{} <) \to ((A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq x) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{} <)))$
43	42	ceqsralv	$⊢ sup (ran S ℝ^{} <) \in ℝ^{} \to (\forall x \in ℝ^{} (x = sup (ran S ℝ^{} <) \to (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq x)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{*} <)))$
44	40 43	syl	$⊢ g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (\forall x \in ℝ^{} (x = sup (ran S ℝ^{} <) \to (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq x)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{*} <)))$
45	31 44	bitrid	$⊢ g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to (\forall x \in ℝ^{} ((A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{*} <)))$
46	45	ralbiia	$⊢ \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \forall x \in ℝ^{} ((A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x) \leftrightarrow \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{*} <))$
47	25 27 46	3bitr3i	$⊢ \forall x \in ℝ^{} (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land x = sup (ran S ℝ^{} <)) \to {vol}^{} (A) + B \leq x) \leftrightarrow \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{*} <))$
48	24 47	bitri	$⊢ \forall x \in \{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} {vol}^{} (A) + B \leq x \leftrightarrow \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{*} <))$
49	16 48	bitr2di	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to (\forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{} <)) \leftrightarrow {vol}^{} (A) + B \leq sup (\{y \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} ℝ^{*} <))$
50	12 49	bitr4d	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to ({vol}^{} (A) + B \leq {vol}^{} (A) \leftrightarrow \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{*} <)))$
51	8 50	mtbid	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to \neg \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{*} <))$
52		rexanali	$⊢ \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land \neg {vol}^{} (A) + B \leq sup (ran S ℝ^{} <)) \leftrightarrow \neg \forall g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \to {vol}^{} (A) + B \leq sup (ran S ℝ^{} <))$
53	51 52	sylibr	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land \neg {vol}^{} (A) + B \leq sup (ran S ℝ^{*} <))$
54		xrltnle	$⊢ (sup (ran S ℝ^{} <) \in ℝ^{} \land {vol}^{} (A) + B \in ℝ^{}) \to (sup (ran S ℝ^{} <) < {vol}^{} (A) + B \leftrightarrow \neg {vol}^{} (A) + B \leq sup (ran S ℝ^{} <))$
55		xrltle	$⊢ (sup (ran S ℝ^{} <) \in ℝ^{} \land {vol}^{} (A) + B \in ℝ^{}) \to (sup (ran S ℝ^{} <) < {vol}^{} (A) + B \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + B)$
56	54 55	sylbird	$⊢ (sup (ran S ℝ^{} <) \in ℝ^{} \land {vol}^{} (A) + B \in ℝ^{}) \to (\neg {vol}^{} (A) + B \leq sup (ran S ℝ^{} <) \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + B)$
57	40 14 56	syl2anr	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to (\neg {vol}^{} (A) + B \leq sup (ran S ℝ^{} <) \to sup (ran S ℝ^{} <) \leq {vol}^{*} (A) + B)$
58	57	anim2d	$⊢ ((A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((A \subseteq ⋃ ran ((.) \circ g) \land \neg {vol}^{} (A) + B \leq sup (ran S ℝ^{} <)) \to (A \subseteq ⋃ ran ((.) \circ g) \land sup (ran S ℝ^{} <) \leq {vol}^{*} (A) + B))$
59	58	reximdva	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land \neg {vol}^{} (A) + B \leq sup (ran S ℝ^{} <)) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land sup (ran S ℝ^{} <) \leq {vol}^{*} (A) + B))$
60	53 59	mpd	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land B \in ℝ^{+}) \to \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land sup (ran S ℝ^{} <) \leq {vol}^{*} (A) + B)$

Metamath Proof Explorer

Theorem ovolgelb

Proof