ovolscalem2

	Ref	Expression
Hypotheses	ovolsca.1	$⊢ φ \to A \subseteq ℝ$
	ovolsca.2	$⊢ φ \to C \in ℝ^{+}$
	ovolsca.3	$⊢ φ \to B = \{x \in ℝ \| C x \in A\}$
	ovolsca.4	$⊢ φ \to {vol}^{*} (A) \in ℝ$
Assertion	ovolscalem2	$⊢ φ \to {vol}^{} (B) \leq \frac{{vol}^{} (A)}{C}$

Proof

Step	Hyp	Ref	Expression
1		ovolsca.1	$⊢ φ \to A \subseteq ℝ$
2		ovolsca.2	$⊢ φ \to C \in ℝ^{+}$
3		ovolsca.3	$⊢ φ \to B = \{x \in ℝ \| C x \in A\}$
4		ovolsca.4	$⊢ φ \to {vol}^{*} (A) \in ℝ$
5	1	adantr	$⊢ (φ \land y \in ℝ^{+}) \to A \subseteq ℝ$
6	4	adantr	$⊢ (φ \land y \in ℝ^{+}) \to {vol}^{*} (A) \in ℝ$
7		rpmulcl	$⊢ (C \in ℝ^{+} \land y \in ℝ^{+}) \to C y \in ℝ^{+}$
8	2 7	sylan	$⊢ (φ \land y \in ℝ^{+}) \to C y \in ℝ^{+}$
9		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
10	9	ovolgelb	$⊢ (A \subseteq ℝ \land {vol}^{} (A) \in ℝ \land C y \in ℝ^{+}) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{*} (A) + C y)$
11	5 6 8 10	syl3anc	$⊢ (φ \land y \in ℝ^{+}) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y)$
12	1	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y))) \to A \subseteq ℝ$
13	2	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y))) \to C \in ℝ^{+}$
14	3	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y))) \to B = \{x \in ℝ \| C x \in A\}$
15	4	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y))) \to {vol}^{*} (A) \in ℝ$
16		2fveq3	$⊢ m = n \to 1^{st} (f (m)) = 1^{st} (f (n))$
17	16	oveq1d	$⊢ m = n \to \frac{1^{st} (f (m))}{C} = \frac{1^{st} (f (n))}{C}$
18		2fveq3	$⊢ m = n \to 2^{nd} (f (m)) = 2^{nd} (f (n))$
19	18	oveq1d	$⊢ m = n \to \frac{2^{nd} (f (m))}{C} = \frac{2^{nd} (f (n))}{C}$
20	17 19	opeq12d	$⊢ m = n \to ⟨\frac{1^{st} (f (m))}{C}, \frac{2^{nd} (f (m))}{C}⟩ = ⟨\frac{1^{st} (f (n))}{C}, \frac{2^{nd} (f (n))}{C}⟩$
21	20	cbvmptv	$⊢ (m \in ℕ ⟼ ⟨\frac{1^{st} (f (m))}{C}, \frac{2^{nd} (f (m))}{C}⟩) = (n \in ℕ ⟼ ⟨\frac{1^{st} (f (n))}{C}, \frac{2^{nd} (f (n))}{C}⟩)$
22		elmapi	$⊢ f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
23	22	ad2antrl	$⊢ ((φ \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y))) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
24		simprrl	$⊢ ((φ \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y))) \to A \subseteq ⋃ ran ((.) \circ f)$
25		simplr	$⊢ ((φ \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y))) \to y \in ℝ^{+}$
26		simprrr	$⊢ ((φ \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y))) \to sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y$
27	12 13 14 15 9 21 23 24 25 26	ovolscalem1	$⊢ ((φ \land y \in ℝ^{+}) \land (f \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leq {vol}^{} (A) + C y))) \to {vol}^{} (B) \leq (\frac{{vol}^{} (A)}{C}) + y$
28	11 27	rexlimddv	$⊢ (φ \land y \in ℝ^{+}) \to {vol}^{} (B) \leq (\frac{{vol}^{} (A)}{C}) + y$
29	28	ralrimiva	$⊢ φ \to \forall y \in ℝ^{+} {vol}^{} (B) \leq (\frac{{vol}^{} (A)}{C}) + y$
30		ssrab2	$⊢ \{x \in ℝ \| C x \in A\} \subseteq ℝ$
31	3 30	eqsstrdi	$⊢ φ \to B \subseteq ℝ$
32		ovolcl	$⊢ B \subseteq ℝ \to {vol}^{} (B) \in ℝ^{}$
33	31 32	syl	$⊢ φ \to {vol}^{} (B) \in ℝ^{}$
34	4 2	rerpdivcld	$⊢ φ \to \frac{{vol}^{*} (A)}{C} \in ℝ$
35		xralrple	$⊢ ({vol}^{} (B) \in ℝ^{} \land \frac{{vol}^{} (A)}{C} \in ℝ) \to ({vol}^{} (B) \leq \frac{{vol}^{} (A)}{C} \leftrightarrow \forall y \in ℝ^{+} {vol}^{} (B) \leq (\frac{{vol}^{*} (A)}{C}) + y)$
36	33 34 35	syl2anc	$⊢ φ \to ({vol}^{} (B) \leq \frac{{vol}^{} (A)}{C} \leftrightarrow \forall y \in ℝ^{+} {vol}^{} (B) \leq (\frac{{vol}^{} (A)}{C}) + y)$
37	29 36	mpbird	$⊢ φ \to {vol}^{} (B) \leq \frac{{vol}^{} (A)}{C}$

Metamath Proof Explorer

Theorem ovolscalem2

Proof