ovolscalem1

	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 ℝ$
	ovolsca.5	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	ovolsca.6	$⊢ G = (n \in ℕ ⟼ ⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩)$
	ovolsca.7	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	ovolsca.8	$⊢ φ \to A \subseteq ⋃ ran ((.) \circ F)$
	ovolsca.9	$⊢ φ \to R \in ℝ^{+}$
	ovolsca.10	$⊢ φ \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + C R$
Assertion	ovolscalem1	$⊢ φ \to {vol}^{} (B) \leq (\frac{{vol}^{} (A)}{C}) + R$

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		ovolsca.5	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
6		ovolsca.6	$⊢ G = (n \in ℕ ⟼ ⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩)$
7		ovolsca.7	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
8		ovolsca.8	$⊢ φ \to A \subseteq ⋃ ran ((.) \circ F)$
9		ovolsca.9	$⊢ φ \to R \in ℝ^{+}$
10		ovolsca.10	$⊢ φ \to sup (ran S ℝ^{} <) \leq {vol}^{} (A) + C R$
11		ssrab2	$⊢ \{x \in ℝ \| C x \in A\} \subseteq ℝ$
12	3 11	eqsstrdi	$⊢ φ \to B \subseteq ℝ$
13		ovolcl	$⊢ B \subseteq ℝ \to {vol}^{} (B) \in ℝ^{}$
14	12 13	syl	$⊢ φ \to {vol}^{} (B) \in ℝ^{}$
15		ovolfcl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n)))$
16	7 15	sylan	$⊢ (φ \land n \in ℕ) \to (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land 1^{st} (F (n)) \leq 2^{nd} (F (n)))$
17	16	simp3d	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) \leq 2^{nd} (F (n))$
18	16	simp1d	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) \in ℝ$
19	16	simp2d	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) \in ℝ$
20	2	rpregt0d	$⊢ φ \to (C \in ℝ \land 0 < C)$
21	20	adantr	$⊢ (φ \land n \in ℕ) \to (C \in ℝ \land 0 < C)$
22		lediv1	$⊢ (1^{st} (F (n)) \in ℝ \land 2^{nd} (F (n)) \in ℝ \land (C \in ℝ \land 0 < C)) \to (1^{st} (F (n)) \leq 2^{nd} (F (n)) \leftrightarrow \frac{1^{st} (F (n))}{C} \leq \frac{2^{nd} (F (n))}{C})$
23	18 19 21 22	syl3anc	$⊢ (φ \land n \in ℕ) \to (1^{st} (F (n)) \leq 2^{nd} (F (n)) \leftrightarrow \frac{1^{st} (F (n))}{C} \leq \frac{2^{nd} (F (n))}{C})$
24	17 23	mpbid	$⊢ (φ \land n \in ℕ) \to \frac{1^{st} (F (n))}{C} \leq \frac{2^{nd} (F (n))}{C}$
25		df-br	$⊢ \frac{1^{st} (F (n))}{C} \leq \frac{2^{nd} (F (n))}{C} \leftrightarrow ⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩ \in \leq$
26	24 25	sylib	$⊢ (φ \land n \in ℕ) \to ⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩ \in \leq$
27	2	adantr	$⊢ (φ \land n \in ℕ) \to C \in ℝ^{+}$
28	18 27	rerpdivcld	$⊢ (φ \land n \in ℕ) \to \frac{1^{st} (F (n))}{C} \in ℝ$
29	19 27	rerpdivcld	$⊢ (φ \land n \in ℕ) \to \frac{2^{nd} (F (n))}{C} \in ℝ$
30	28 29	opelxpd	$⊢ (φ \land n \in ℕ) \to ⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩ \in ℝ^{2}$
31	26 30	elind	$⊢ (φ \land n \in ℕ) \to ⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩ \in (\leq \cap ℝ^{2})$
32	31 6	fmptd	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
33		eqid	$⊢ (abs \circ -) \circ G = (abs \circ -) \circ G$
34		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ G)) = seq 1 (+ ((abs \circ -) \circ G))$
35	33 34	ovolsf	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ G)) : ℕ ⟶ [0, +∞)$
36	32 35	syl	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ G)) : ℕ ⟶ [0, +∞)$
37	36	frnd	$⊢ φ \to ran seq 1 (+ ((abs \circ -) \circ G)) \subseteq [0, +∞)$
38		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
39	37 38	sstrdi	$⊢ φ \to ran seq 1 (+ ((abs \circ -) \circ G)) \subseteq ℝ^{*}$
40		supxrcl	$⊢ ran seq 1 (+ ((abs \circ -) \circ G)) \subseteq ℝ^{} \to sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <) \in ℝ^{*}$
41	39 40	syl	$⊢ φ \to sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <) \in ℝ^{}$
42	4 2	rerpdivcld	$⊢ φ \to \frac{{vol}^{*} (A)}{C} \in ℝ$
43	9	rpred	$⊢ φ \to R \in ℝ$
44	42 43	readdcld	$⊢ φ \to (\frac{{vol}^{*} (A)}{C}) + R \in ℝ$
45	44	rexrd	$⊢ φ \to (\frac{{vol}^{} (A)}{C}) + R \in ℝ^{}$
46	3	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in \{x \in ℝ \| C x \in A\})$
47		oveq2	$⊢ x = y \to C x = C y$
48	47	eleq1d	$⊢ x = y \to (C x \in A \leftrightarrow C y \in A)$
49	48	elrab	$⊢ y \in \{x \in ℝ \| C x \in A\} \leftrightarrow (y \in ℝ \land C y \in A)$
50	46 49	bitrdi	$⊢ φ \to (y \in B \leftrightarrow (y \in ℝ \land C y \in A))$
51		breq2	$⊢ x = C y \to (1^{st} (F (n)) < x \leftrightarrow 1^{st} (F (n)) < C y)$
52		breq1	$⊢ x = C y \to (x < 2^{nd} (F (n)) \leftrightarrow C y < 2^{nd} (F (n)))$
53	51 52	anbi12d	$⊢ x = C y \to ((1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \leftrightarrow (1^{st} (F (n)) < C y \land C y < 2^{nd} (F (n))))$
54	53	rexbidv	$⊢ x = C y \to (\exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))) \leftrightarrow \exists n \in ℕ (1^{st} (F (n)) < C y \land C y < 2^{nd} (F (n))))$
55		ovolfioo	$⊢ (A \subseteq ℝ \land F : ℕ ⟶ \leq \cap ℝ^{2}) \to (A \subseteq ⋃ ran ((.) \circ F) \leftrightarrow \forall x \in A \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))))$
56	1 7 55	syl2anc	$⊢ φ \to (A \subseteq ⋃ ran ((.) \circ F) \leftrightarrow \forall x \in A \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n))))$
57	8 56	mpbid	$⊢ φ \to \forall x \in A \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n)))$
58	57	adantr	$⊢ (φ \land (y \in ℝ \land C y \in A)) \to \forall x \in A \exists n \in ℕ (1^{st} (F (n)) < x \land x < 2^{nd} (F (n)))$
59		simprr	$⊢ (φ \land (y \in ℝ \land C y \in A)) \to C y \in A$
60	54 58 59	rspcdva	$⊢ (φ \land (y \in ℝ \land C y \in A)) \to \exists n \in ℕ (1^{st} (F (n)) < C y \land C y < 2^{nd} (F (n)))$
61		opex	$⊢ ⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩ \in V$
62	6	fvmpt2	$⊢ (n \in ℕ \land ⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩ \in V) \to G (n) = ⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩$
63	61 62	mpan2	$⊢ n \in ℕ \to G (n) = ⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩$
64	63	fveq2d	$⊢ n \in ℕ \to 1^{st} (G (n)) = 1^{st} (⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩)$
65		ovex	$⊢ \frac{1^{st} (F (n))}{C} \in V$
66		ovex	$⊢ \frac{2^{nd} (F (n))}{C} \in V$
67	65 66	op1st	$⊢ 1^{st} (⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩) = \frac{1^{st} (F (n))}{C}$
68	64 67	eqtrdi	$⊢ n \in ℕ \to 1^{st} (G (n)) = \frac{1^{st} (F (n))}{C}$
69	68	adantl	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to 1^{st} (G (n)) = \frac{1^{st} (F (n))}{C}$
70	69	breq1d	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to (1^{st} (G (n)) < y \leftrightarrow \frac{1^{st} (F (n))}{C} < y)$
71	18	adantlr	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to 1^{st} (F (n)) \in ℝ$
72		simplrl	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to y \in ℝ$
73	21	adantlr	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to (C \in ℝ \land 0 < C)$
74		ltdivmul	$⊢ (1^{st} (F (n)) \in ℝ \land y \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{1^{st} (F (n))}{C} < y \leftrightarrow 1^{st} (F (n)) < C y)$
75	71 72 73 74	syl3anc	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to (\frac{1^{st} (F (n))}{C} < y \leftrightarrow 1^{st} (F (n)) < C y)$
76	70 75	bitr2d	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to (1^{st} (F (n)) < C y \leftrightarrow 1^{st} (G (n)) < y)$
77	19	adantlr	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to 2^{nd} (F (n)) \in ℝ$
78		ltmuldiv2	$⊢ (y \in ℝ \land 2^{nd} (F (n)) \in ℝ \land (C \in ℝ \land 0 < C)) \to (C y < 2^{nd} (F (n)) \leftrightarrow y < \frac{2^{nd} (F (n))}{C})$
79	72 77 73 78	syl3anc	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to (C y < 2^{nd} (F (n)) \leftrightarrow y < \frac{2^{nd} (F (n))}{C})$
80	63	fveq2d	$⊢ n \in ℕ \to 2^{nd} (G (n)) = 2^{nd} (⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩)$
81	65 66	op2nd	$⊢ 2^{nd} (⟨\frac{1^{st} (F (n))}{C}, \frac{2^{nd} (F (n))}{C}⟩) = \frac{2^{nd} (F (n))}{C}$
82	80 81	eqtrdi	$⊢ n \in ℕ \to 2^{nd} (G (n)) = \frac{2^{nd} (F (n))}{C}$
83	82	adantl	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to 2^{nd} (G (n)) = \frac{2^{nd} (F (n))}{C}$
84	83	breq2d	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to (y < 2^{nd} (G (n)) \leftrightarrow y < \frac{2^{nd} (F (n))}{C})$
85	79 84	bitr4d	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to (C y < 2^{nd} (F (n)) \leftrightarrow y < 2^{nd} (G (n)))$
86	76 85	anbi12d	$⊢ ((φ \land (y \in ℝ \land C y \in A)) \land n \in ℕ) \to ((1^{st} (F (n)) < C y \land C y < 2^{nd} (F (n))) \leftrightarrow (1^{st} (G (n)) < y \land y < 2^{nd} (G (n))))$
87	86	rexbidva	$⊢ (φ \land (y \in ℝ \land C y \in A)) \to (\exists n \in ℕ (1^{st} (F (n)) < C y \land C y < 2^{nd} (F (n))) \leftrightarrow \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n))))$
88	60 87	mpbid	$⊢ (φ \land (y \in ℝ \land C y \in A)) \to \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n)))$
89	88	ex	$⊢ φ \to ((y \in ℝ \land C y \in A) \to \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n))))$
90	50 89	sylbid	$⊢ φ \to (y \in B \to \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n))))$
91	90	ralrimiv	$⊢ φ \to \forall y \in B \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n)))$
92		ovolfioo	$⊢ (B \subseteq ℝ \land G : ℕ ⟶ \leq \cap ℝ^{2}) \to (B \subseteq ⋃ ran ((.) \circ G) \leftrightarrow \forall y \in B \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n))))$
93	12 32 92	syl2anc	$⊢ φ \to (B \subseteq ⋃ ran ((.) \circ G) \leftrightarrow \forall y \in B \exists n \in ℕ (1^{st} (G (n)) < y \land y < 2^{nd} (G (n))))$
94	91 93	mpbird	$⊢ φ \to B \subseteq ⋃ ran ((.) \circ G)$
95	34	ovollb	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land B \subseteq ⋃ ran ((.) \circ G)) \to {vol}^{} (B) \leq sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <)$
96	32 94 95	syl2anc	$⊢ φ \to {vol}^{} (B) \leq sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <)$
97		fzfid	$⊢ (φ \land k \in ℕ) \to (1 \dots k) \in Fin$
98	2	rpcnd	$⊢ φ \to C \in ℂ$
99	98	adantr	$⊢ (φ \land k \in ℕ) \to C \in ℂ$
100		simpl	$⊢ (φ \land k \in ℕ) \to φ$
101		elfznn	$⊢ n \in (1 \dots k) \to n \in ℕ$
102	19 18	resubcld	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) - 1^{st} (F (n)) \in ℝ$
103	100 101 102	syl2an	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to 2^{nd} (F (n)) - 1^{st} (F (n)) \in ℝ$
104	103	recnd	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to 2^{nd} (F (n)) - 1^{st} (F (n)) \in ℂ$
105	2	rpne0d	$⊢ φ \to C \neq 0$
106	105	adantr	$⊢ (φ \land k \in ℕ) \to C \neq 0$
107	97 99 104 106	fsumdivc	$⊢ (φ \land k \in ℕ) \to \frac{\sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n)))}{C} = \sum_{n = 1}^{k} (\frac{2^{nd} (F (n)) - 1^{st} (F (n))}{C})$
108	82 68	oveq12d	$⊢ n \in ℕ \to 2^{nd} (G (n)) - 1^{st} (G (n)) = (\frac{2^{nd} (F (n))}{C}) - (\frac{1^{st} (F (n))}{C})$
109	108	adantl	$⊢ (φ \land n \in ℕ) \to 2^{nd} (G (n)) - 1^{st} (G (n)) = (\frac{2^{nd} (F (n))}{C}) - (\frac{1^{st} (F (n))}{C})$
110	33	ovolfsval	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to ((abs \circ -) \circ G) (n) = 2^{nd} (G (n)) - 1^{st} (G (n))$
111	32 110	sylan	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) = 2^{nd} (G (n)) - 1^{st} (G (n))$
112	19	recnd	$⊢ (φ \land n \in ℕ) \to 2^{nd} (F (n)) \in ℂ$
113	18	recnd	$⊢ (φ \land n \in ℕ) \to 1^{st} (F (n)) \in ℂ$
114	2	rpcnne0d	$⊢ φ \to (C \in ℂ \land C \neq 0)$
115	114	adantr	$⊢ (φ \land n \in ℕ) \to (C \in ℂ \land C \neq 0)$
116		divsubdir	$⊢ (2^{nd} (F (n)) \in ℂ \land 1^{st} (F (n)) \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{2^{nd} (F (n)) - 1^{st} (F (n))}{C} = (\frac{2^{nd} (F (n))}{C}) - (\frac{1^{st} (F (n))}{C})$
117	112 113 115 116	syl3anc	$⊢ (φ \land n \in ℕ) \to \frac{2^{nd} (F (n)) - 1^{st} (F (n))}{C} = (\frac{2^{nd} (F (n))}{C}) - (\frac{1^{st} (F (n))}{C})$
118	109 111 117	3eqtr4d	$⊢ (φ \land n \in ℕ) \to ((abs \circ -) \circ G) (n) = \frac{2^{nd} (F (n)) - 1^{st} (F (n))}{C}$
119	100 101 118	syl2an	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to ((abs \circ -) \circ G) (n) = \frac{2^{nd} (F (n)) - 1^{st} (F (n))}{C}$
120		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
121		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
122	120 121	eleqtrdi	$⊢ (φ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
123	102 27	rerpdivcld	$⊢ (φ \land n \in ℕ) \to \frac{2^{nd} (F (n)) - 1^{st} (F (n))}{C} \in ℝ$
124	123	recnd	$⊢ (φ \land n \in ℕ) \to \frac{2^{nd} (F (n)) - 1^{st} (F (n))}{C} \in ℂ$
125	100 101 124	syl2an	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to \frac{2^{nd} (F (n)) - 1^{st} (F (n))}{C} \in ℂ$
126	119 122 125	fsumser	$⊢ (φ \land k \in ℕ) \to \sum_{n = 1}^{k} (\frac{2^{nd} (F (n)) - 1^{st} (F (n))}{C}) = seq 1 (+ ((abs \circ -) \circ G)) (k)$
127	107 126	eqtrd	$⊢ (φ \land k \in ℕ) \to \frac{\sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n)))}{C} = seq 1 (+ ((abs \circ -) \circ G)) (k)$
128		eqid	$⊢ (abs \circ -) \circ F = (abs \circ -) \circ F$
129	128 5	ovolsf	$⊢ F : ℕ ⟶ \leq \cap ℝ^{2} \to S : ℕ ⟶ [0, +∞)$
130	7 129	syl	$⊢ φ \to S : ℕ ⟶ [0, +∞)$
131	130	frnd	$⊢ φ \to ran S \subseteq [0, +∞)$
132	131 38	sstrdi	$⊢ φ \to ran S \subseteq ℝ^{*}$
133	2 9	rpmulcld	$⊢ φ \to C R \in ℝ^{+}$
134	133	rpred	$⊢ φ \to C R \in ℝ$
135	4 134	readdcld	$⊢ φ \to {vol}^{*} (A) + C R \in ℝ$
136	135	rexrd	$⊢ φ \to {vol}^{} (A) + C R \in ℝ^{}$
137		supxrleub	$⊢ (ran S \subseteq ℝ^{} \land {vol}^{} (A) + C R \in ℝ^{}) \to (sup (ran S ℝ^{} <) \leq {vol}^{} (A) + C R \leftrightarrow \forall x \in ran S x \leq {vol}^{} (A) + C R)$
138	132 136 137	syl2anc	$⊢ φ \to (sup (ran S ℝ^{} <) \leq {vol}^{} (A) + C R \leftrightarrow \forall x \in ran S x \leq {vol}^{*} (A) + C R)$
139	10 138	mpbid	$⊢ φ \to \forall x \in ran S x \leq {vol}^{*} (A) + C R$
140	130	ffnd	$⊢ φ \to S Fn ℕ$
141		breq1	$⊢ x = S (k) \to (x \leq {vol}^{} (A) + C R \leftrightarrow S (k) \leq {vol}^{} (A) + C R)$
142	141	ralrn	$⊢ S Fn ℕ \to (\forall x \in ran S x \leq {vol}^{} (A) + C R \leftrightarrow \forall k \in ℕ S (k) \leq {vol}^{} (A) + C R)$
143	140 142	syl	$⊢ φ \to (\forall x \in ran S x \leq {vol}^{} (A) + C R \leftrightarrow \forall k \in ℕ S (k) \leq {vol}^{} (A) + C R)$
144	139 143	mpbid	$⊢ φ \to \forall k \in ℕ S (k) \leq {vol}^{*} (A) + C R$
145	144	r19.21bi	$⊢ (φ \land k \in ℕ) \to S (k) \leq {vol}^{*} (A) + C R$
146	7	adantr	$⊢ (φ \land k \in ℕ) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
147	128	ovolfsval	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to ((abs \circ -) \circ F) (n) = 2^{nd} (F (n)) - 1^{st} (F (n))$
148	146 101 147	syl2an	$⊢ ((φ \land k \in ℕ) \land n \in (1 \dots k)) \to ((abs \circ -) \circ F) (n) = 2^{nd} (F (n)) - 1^{st} (F (n))$
149	148 122 104	fsumser	$⊢ (φ \land k \in ℕ) \to \sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n))) = seq 1 (+ ((abs \circ -) \circ F)) (k)$
150	5	fveq1i	$⊢ S (k) = seq 1 (+ ((abs \circ -) \circ F)) (k)$
151	149 150	eqtr4di	$⊢ (φ \land k \in ℕ) \to \sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n))) = S (k)$
152	42	recnd	$⊢ φ \to \frac{{vol}^{*} (A)}{C} \in ℂ$
153	9	rpcnd	$⊢ φ \to R \in ℂ$
154	98 152 153	adddid	$⊢ φ \to C ((\frac{{vol}^{} (A)}{C}) + R) = C (\frac{{vol}^{} (A)}{C}) + C R$
155	4	recnd	$⊢ φ \to {vol}^{*} (A) \in ℂ$
156	155 98 105	divcan2d	$⊢ φ \to C (\frac{{vol}^{} (A)}{C}) = {vol}^{} (A)$
157	156	oveq1d	$⊢ φ \to C (\frac{{vol}^{} (A)}{C}) + C R = {vol}^{} (A) + C R$
158	154 157	eqtrd	$⊢ φ \to C ((\frac{{vol}^{} (A)}{C}) + R) = {vol}^{} (A) + C R$
159	158	adantr	$⊢ (φ \land k \in ℕ) \to C ((\frac{{vol}^{} (A)}{C}) + R) = {vol}^{} (A) + C R$
160	145 151 159	3brtr4d	$⊢ (φ \land k \in ℕ) \to \sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n))) \leq C ((\frac{{vol}^{*} (A)}{C}) + R)$
161	97 103	fsumrecl	$⊢ (φ \land k \in ℕ) \to \sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n))) \in ℝ$
162	44	adantr	$⊢ (φ \land k \in ℕ) \to (\frac{{vol}^{*} (A)}{C}) + R \in ℝ$
163	20	adantr	$⊢ (φ \land k \in ℕ) \to (C \in ℝ \land 0 < C)$
164		ledivmul	$⊢ (\sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n))) \in ℝ \land (\frac{{vol}^{} (A)}{C}) + R \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{\sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n)))}{C} \leq (\frac{{vol}^{} (A)}{C}) + R \leftrightarrow \sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n))) \leq C ((\frac{{vol}^{*} (A)}{C}) + R))$
165	161 162 163 164	syl3anc	$⊢ (φ \land k \in ℕ) \to (\frac{\sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n)))}{C} \leq (\frac{{vol}^{} (A)}{C}) + R \leftrightarrow \sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n))) \leq C ((\frac{{vol}^{} (A)}{C}) + R))$
166	160 165	mpbird	$⊢ (φ \land k \in ℕ) \to \frac{\sum_{n = 1}^{k} (2^{nd} (F (n)) - 1^{st} (F (n)))}{C} \leq (\frac{{vol}^{*} (A)}{C}) + R$
167	127 166	eqbrtrrd	$⊢ (φ \land k \in ℕ) \to seq 1 (+ ((abs \circ -) \circ G)) (k) \leq (\frac{{vol}^{*} (A)}{C}) + R$
168	167	ralrimiva	$⊢ φ \to \forall k \in ℕ seq 1 (+ ((abs \circ -) \circ G)) (k) \leq (\frac{{vol}^{*} (A)}{C}) + R$
169	36	ffnd	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ G)) Fn ℕ$
170		breq1	$⊢ y = seq 1 (+ ((abs \circ -) \circ G)) (k) \to (y \leq (\frac{{vol}^{} (A)}{C}) + R \leftrightarrow seq 1 (+ ((abs \circ -) \circ G)) (k) \leq (\frac{{vol}^{} (A)}{C}) + R)$
171	170	ralrn	$⊢ seq 1 (+ ((abs \circ -) \circ G)) Fn ℕ \to (\forall y \in ran seq 1 (+ ((abs \circ -) \circ G)) y \leq (\frac{{vol}^{} (A)}{C}) + R \leftrightarrow \forall k \in ℕ seq 1 (+ ((abs \circ -) \circ G)) (k) \leq (\frac{{vol}^{} (A)}{C}) + R)$
172	169 171	syl	$⊢ φ \to (\forall y \in ran seq 1 (+ ((abs \circ -) \circ G)) y \leq (\frac{{vol}^{} (A)}{C}) + R \leftrightarrow \forall k \in ℕ seq 1 (+ ((abs \circ -) \circ G)) (k) \leq (\frac{{vol}^{} (A)}{C}) + R)$
173	168 172	mpbird	$⊢ φ \to \forall y \in ran seq 1 (+ ((abs \circ -) \circ G)) y \leq (\frac{{vol}^{*} (A)}{C}) + R$
174		supxrleub	$⊢ (ran seq 1 (+ ((abs \circ -) \circ G)) \subseteq ℝ^{} \land (\frac{{vol}^{} (A)}{C}) + R \in ℝ^{}) \to (sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <) \leq (\frac{{vol}^{} (A)}{C}) + R \leftrightarrow \forall y \in ran seq 1 (+ ((abs \circ -) \circ G)) y \leq (\frac{{vol}^{} (A)}{C}) + R)$
175	39 45 174	syl2anc	$⊢ φ \to (sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <) \leq (\frac{{vol}^{} (A)}{C}) + R \leftrightarrow \forall y \in ran seq 1 (+ ((abs \circ -) \circ G)) y \leq (\frac{{vol}^{*} (A)}{C}) + R)$
176	173 175	mpbird	$⊢ φ \to sup (ran seq 1 (+ ((abs \circ -) \circ G)) ℝ^{} <) \leq (\frac{{vol}^{} (A)}{C}) + R$
177	14 41 45 96 176	xrletrd	$⊢ φ \to {vol}^{} (B) \leq (\frac{{vol}^{} (A)}{C}) + R$

Metamath Proof Explorer

Theorem ovolscalem1

Proof