ovollb2

Description: It is often more convenient to do calculations with *closed* coverings rather than open ones; here we show that it makes no difference (compare ovollb ). (Contributed by Mario Carneiro, 24-Mar-2015)

		Ref	Expression
	Hypothesis	ovollb2.1	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	Assertion	ovollb2	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to {vol}^{} (A) \leq sup (ran S ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		ovollb2.1	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
2		simpr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to A \subseteq ⋃ ran ([.] \circ F)$
3		ovolficcss	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃ ran ([.] \circ F) \subseteq ℝ$
4	3	adantr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to ⋃ ran ([.] \circ F) \subseteq ℝ$
5	2 4	sstrd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to A \subseteq ℝ$
6		ovolcl	$⊢ A \subseteq ℝ \to {vol}^{} (A) \in ℝ^{}$
7	5 6	syl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to {vol}^{} (A) \in ℝ^{}$
8	7	adantr	$⊢ ((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) = +∞) \to {vol}^{} (A) \in ℝ^{*}$
9		pnfge	$⊢ {vol}^{} (A) \in ℝ^{} \to {vol}^{*} (A) \leq +∞$
10	8 9	syl	$⊢ ((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) = +∞) \to {vol}^{} (A) \leq +∞$
11		simpr	$⊢ ((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) = +∞) \to sup (ran S ℝ^{} <) = +∞$
12	10 11	breqtrrd	$⊢ ((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) = +∞) \to {vol}^{} (A) \leq sup (ran S ℝ^{*} <)$
13		eqid	$⊢ (abs \circ -) \circ F = (abs \circ -) \circ F$
14	13 1	ovolsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
15	14	adantr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to S : ℕ ⟶ [0, +∞)$
16	15	frnd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to ran S \subseteq [0, +∞)$
17		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
18	16 17	sstrdi	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to ran S \subseteq ℝ$
19		1nn	$⊢ 1 \in ℕ$
20	15	fdmd	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to dom S = ℕ$
21	19 20	eleqtrrid	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to 1 \in dom S$
22	21	ne0d	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to dom S \neq \emptyset$
23		dm0rn0	$⊢ dom S = \emptyset \leftrightarrow ran S = \emptyset$
24	23	necon3bii	$⊢ dom S \neq \emptyset \leftrightarrow ran S \neq \emptyset$
25	22 24	sylib	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to ran S \neq \emptyset$
26		supxrre2	$⊢ (ran S \subseteq ℝ \land ran S \neq \emptyset) \to (sup (ran S ℝ^{} <) \in ℝ \leftrightarrow sup (ran S ℝ^{} <) \neq +∞)$
27	18 25 26	syl2anc	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to (sup (ran S ℝ^{} <) \in ℝ \leftrightarrow sup (ran S ℝ^{} <) \neq +∞)$
28	27	biimpar	$⊢ ((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) \neq +∞) \to sup (ran S ℝ^{} <) \in ℝ$
29		2fveq3	$⊢ m = n \to 1^{st} (F (m)) = 1^{st} (F (n))$
30		oveq2	$⊢ m = n \to 2^{m} = 2^{n}$
31	30	oveq2d	$⊢ m = n \to \frac{\frac{x}{2}}{2^{m}} = \frac{\frac{x}{2}}{2^{n}}$
32	29 31	oveq12d	$⊢ m = n \to 1^{st} (F (m)) - (\frac{\frac{x}{2}}{2^{m}}) = 1^{st} (F (n)) - (\frac{\frac{x}{2}}{2^{n}})$
33		2fveq3	$⊢ m = n \to 2^{nd} (F (m)) = 2^{nd} (F (n))$
34	33 31	oveq12d	$⊢ m = n \to 2^{nd} (F (m)) + (\frac{\frac{x}{2}}{2^{m}}) = 2^{nd} (F (n)) + (\frac{\frac{x}{2}}{2^{n}})$
35	32 34	opeq12d	$⊢ m = n \to ⟨1^{st} (F (m)) - (\frac{\frac{x}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{x}{2}}{2^{m}})⟩ = ⟨1^{st} (F (n)) - (\frac{\frac{x}{2}}{2^{n}}), 2^{nd} (F (n)) + (\frac{\frac{x}{2}}{2^{n}})⟩$
36	35	cbvmptv	$⊢ (m \in ℕ ⟼ ⟨1^{st} (F (m)) - (\frac{\frac{x}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{x}{2}}{2^{m}})⟩) = (n \in ℕ ⟼ ⟨1^{st} (F (n)) - (\frac{\frac{x}{2}}{2^{n}}), 2^{nd} (F (n)) + (\frac{\frac{x}{2}}{2^{n}})⟩)$
37		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ (m \in ℕ ⟼ ⟨1^{st} (F (m)) - (\frac{\frac{x}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{x}{2}}{2^{m}})⟩))) = seq 1 (+ ((abs \circ -) \circ (m \in ℕ ⟼ ⟨1^{st} (F (m)) - (\frac{\frac{x}{2}}{2^{m}}), 2^{nd} (F (m)) + (\frac{\frac{x}{2}}{2^{m}})⟩)))$
38		simplll	$⊢ (((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{*} <) \in ℝ) \land x \in ℝ^{+}) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
39		simpllr	$⊢ (((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{*} <) \in ℝ) \land x \in ℝ^{+}) \to A \subseteq ⋃ ran ([.] \circ F)$
40		simpr	$⊢ (((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{*} <) \in ℝ) \land x \in ℝ^{+}) \to x \in ℝ^{+}$
41		simplr	$⊢ (((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) \in ℝ) \land x \in ℝ^{+}) \to sup (ran S ℝ^{} <) \in ℝ$
42	1 36 37 38 39 40 41	ovollb2lem	$⊢ (((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) \in ℝ) \land x \in ℝ^{+}) \to {vol}^{} (A) \leq sup (ran S ℝ^{*} <) + x$
43	42	ralrimiva	$⊢ ((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) \in ℝ) \to \forall x \in ℝ^{+} {vol}^{} (A) \leq sup (ran S ℝ^{*} <) + x$
44		xralrple	$⊢ ({vol}^{} (A) \in ℝ^{} \land sup (ran S ℝ^{} <) \in ℝ) \to ({vol}^{} (A) \leq sup (ran S ℝ^{} <) \leftrightarrow \forall x \in ℝ^{+} {vol}^{} (A) \leq sup (ran S ℝ^{*} <) + x)$
45	7 44	sylan	$⊢ ((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) \in ℝ) \to ({vol}^{} (A) \leq sup (ran S ℝ^{} <) \leftrightarrow \forall x \in ℝ^{+} {vol}^{} (A) \leq sup (ran S ℝ^{*} <) + x)$
46	43 45	mpbird	$⊢ ((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) \in ℝ) \to {vol}^{} (A) \leq sup (ran S ℝ^{*} <)$
47	28 46	syldan	$⊢ ((F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \land sup (ran S ℝ^{} <) \neq +∞) \to {vol}^{} (A) \leq sup (ran S ℝ^{*} <)$
48	12 47	pm2.61dane	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ([.] \circ F)) \to {vol}^{} (A) \leq sup (ran S ℝ^{} <)$

Metamath Proof Explorer

Theorem ovollb2

Proof