mblfinlem2

Description: Lemma for ismblfin , effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different definition of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018) (Revised by Brendan Leahy, 13-Jul-2018)

		Ref	Expression
	Assertion	mblfinlem2	$⊢ (A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{} (s))$

Proof

Step	Hyp	Ref	Expression
1		retop	$⊢ topGen (ran (.)) \in Top$
2		0cld	$⊢ topGen (ran (.)) \in Top \to \emptyset \in Clsd (topGen (ran (.)))$
3	1 2	ax-mp	$⊢ \emptyset \in Clsd (topGen (ran (.)))$
4		simpl3	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land A = \emptyset) \to M < {vol}^{} (A)$
5		fveq2	$⊢ A = \emptyset \to {vol}^{} (A) = {vol}^{} (\emptyset)$
6	5	adantl	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land A = \emptyset) \to {vol}^{} (A) = {vol}^{*} (\emptyset)$
7	4 6	breqtrd	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land A = \emptyset) \to M < {vol}^{} (\emptyset)$
8		0ss	$⊢ \emptyset \subseteq A$
9	7 8	jctil	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land A = \emptyset) \to (\emptyset \subseteq A \land M < {vol}^{} (\emptyset))$
10		sseq1	$⊢ s = \emptyset \to (s \subseteq A \leftrightarrow \emptyset \subseteq A)$
11		fveq2	$⊢ s = \emptyset \to {vol}^{} (s) = {vol}^{} (\emptyset)$
12	11	breq2d	$⊢ s = \emptyset \to (M < {vol}^{} (s) \leftrightarrow M < {vol}^{} (\emptyset))$
13	10 12	anbi12d	$⊢ s = \emptyset \to ((s \subseteq A \land M < {vol}^{} (s)) \leftrightarrow (\emptyset \subseteq A \land M < {vol}^{} (\emptyset)))$
14	13	rspcev	$⊢ (\emptyset \in Clsd (topGen (ran (.))) \land (\emptyset \subseteq A \land M < {vol}^{} (\emptyset))) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{} (s))$
15	3 9 14	sylancr	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land A = \emptyset) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{} (s))$
16		mblfinlem1	$⊢ (A \in topGen (ran (.)) \land A \neq \emptyset) \to \exists f f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
17	16	3ad2antl1	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \land A \neq \emptyset) \to \exists f f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
18		simpl3	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to M < {vol}^{} (A)$
19		f1ofo	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to f : ℕ \underset{onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
20		rnco2	$⊢ ran ([.] \circ f) = [.] [ran f]$
21		forn	$⊢ f : ℕ \underset{onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ran f = \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
22	21	imaeq2d	$⊢ f : ℕ \underset{onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to [.] [ran f] = [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}]$
23	20 22	syl5eq	$⊢ f : ℕ \underset{onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ran ([.] \circ f) = [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}]$
24	23	unieqd	$⊢ f : ℕ \underset{onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ⋃ ran ([.] \circ f) = ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}]$
25	19 24	syl	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ⋃ ran ([.] \circ f) = ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}]$
26	25	adantl	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to ⋃ ran ([.] \circ f) = ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}]$
27		oveq1	$⊢ x = u \to \frac{x}{2^{y}} = \frac{u}{2^{y}}$
28		oveq1	$⊢ x = u \to x + 1 = u + 1$
29	28	oveq1d	$⊢ x = u \to \frac{x + 1}{2^{y}} = \frac{u + 1}{2^{y}}$
30	27 29	opeq12d	$⊢ x = u \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ = ⟨\frac{u}{2^{y}}, \frac{u + 1}{2^{y}}⟩$
31		oveq2	$⊢ y = v \to 2^{y} = 2^{v}$
32	31	oveq2d	$⊢ y = v \to \frac{u}{2^{y}} = \frac{u}{2^{v}}$
33	31	oveq2d	$⊢ y = v \to \frac{u + 1}{2^{y}} = \frac{u + 1}{2^{v}}$
34	32 33	opeq12d	$⊢ y = v \to ⟨\frac{u}{2^{y}}, \frac{u + 1}{2^{y}}⟩ = ⟨\frac{u}{2^{v}}, \frac{u + 1}{2^{v}}⟩$
35	30 34	cbvmpov	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) = (u \in ℤ, v \in ℕ_{0} ⟼ ⟨\frac{u}{2^{v}}, \frac{u + 1}{2^{v}}⟩)$
36		fveq2	$⊢ a = z \to [.] (a) = [.] (z)$
37	36	sseq1d	$⊢ a = z \to ([.] (a) \subseteq [.] (c) \leftrightarrow [.] (z) \subseteq [.] (c))$
38		eqeq1	$⊢ a = z \to (a = c \leftrightarrow z = c)$
39	37 38	imbi12d	$⊢ a = z \to (([.] (a) \subseteq [.] (c) \to a = c) \leftrightarrow ([.] (z) \subseteq [.] (c) \to z = c))$
40	39	ralbidv	$⊢ a = z \to (\forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c) \leftrightarrow \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (z) \subseteq [.] (c) \to z = c))$
41	40	cbvrabv	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} = \{z \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (z) \subseteq [.] (c) \to z = c)\}$
42		ssrab2	$⊢ \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \subseteq ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
43	42	a1i	$⊢ (A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \to \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \subseteq ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
44	35 41 43	dyadmbllem	$⊢ (A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \to ⋃ [.] [\{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}] = ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}]$
45	44	adantr	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to ⋃ [.] [\{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}] = ⋃ [.] [\{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}]$
46	26 45	eqtr4d	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to ⋃ ran ([.] \circ f) = ⋃ [.] [\{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}]$
47		opnmbllem0	$⊢ A \in topGen (ran (.)) \to ⋃ [.] [\{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}] = A$
48	47	3ad2ant1	$⊢ (A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \to ⋃ [.] [\{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}] = A$
49	48	adantr	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to ⋃ [.] [\{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}] = A$
50	46 49	eqtrd	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to ⋃ ran ([.] \circ f) = A$
51	50	fveq2d	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to {vol}^{} (⋃ ran ([.] \circ f)) = {vol}^{*} (A)$
52		f1of	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
53		ssrab2	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}$
54	35	dyadf	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2}$
55		frn	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ \leq \cap ℝ^{2} \to ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq \leq \cap ℝ^{2}$
56	54 55	ax-mp	$⊢ ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq \leq \cap ℝ^{2}$
57	42 56	sstri	$⊢ \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \subseteq \leq \cap ℝ^{2}$
58	53 57	sstri	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq \leq \cap ℝ^{2}$
59		fss	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq \leq \cap ℝ^{2}) \to f : ℕ ⟶ \leq \cap ℝ^{2}$
60	52 58 59	sylancl	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to f : ℕ ⟶ \leq \cap ℝ^{2}$
61	53 42	sstri	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
62		ffvelrn	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to f (m) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
63	61 62	sseldi	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to f (m) \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
64	63	adantrr	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to f (m) \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
65		ffvelrn	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to f (z) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
66	61 65	sseldi	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to f (z) \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
67	66	adantrl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to f (z) \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
68	35	dyaddisj	$⊢ (f (m) \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \land f (z) \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)) \to ([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m)) \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset)$
69	64 67 68	syl2anc	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to ([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m)) \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset)$
70	52 69	sylan	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to ([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m)) \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset)$
71		df-3or	$⊢ ([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m)) \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset) \leftrightarrow (([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m))) \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset)$
72	70 71	sylib	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to (([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m))) \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset)$
73		elrabi	$⊢ f (z) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to f (z) \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}$
74		fveq2	$⊢ a = f (m) \to [.] (a) = [.] (f (m))$
75	74	sseq1d	$⊢ a = f (m) \to ([.] (a) \subseteq [.] (c) \leftrightarrow [.] (f (m)) \subseteq [.] (c))$
76		eqeq1	$⊢ a = f (m) \to (a = c \leftrightarrow f (m) = c)$
77	75 76	imbi12d	$⊢ a = f (m) \to (([.] (a) \subseteq [.] (c) \to a = c) \leftrightarrow ([.] (f (m)) \subseteq [.] (c) \to f (m) = c))$
78	77	ralbidv	$⊢ a = f (m) \to (\forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c) \leftrightarrow \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (f (m)) \subseteq [.] (c) \to f (m) = c))$
79	78	elrab	$⊢ f (m) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \leftrightarrow (f (m) \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \land \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (f (m)) \subseteq [.] (c) \to f (m) = c))$
80	79	simprbi	$⊢ f (m) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (f (m)) \subseteq [.] (c) \to f (m) = c)$
81		fveq2	$⊢ c = f (z) \to [.] (c) = [.] (f (z))$
82	81	sseq2d	$⊢ c = f (z) \to ([.] (f (m)) \subseteq [.] (c) \leftrightarrow [.] (f (m)) \subseteq [.] (f (z)))$
83		eqeq2	$⊢ c = f (z) \to (f (m) = c \leftrightarrow f (m) = f (z))$
84	82 83	imbi12d	$⊢ c = f (z) \to (([.] (f (m)) \subseteq [.] (c) \to f (m) = c) \leftrightarrow ([.] (f (m)) \subseteq [.] (f (z)) \to f (m) = f (z)))$
85	84	rspcva	$⊢ (f (z) \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \land \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (f (m)) \subseteq [.] (c) \to f (m) = c)) \to ([.] (f (m)) \subseteq [.] (f (z)) \to f (m) = f (z))$
86	73 80 85	syl2anr	$⊢ (f (m) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land f (z) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to ([.] (f (m)) \subseteq [.] (f (z)) \to f (m) = f (z))$
87		elrabi	$⊢ f (m) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to f (m) \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\}$
88		fveq2	$⊢ a = f (z) \to [.] (a) = [.] (f (z))$
89	88	sseq1d	$⊢ a = f (z) \to ([.] (a) \subseteq [.] (c) \leftrightarrow [.] (f (z)) \subseteq [.] (c))$
90		eqeq1	$⊢ a = f (z) \to (a = c \leftrightarrow f (z) = c)$
91	89 90	imbi12d	$⊢ a = f (z) \to (([.] (a) \subseteq [.] (c) \to a = c) \leftrightarrow ([.] (f (z)) \subseteq [.] (c) \to f (z) = c))$
92	91	ralbidv	$⊢ a = f (z) \to (\forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c) \leftrightarrow \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (f (z)) \subseteq [.] (c) \to f (z) = c))$
93	92	elrab	$⊢ f (z) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \leftrightarrow (f (z) \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \land \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (f (z)) \subseteq [.] (c) \to f (z) = c))$
94	93	simprbi	$⊢ f (z) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (f (z)) \subseteq [.] (c) \to f (z) = c)$
95		fveq2	$⊢ c = f (m) \to [.] (c) = [.] (f (m))$
96	95	sseq2d	$⊢ c = f (m) \to ([.] (f (z)) \subseteq [.] (c) \leftrightarrow [.] (f (z)) \subseteq [.] (f (m)))$
97		eqeq2	$⊢ c = f (m) \to (f (z) = c \leftrightarrow f (z) = f (m))$
98	96 97	imbi12d	$⊢ c = f (m) \to (([.] (f (z)) \subseteq [.] (c) \to f (z) = c) \leftrightarrow ([.] (f (z)) \subseteq [.] (f (m)) \to f (z) = f (m)))$
99	98	rspcva	$⊢ (f (m) \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \land \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (f (z)) \subseteq [.] (c) \to f (z) = c)) \to ([.] (f (z)) \subseteq [.] (f (m)) \to f (z) = f (m))$
100	87 94 99	syl2an	$⊢ (f (m) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land f (z) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to ([.] (f (z)) \subseteq [.] (f (m)) \to f (z) = f (m))$
101		eqcom	$⊢ f (z) = f (m) \leftrightarrow f (m) = f (z)$
102	100 101	syl6ib	$⊢ (f (m) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land f (z) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to ([.] (f (z)) \subseteq [.] (f (m)) \to f (m) = f (z))$
103	86 102	jaod	$⊢ (f (m) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land f (z) \in \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to (([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m))) \to f (m) = f (z))$
104	62 65 103	syl2an	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \land (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ)) \to (([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m))) \to f (m) = f (z))$
105	104	anandis	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to (([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m))) \to f (m) = f (z))$
106	52 105	sylan	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to (([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m))) \to f (m) = f (z))$
107		f1of1	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to f : ℕ \underset{1-1}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
108		f1veqaeq	$⊢ (f : ℕ \underset{1-1}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to (f (m) = f (z) \to m = z)$
109	107 108	sylan	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to (f (m) = f (z) \to m = z)$
110	106 109	syld	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to (([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m))) \to m = z)$
111	110	orim1d	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to ((([.] (f (m)) \subseteq [.] (f (z)) \lor [.] (f (z)) \subseteq [.] (f (m))) \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset) \to (m = z \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset))$
112	72 111	mpd	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to (m = z \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset)$
113	112	ralrimivva	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to \forall m \in ℕ \forall z \in ℕ (m = z \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset)$
114		eqeq1	$⊢ m = z \to (m = p \leftrightarrow z = p)$
115		2fveq3	$⊢ m = z \to (.) (f (m)) = (.) (f (z))$
116	115	ineq1d	$⊢ m = z \to (.) (f (m)) \cap (.) (f (p)) = (.) (f (z)) \cap (.) (f (p))$
117	116	eqeq1d	$⊢ m = z \to ((.) (f (m)) \cap (.) (f (p)) = \emptyset \leftrightarrow (.) (f (z)) \cap (.) (f (p)) = \emptyset)$
118	114 117	orbi12d	$⊢ m = z \to ((m = p \lor (.) (f (m)) \cap (.) (f (p)) = \emptyset) \leftrightarrow (z = p \lor (.) (f (z)) \cap (.) (f (p)) = \emptyset))$
119	118	ralbidv	$⊢ m = z \to (\forall p \in ℕ (m = p \lor (.) (f (m)) \cap (.) (f (p)) = \emptyset) \leftrightarrow \forall p \in ℕ (z = p \lor (.) (f (z)) \cap (.) (f (p)) = \emptyset))$
120	119	cbvralvw	$⊢ \forall m \in ℕ \forall p \in ℕ (m = p \lor (.) (f (m)) \cap (.) (f (p)) = \emptyset) \leftrightarrow \forall z \in ℕ \forall p \in ℕ (z = p \lor (.) (f (z)) \cap (.) (f (p)) = \emptyset)$
121		eqeq2	$⊢ z = p \to (m = z \leftrightarrow m = p)$
122		2fveq3	$⊢ z = p \to (.) (f (z)) = (.) (f (p))$
123	122	ineq2d	$⊢ z = p \to (.) (f (m)) \cap (.) (f (z)) = (.) (f (m)) \cap (.) (f (p))$
124	123	eqeq1d	$⊢ z = p \to ((.) (f (m)) \cap (.) (f (z)) = \emptyset \leftrightarrow (.) (f (m)) \cap (.) (f (p)) = \emptyset)$
125	121 124	orbi12d	$⊢ z = p \to ((m = z \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset) \leftrightarrow (m = p \lor (.) (f (m)) \cap (.) (f (p)) = \emptyset))$
126	125	cbvralvw	$⊢ \forall z \in ℕ (m = z \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset) \leftrightarrow \forall p \in ℕ (m = p \lor (.) (f (m)) \cap (.) (f (p)) = \emptyset)$
127	126	ralbii	$⊢ \forall m \in ℕ \forall z \in ℕ (m = z \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset) \leftrightarrow \forall m \in ℕ \forall p \in ℕ (m = p \lor (.) (f (m)) \cap (.) (f (p)) = \emptyset)$
128	122	disjor	$⊢ \underset{z \in ℕ}{Disj} (.) (f (z)) \leftrightarrow \forall z \in ℕ \forall p \in ℕ (z = p \lor (.) (f (z)) \cap (.) (f (p)) = \emptyset)$
129	120 127 128	3bitr4ri	$⊢ \underset{z \in ℕ}{Disj} (.) (f (z)) \leftrightarrow \forall m \in ℕ \forall z \in ℕ (m = z \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset)$
130	113 129	sylibr	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to \underset{z \in ℕ}{Disj} (.) (f (z))$
131		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ f)) = seq 1 (+ ((abs \circ -) \circ f))$
132	60 130 131	uniiccvol	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to {vol}^{} (⋃ ran ([.] \circ f)) = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)$
133	132	adantl	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to {vol}^{} (⋃ ran ([.] \circ f)) = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
134	51 133	eqtr3d	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to {vol}^{} (A) = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <)$
135	18 134	breqtrd	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to M < sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)$
136		absf	$⊢ abs : ℂ ⟶ ℝ$
137		subf	$⊢ - : ℂ \times ℂ ⟶ ℂ$
138		fco	$⊢ (abs : ℂ ⟶ ℝ \land - : ℂ \times ℂ ⟶ ℂ) \to (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
139	136 137 138	mp2an	$⊢ (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
140		zre	$⊢ x \in ℤ \to x \in ℝ$
141		2re	$⊢ 2 \in ℝ$
142		reexpcl	$⊢ (2 \in ℝ \land y \in ℕ_{0}) \to 2^{y} \in ℝ$
143	141 142	mpan	$⊢ y \in ℕ_{0} \to 2^{y} \in ℝ$
144		2cn	$⊢ 2 \in ℂ$
145		2ne0	$⊢ 2 \neq 0$
146		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
147		expne0i	$⊢ (2 \in ℂ \land 2 \neq 0 \land y \in ℤ) \to 2^{y} \neq 0$
148	144 145 146 147	mp3an12i	$⊢ y \in ℕ_{0} \to 2^{y} \neq 0$
149	143 148	jca	$⊢ y \in ℕ_{0} \to (2^{y} \in ℝ \land 2^{y} \neq 0)$
150		redivcl	$⊢ (x \in ℝ \land 2^{y} \in ℝ \land 2^{y} \neq 0) \to \frac{x}{2^{y}} \in ℝ$
151		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
152		redivcl	$⊢ (x + 1 \in ℝ \land 2^{y} \in ℝ \land 2^{y} \neq 0) \to \frac{x + 1}{2^{y}} \in ℝ$
153	151 152	syl3an1	$⊢ (x \in ℝ \land 2^{y} \in ℝ \land 2^{y} \neq 0) \to \frac{x + 1}{2^{y}} \in ℝ$
154	150 153	opelxpd	$⊢ (x \in ℝ \land 2^{y} \in ℝ \land 2^{y} \neq 0) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2}$
155	154	3expb	$⊢ (x \in ℝ \land (2^{y} \in ℝ \land 2^{y} \neq 0)) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2}$
156	140 149 155	syl2an	$⊢ (x \in ℤ \land y \in ℕ_{0}) \to ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2}$
157	156	rgen2	$⊢ \forall x \in ℤ \forall y \in ℕ_{0} ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2}$
158		eqid	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) = (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩)$
159	158	fmpo	$⊢ \forall x \in ℤ \forall y \in ℕ_{0} ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩ \in ℝ^{2} \leftrightarrow (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ ℝ^{2}$
160	157 159	mpbi	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ ℝ^{2}$
161		frn	$⊢ (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) : ℤ \times ℕ_{0} ⟶ ℝ^{2} \to ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq ℝ^{2}$
162	160 161	ax-mp	$⊢ ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \subseteq ℝ^{2}$
163	42 162	sstri	$⊢ \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \subseteq ℝ^{2}$
164	53 163	sstri	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℝ^{2}$
165		ax-resscn	$⊢ ℝ \subseteq ℂ$
166		xpss12	$⊢ (ℝ \subseteq ℂ \land ℝ \subseteq ℂ) \to ℝ^{2} \subseteq ℂ \times ℂ$
167	165 165 166	mp2an	$⊢ ℝ^{2} \subseteq ℂ \times ℂ$
168	164 167	sstri	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℂ \times ℂ$
169		fss	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℂ \times ℂ) \to f : ℕ ⟶ ℂ \times ℂ$
170	168 169	mpan2	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to f : ℕ ⟶ ℂ \times ℂ$
171		fco	$⊢ ((abs \circ -) : ℂ \times ℂ ⟶ ℝ \land f : ℕ ⟶ ℂ \times ℂ) \to ((abs \circ -) \circ f) : ℕ ⟶ ℝ$
172	139 170 171	sylancr	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ((abs \circ -) \circ f) : ℕ ⟶ ℝ$
173		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
174		1z	$⊢ 1 \in ℤ$
175	174	a1i	$⊢ ((abs \circ -) \circ f) : ℕ ⟶ ℝ \to 1 \in ℤ$
176		ffvelrn	$⊢ (((abs \circ -) \circ f) : ℕ ⟶ ℝ \land n \in ℕ) \to ((abs \circ -) \circ f) (n) \in ℝ$
177	173 175 176	serfre	$⊢ ((abs \circ -) \circ f) : ℕ ⟶ ℝ \to seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ ℝ$
178		frn	$⊢ seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ ℝ \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ$
179		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
180	178 179	sstrdi	$⊢ seq 1 (+ ((abs \circ -) \circ f)) : ℕ ⟶ ℝ \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{*}$
181	52 172 177 180	4syl	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{*}$
182		rexr	$⊢ M \in ℝ \to M \in ℝ^{*}$
183	182	3ad2ant2	$⊢ (A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \to M \in ℝ^{}$
184		supxrlub	$⊢ (ran seq 1 (+ ((abs \circ -) \circ f)) \subseteq ℝ^{} \land M \in ℝ^{}) \to (M < sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <) \leftrightarrow \exists z \in ran seq 1 (+ ((abs \circ -) \circ f)) M < z)$
185	181 183 184	syl2anr	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to (M < sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <) \leftrightarrow \exists z \in ran seq 1 (+ ((abs \circ -) \circ f)) M < z)$
186	135 185	mpbid	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to \exists z \in ran seq 1 (+ ((abs \circ -) \circ f)) M < z$
187		seqfn	$⊢ 1 \in ℤ \to seq 1 (+ ((abs \circ -) \circ f)) Fn ℤ_{\geq 1}$
188	174 187	ax-mp	$⊢ seq 1 (+ ((abs \circ -) \circ f)) Fn ℤ_{\geq 1}$
189	173	fneq2i	$⊢ seq 1 (+ ((abs \circ -) \circ f)) Fn ℕ \leftrightarrow seq 1 (+ ((abs \circ -) \circ f)) Fn ℤ_{\geq 1}$
190	188 189	mpbir	$⊢ seq 1 (+ ((abs \circ -) \circ f)) Fn ℕ$
191		breq2	$⊢ z = seq 1 (+ ((abs \circ -) \circ f)) (n) \to (M < z \leftrightarrow M < seq 1 (+ ((abs \circ -) \circ f)) (n))$
192	191	rexrn	$⊢ seq 1 (+ ((abs \circ -) \circ f)) Fn ℕ \to (\exists z \in ran seq 1 (+ ((abs \circ -) \circ f)) M < z \leftrightarrow \exists n \in ℕ M < seq 1 (+ ((abs \circ -) \circ f)) (n))$
193	190 192	ax-mp	$⊢ \exists z \in ran seq 1 (+ ((abs \circ -) \circ f)) M < z \leftrightarrow \exists n \in ℕ M < seq 1 (+ ((abs \circ -) \circ f)) (n)$
194	186 193	sylib	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{*} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to \exists n \in ℕ M < seq 1 (+ ((abs \circ -) \circ f)) (n)$
195	60	ffvelrnda	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to f (z) \in (\leq \cap ℝ^{2})$
196		0le0	$⊢ 0 \leq 0$
197		df-br	$⊢ 0 \leq 0 \leftrightarrow ⟨0, 0⟩ \in \leq$
198	196 197	mpbi	$⊢ ⟨0, 0⟩ \in \leq$
199		0re	$⊢ 0 \in ℝ$
200		opelxpi	$⊢ (0 \in ℝ \land 0 \in ℝ) \to ⟨0, 0⟩ \in ℝ^{2}$
201	199 199 200	mp2an	$⊢ ⟨0, 0⟩ \in ℝ^{2}$
202		elin	$⊢ ⟨0, 0⟩ \in (\leq \cap ℝ^{2}) \leftrightarrow (⟨0, 0⟩ \in \leq \land ⟨0, 0⟩ \in ℝ^{2})$
203	198 201 202	mpbir2an	$⊢ ⟨0, 0⟩ \in (\leq \cap ℝ^{2})$
204		ifcl	$⊢ (f (z) \in (\leq \cap ℝ^{2}) \land ⟨0, 0⟩ \in (\leq \cap ℝ^{2})) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) \in (\leq \cap ℝ^{2})$
205	195 203 204	sylancl	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) \in (\leq \cap ℝ^{2})$
206	205	fmpttd	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) : ℕ ⟶ \leq \cap ℝ^{2}$
207		df-ov	$⊢ (0, 0) = (.) (⟨0, 0⟩)$
208		iooid	$⊢ (0, 0) = \emptyset$
209	207 208	eqtr3i	$⊢ (.) (⟨0, 0⟩) = \emptyset$
210	209	ineq1i	$⊢ (.) (⟨0, 0⟩) \cap (.) (f (z)) = \emptyset \cap (.) (f (z))$
211		0in	$⊢ \emptyset \cap (.) (f (z)) = \emptyset$
212	210 211	eqtri	$⊢ (.) (⟨0, 0⟩) \cap (.) (f (z)) = \emptyset$
213	212	olci	$⊢ (m = z \lor (.) (⟨0, 0⟩) \cap (.) (f (z)) = \emptyset)$
214		ineq1	$⊢ (.) (f (m)) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \to (.) (f (m)) \cap (.) (f (z)) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z))$
215	214	eqeq1d	$⊢ (.) (f (m)) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \to ((.) (f (m)) \cap (.) (f (z)) = \emptyset \leftrightarrow if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z)) = \emptyset)$
216	215	orbi2d	$⊢ (.) (f (m)) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \to ((m = z \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset) \leftrightarrow (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z)) = \emptyset))$
217		ineq1	$⊢ (.) (⟨0, 0⟩) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \to (.) (⟨0, 0⟩) \cap (.) (f (z)) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z))$
218	217	eqeq1d	$⊢ (.) (⟨0, 0⟩) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \to ((.) (⟨0, 0⟩) \cap (.) (f (z)) = \emptyset \leftrightarrow if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z)) = \emptyset)$
219	218	orbi2d	$⊢ (.) (⟨0, 0⟩) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \to ((m = z \lor (.) (⟨0, 0⟩) \cap (.) (f (z)) = \emptyset) \leftrightarrow (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z)) = \emptyset))$
220	216 219	ifboth	$⊢ ((m = z \lor (.) (f (m)) \cap (.) (f (z)) = \emptyset) \land (m = z \lor (.) (⟨0, 0⟩) \cap (.) (f (z)) = \emptyset)) \to (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z)) = \emptyset)$
221	112 213 220	sylancl	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z)) = \emptyset)$
222	209	ineq2i	$⊢ if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (⟨0, 0⟩) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap \emptyset$
223		in0	$⊢ if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap \emptyset = \emptyset$
224	222 223	eqtri	$⊢ if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (⟨0, 0⟩) = \emptyset$
225	224	olci	$⊢ (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (⟨0, 0⟩) = \emptyset)$
226		ineq2	$⊢ (.) (f (z)) = if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) \to if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z)) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩))$
227	226	eqeq1d	$⊢ (.) (f (z)) = if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) \to (if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z)) = \emptyset \leftrightarrow if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) = \emptyset)$
228	227	orbi2d	$⊢ (.) (f (z)) = if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) \to ((m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z)) = \emptyset) \leftrightarrow (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) = \emptyset))$
229		ineq2	$⊢ (.) (⟨0, 0⟩) = if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) \to if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (⟨0, 0⟩) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩))$
230	229	eqeq1d	$⊢ (.) (⟨0, 0⟩) = if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) \to (if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (⟨0, 0⟩) = \emptyset \leftrightarrow if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) = \emptyset)$
231	230	orbi2d	$⊢ (.) (⟨0, 0⟩) = if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) \to ((m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (⟨0, 0⟩) = \emptyset) \leftrightarrow (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) = \emptyset))$
232	228 231	ifboth	$⊢ ((m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (f (z)) = \emptyset) \land (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap (.) (⟨0, 0⟩) = \emptyset)) \to (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) = \emptyset)$
233	221 225 232	sylancl	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (m \in ℕ \land z \in ℕ)) \to (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) = \emptyset)$
234	233	ralrimivva	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to \forall m \in ℕ \forall z \in ℕ (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) = \emptyset)$
235		disjeq2	$⊢ \forall m \in ℕ (.) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m)) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \to (\underset{m \in ℕ}{Disj} (.) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m)) \leftrightarrow \underset{m \in ℕ}{Disj} if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)))$
236		eleq1w	$⊢ z = m \to (z \in (1 \dots n) \leftrightarrow m \in (1 \dots n))$
237		fveq2	$⊢ z = m \to f (z) = f (m)$
238	236 237	ifbieq1d	$⊢ z = m \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) = if (m \in (1 \dots n), f (m), ⟨0, 0⟩)$
239		eqid	$⊢ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))$
240		fvex	$⊢ f (m) \in V$
241		opex	$⊢ ⟨0, 0⟩ \in V$
242	240 241	ifex	$⊢ if (m \in (1 \dots n), f (m), ⟨0, 0⟩) \in V$
243	238 239 242	fvmpt	$⊢ m \in ℕ \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m) = if (m \in (1 \dots n), f (m), ⟨0, 0⟩)$
244	243	fveq2d	$⊢ m \in ℕ \to (.) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m)) = (.) (if (m \in (1 \dots n), f (m), ⟨0, 0⟩))$
245		fvif	$⊢ (.) (if (m \in (1 \dots n), f (m), ⟨0, 0⟩)) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩))$
246	244 245	eqtrdi	$⊢ m \in ℕ \to (.) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m)) = if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩))$
247	235 246	mprg	$⊢ \underset{m \in ℕ}{Disj} (.) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m)) \leftrightarrow \underset{m \in ℕ}{Disj} if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩))$
248		eleq1w	$⊢ m = z \to (m \in (1 \dots n) \leftrightarrow z \in (1 \dots n))$
249	248 115	ifbieq1d	$⊢ m = z \to if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) = if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩))$
250	249	disjor	$⊢ \underset{m \in ℕ}{Disj} if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \leftrightarrow \forall m \in ℕ \forall z \in ℕ (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) = \emptyset)$
251	247 250	bitri	$⊢ \underset{m \in ℕ}{Disj} (.) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m)) \leftrightarrow \forall m \in ℕ \forall z \in ℕ (m = z \lor if (m \in (1 \dots n), (.) (f (m)), (.) (⟨0, 0⟩)) \cap if (z \in (1 \dots n), (.) (f (z)), (.) (⟨0, 0⟩)) = \emptyset)$
252	234 251	sylibr	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to \underset{m \in ℕ}{Disj} (.) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m))$
253		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) = seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))))$
254	206 252 253	uniiccvol	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to {vol}^{} (⋃ ran ([.] \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) = sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) ℝ^{} <)$
255	254	adantr	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to {vol}^{} (⋃ ran ([.] \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) = sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) ℝ^{} <)$
256		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
257	164 256	sstri	$⊢ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \subseteq ℝ^{} \times ℝ^{}$
258	257 65	sseldi	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to f (z) \in (ℝ^{} \times ℝ^{})$
259		0xr	$⊢ 0 \in ℝ^{*}$
260		opelxpi	$⊢ (0 \in ℝ^{} \land 0 \in ℝ^{}) \to ⟨0, 0⟩ \in (ℝ^{} \times ℝ^{})$
261	259 259 260	mp2an	$⊢ ⟨0, 0⟩ \in (ℝ^{} \times ℝ^{})$
262		ifcl	$⊢ (f (z) \in (ℝ^{} \times ℝ^{}) \land ⟨0, 0⟩ \in (ℝ^{} \times ℝ^{})) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) \in (ℝ^{} \times ℝ^{})$
263	258 261 262	sylancl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) \in (ℝ^{} \times ℝ^{})$
264		eqidd	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))$
265		iccf	$⊢ [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
266	265	a1i	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to [.] : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
267	266	feqmptd	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to [.] = (m \in (ℝ^{} \times ℝ^{}) ⟼ [.] (m))$
268		fveq2	$⊢ m = if (z \in (1 \dots n), f (z), ⟨0, 0⟩) \to [.] (m) = [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩))$
269	263 264 267 268	fmptco	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to [.] \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = (z \in ℕ ⟼ [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))$
270	52 269	syl	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to [.] \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = (z \in ℕ ⟼ [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))$
271	270	rneqd	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ran ([.] \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) = ran (z \in ℕ ⟼ [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))$
272	271	unieqd	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ⋃ ran ([.] \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) = ⋃ ran (z \in ℕ ⟼ [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))$
273		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
274	273 173	eleqtrdi	$⊢ n \in ℕ \to n + 1 \in ℤ_{\geq 1}$
275		fzouzsplit	$⊢ n + 1 \in ℤ_{\geq 1} \to ℤ_{\geq 1} = (1 ..^n + 1) \cup ℤ_{\geq (n + 1)}$
276	274 275	syl	$⊢ n \in ℕ \to ℤ_{\geq 1} = (1 ..^n + 1) \cup ℤ_{\geq (n + 1)}$
277	173 276	syl5eq	$⊢ n \in ℕ \to ℕ = (1 ..^n + 1) \cup ℤ_{\geq (n + 1)}$
278		nnz	$⊢ n \in ℕ \to n \in ℤ$
279		fzval3	$⊢ n \in ℤ \to (1 \dots n) = (1 ..^n + 1)$
280	278 279	syl	$⊢ n \in ℕ \to (1 \dots n) = (1 ..^n + 1)$
281	280	uneq1d	$⊢ n \in ℕ \to (1 \dots n) \cup ℤ_{\geq (n + 1)} = (1 ..^n + 1) \cup ℤ_{\geq (n + 1)}$
282	277 281	eqtr4d	$⊢ n \in ℕ \to ℕ = (1 \dots n) \cup ℤ_{\geq (n + 1)}$
283		fvif	$⊢ [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩))$
284	283	a1i	$⊢ n \in ℕ \to [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩))$
285	282 284	iuneq12d	$⊢ n \in ℕ \to ⋃_{z \in ℕ} [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = ⋃_{z \in (1 \dots n) \cup ℤ_{\geq (n + 1)}} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩))$
286		fvex	$⊢ [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) \in V$
287	286	dfiun3	$⊢ ⋃_{z \in ℕ} [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = ⋃ ran (z \in ℕ ⟼ [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))$
288		iunxun	$⊢ ⋃_{z \in (1 \dots n) \cup ℤ_{\geq (n + 1)}} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩)) = ⋃_{z = 1}^{n} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩)) \cup ⋃_{z \in ℤ_{\geq (n + 1)}} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩))$
289	285 287 288	3eqtr3g	$⊢ n \in ℕ \to ⋃ ran (z \in ℕ ⟼ [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) = ⋃_{z = 1}^{n} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩)) \cup ⋃_{z \in ℤ_{\geq (n + 1)}} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩))$
290		iftrue	$⊢ z \in (1 \dots n) \to if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩)) = [.] (f (z))$
291	290	iuneq2i	$⊢ ⋃_{z = 1}^{n} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩)) = ⋃_{z = 1}^{n} [.] (f (z))$
292	291	a1i	$⊢ n \in ℕ \to ⋃_{z = 1}^{n} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩)) = ⋃_{z = 1}^{n} [.] (f (z))$
293		uznfz	$⊢ z \in ℤ_{\geq (n + 1)} \to \neg z \in (1 \dots n + 1 - 1)$
294	293	adantl	$⊢ (n \in ℕ \land z \in ℤ_{\geq (n + 1)}) \to \neg z \in (1 \dots n + 1 - 1)$
295		nncn	$⊢ n \in ℕ \to n \in ℂ$
296		ax-1cn	$⊢ 1 \in ℂ$
297		pncan	$⊢ (n \in ℂ \land 1 \in ℂ) \to n + 1 - 1 = n$
298	295 296 297	sylancl	$⊢ n \in ℕ \to n + 1 - 1 = n$
299	298	oveq2d	$⊢ n \in ℕ \to (1 \dots n + 1 - 1) = (1 \dots n)$
300	299	eleq2d	$⊢ n \in ℕ \to (z \in (1 \dots n + 1 - 1) \leftrightarrow z \in (1 \dots n))$
301	300	notbid	$⊢ n \in ℕ \to (\neg z \in (1 \dots n + 1 - 1) \leftrightarrow \neg z \in (1 \dots n))$
302	301	adantr	$⊢ (n \in ℕ \land z \in ℤ_{\geq (n + 1)}) \to (\neg z \in (1 \dots n + 1 - 1) \leftrightarrow \neg z \in (1 \dots n))$
303	294 302	mpbid	$⊢ (n \in ℕ \land z \in ℤ_{\geq (n + 1)}) \to \neg z \in (1 \dots n)$
304	303	iffalsed	$⊢ (n \in ℕ \land z \in ℤ_{\geq (n + 1)}) \to if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩)) = [.] (⟨0, 0⟩)$
305	304	iuneq2dv	$⊢ n \in ℕ \to ⋃_{z \in ℤ_{\geq (n + 1)}} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩)) = ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩)$
306	292 305	uneq12d	$⊢ n \in ℕ \to ⋃_{z = 1}^{n} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩)) \cup ⋃_{z \in ℤ_{\geq (n + 1)}} if (z \in (1 \dots n), [.] (f (z)), [.] (⟨0, 0⟩)) = ⋃_{z = 1}^{n} [.] (f (z)) \cup ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩)$
307	289 306	eqtrd	$⊢ n \in ℕ \to ⋃ ran (z \in ℕ ⟼ [.] (if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) = ⋃_{z = 1}^{n} [.] (f (z)) \cup ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩)$
308	272 307	sylan9eq	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to ⋃ ran ([.] \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) = ⋃_{z = 1}^{n} [.] (f (z)) \cup ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩)$
309	308	fveq2d	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to {vol}^{} (⋃ ran ([.] \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) = {vol}^{} (⋃_{z = 1}^{n} [.] (f (z)) \cup ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩))$
310		xrltso	$⊢ < Or ℝ^{*}$
311	310	a1i	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to < Or ℝ^{*}$
312		elnnuz	$⊢ n \in ℕ \leftrightarrow n \in ℤ_{\geq 1}$
313	312	biimpi	$⊢ n \in ℕ \to n \in ℤ_{\geq 1}$
314	313	adantl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to n \in ℤ_{\geq 1}$
315		elfznn	$⊢ u \in (1 \dots n) \to u \in ℕ$
316	172	ffvelrnda	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land u \in ℕ) \to ((abs \circ -) \circ f) (u) \in ℝ$
317	315 316	sylan2	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land u \in (1 \dots n)) \to ((abs \circ -) \circ f) (u) \in ℝ$
318	317	adantlr	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land u \in (1 \dots n)) \to ((abs \circ -) \circ f) (u) \in ℝ$
319		readdcl	$⊢ (u \in ℝ \land v \in ℝ) \to u + v \in ℝ$
320	319	adantl	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land (u \in ℝ \land v \in ℝ)) \to u + v \in ℝ$
321	314 318 320	seqcl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ f)) (n) \in ℝ$
322	321	rexrd	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ f)) (n) \in ℝ^{*}$
323		eqidd	$⊢ m \in (1 \dots n) \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))$
324		iftrue	$⊢ m \in (1 \dots n) \to if (m \in (1 \dots n), f (m), ⟨0, 0⟩) = f (m)$
325	238 324	sylan9eqr	$⊢ (m \in (1 \dots n) \land z = m) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) = f (m)$
326		elfznn	$⊢ m \in (1 \dots n) \to m \in ℕ$
327	240	a1i	$⊢ m \in (1 \dots n) \to f (m) \in V$
328	323 325 326 327	fvmptd	$⊢ m \in (1 \dots n) \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m) = f (m)$
329	328	adantl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in (1 \dots n)) \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m) = f (m)$
330	329	fveq2d	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in (1 \dots n)) \to (abs \circ -) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m)) = (abs \circ -) (f (m))$
331		fvex	$⊢ f (z) \in V$
332	331 241	ifex	$⊢ if (z \in (1 \dots n), f (z), ⟨0, 0⟩) \in V$
333	332 239	fnmpti	$⊢ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) Fn ℕ$
334		fvco2	$⊢ ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) Fn ℕ \land m \in ℕ) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = (abs \circ -) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m))$
335	333 326 334	sylancr	$⊢ m \in (1 \dots n) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = (abs \circ -) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m))$
336	335	adantl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in (1 \dots n)) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = (abs \circ -) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m))$
337		ffn	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to f Fn ℕ$
338		fvco2	$⊢ (f Fn ℕ \land m \in ℕ) \to ((abs \circ -) \circ f) (m) = (abs \circ -) (f (m))$
339	337 326 338	syl2an	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in (1 \dots n)) \to ((abs \circ -) \circ f) (m) = (abs \circ -) (f (m))$
340	330 336 339	3eqtr4d	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in (1 \dots n)) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = ((abs \circ -) \circ f) (m)$
341	340	adantlr	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land m \in (1 \dots n)) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = ((abs \circ -) \circ f) (m)$
342	314 341	seqfveq	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (n) = seq 1 (+ ((abs \circ -) \circ f)) (n)$
343	174	a1i	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to 1 \in ℤ$
344	168 65	sseldi	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to f (z) \in (ℂ \times ℂ)$
345		0cn	$⊢ 0 \in ℂ$
346		opelxpi	$⊢ (0 \in ℂ \land 0 \in ℂ) \to ⟨0, 0⟩ \in (ℂ \times ℂ)$
347	345 345 346	mp2an	$⊢ ⟨0, 0⟩ \in (ℂ \times ℂ)$
348		ifcl	$⊢ (f (z) \in (ℂ \times ℂ) \land ⟨0, 0⟩ \in (ℂ \times ℂ)) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) \in (ℂ \times ℂ)$
349	344 347 348	sylancl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) \in (ℂ \times ℂ)$
350	349	fmpttd	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) : ℕ ⟶ ℂ \times ℂ$
351		fco	$⊢ ((abs \circ -) : ℂ \times ℂ ⟶ ℝ \land (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) : ℕ ⟶ ℂ \times ℂ) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) : ℕ ⟶ ℝ$
352	139 350 351	sylancr	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) : ℕ ⟶ ℝ$
353	352	ffvelrnda	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) \in ℝ$
354	173 343 353	serfre	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) : ℕ ⟶ ℝ$
355	354	ffnd	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) Fn ℕ$
356		fnfvelrn	$⊢ (seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) Fn ℕ \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (n) \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))))$
357	355 356	sylan	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (n) \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))))$
358	342 357	eqeltrrd	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ f)) (n) \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))))$
359	354	frnd	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) \subseteq ℝ$
360	359	adantr	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) \subseteq ℝ$
361	360	sselda	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land m \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))))) \to m \in ℝ$
362	321	adantr	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land m \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))))) \to seq 1 (+ ((abs \circ -) \circ f)) (n) \in ℝ$
363		readdcl	$⊢ (m \in ℝ \land u \in ℝ) \to m + u \in ℝ$
364	363	adantl	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \land (m \in ℝ \land u \in ℝ)) \to m + u \in ℝ$
365		recn	$⊢ m \in ℝ \to m \in ℂ$
366		recn	$⊢ u \in ℝ \to u \in ℂ$
367		recn	$⊢ v \in ℝ \to v \in ℂ$
368		addass	$⊢ (m \in ℂ \land u \in ℂ \land v \in ℂ) \to m + u + v = m + u + v$
369	365 366 367 368	syl3an	$⊢ (m \in ℝ \land u \in ℝ \land v \in ℝ) \to m + u + v = m + u + v$
370	369	adantl	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \land (m \in ℝ \land u \in ℝ \land v \in ℝ)) \to m + u + v = m + u + v$
371		nnltp1le	$⊢ (n \in ℕ \land t \in ℕ) \to (n < t \leftrightarrow n + 1 \leq t)$
372	371	biimpa	$⊢ ((n \in ℕ \land t \in ℕ) \land n < t) \to n + 1 \leq t$
373	273	nnzd	$⊢ n \in ℕ \to n + 1 \in ℤ$
374		nnz	$⊢ t \in ℕ \to t \in ℤ$
375		eluz	$⊢ (n + 1 \in ℤ \land t \in ℤ) \to (t \in ℤ_{\geq (n + 1)} \leftrightarrow n + 1 \leq t)$
376	373 374 375	syl2an	$⊢ (n \in ℕ \land t \in ℕ) \to (t \in ℤ_{\geq (n + 1)} \leftrightarrow n + 1 \leq t)$
377	376	adantr	$⊢ ((n \in ℕ \land t \in ℕ) \land n < t) \to (t \in ℤ_{\geq (n + 1)} \leftrightarrow n + 1 \leq t)$
378	372 377	mpbird	$⊢ ((n \in ℕ \land t \in ℕ) \land n < t) \to t \in ℤ_{\geq (n + 1)}$
379	378	adantlll	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to t \in ℤ_{\geq (n + 1)}$
380	313	ad3antlr	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to n \in ℤ_{\geq 1}$
381		simplll	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
382		elfznn	$⊢ m \in (1 \dots t) \to m \in ℕ$
383	381 382 353	syl2an	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \land m \in (1 \dots t)) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) \in ℝ$
384	364 370 379 380 383	seqsplit	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) = seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (n) + seq (n + 1) (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t)$
385	342	ad2antrr	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (n) = seq 1 (+ ((abs \circ -) \circ f)) (n)$
386		elfzelz	$⊢ m \in (n + 1 \dots t) \to m \in ℤ$
387	386	adantl	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to m \in ℤ$
388		0red	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to 0 \in ℝ$
389	273	nnred	$⊢ n \in ℕ \to n + 1 \in ℝ$
390	389	ad3antrrr	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to n + 1 \in ℝ$
391	386	zred	$⊢ m \in (n + 1 \dots t) \to m \in ℝ$
392	391	adantl	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to m \in ℝ$
393	273	nngt0d	$⊢ n \in ℕ \to 0 < n + 1$
394	393	ad3antrrr	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to 0 < n + 1$
395		elfzle1	$⊢ m \in (n + 1 \dots t) \to n + 1 \leq m$
396	395	adantl	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to n + 1 \leq m$
397	388 390 392 394 396	ltletrd	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to 0 < m$
398		elnnz	$⊢ m \in ℕ \leftrightarrow (m \in ℤ \land 0 < m)$
399	387 397 398	sylanbrc	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to m \in ℕ$
400	333 399 334	sylancr	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = (abs \circ -) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m))$
401		eqidd	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))$
402		nnre	$⊢ n \in ℕ \to n \in ℝ$
403	402	adantr	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to n \in ℝ$
404	389	adantr	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to n + 1 \in ℝ$
405	391	adantl	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to m \in ℝ$
406	402	ltp1d	$⊢ n \in ℕ \to n < n + 1$
407	406	adantr	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to n < n + 1$
408	395	adantl	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to n + 1 \leq m$
409	403 404 405 407 408	ltletrd	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to n < m$
410	409	adantr	$⊢ ((n \in ℕ \land m \in (n + 1 \dots t)) \land z = m) \to n < m$
411	403 405	ltnled	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to (n < m \leftrightarrow \neg m \leq n)$
412		breq1	$⊢ m = z \to (m \leq n \leftrightarrow z \leq n)$
413	412	equcoms	$⊢ z = m \to (m \leq n \leftrightarrow z \leq n)$
414	413	notbid	$⊢ z = m \to (\neg m \leq n \leftrightarrow \neg z \leq n)$
415	411 414	sylan9bb	$⊢ ((n \in ℕ \land m \in (n + 1 \dots t)) \land z = m) \to (n < m \leftrightarrow \neg z \leq n)$
416	410 415	mpbid	$⊢ ((n \in ℕ \land m \in (n + 1 \dots t)) \land z = m) \to \neg z \leq n$
417		elfzle2	$⊢ z \in (1 \dots n) \to z \leq n$
418	416 417	nsyl	$⊢ ((n \in ℕ \land m \in (n + 1 \dots t)) \land z = m) \to \neg z \in (1 \dots n)$
419	418	iffalsed	$⊢ ((n \in ℕ \land m \in (n + 1 \dots t)) \land z = m) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) = ⟨0, 0⟩$
420	386	adantl	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to m \in ℤ$
421		0red	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to 0 \in ℝ$
422	393	adantr	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to 0 < n + 1$
423	421 404 405 422 408	ltletrd	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to 0 < m$
424	420 423 398	sylanbrc	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to m \in ℕ$
425	241	a1i	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to ⟨0, 0⟩ \in V$
426	401 419 424 425	fvmptd	$⊢ (n \in ℕ \land m \in (n + 1 \dots t)) \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m) = ⟨0, 0⟩$
427	426	ad4ant14	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m) = ⟨0, 0⟩$
428	427	fveq2d	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to (abs \circ -) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m)) = (abs \circ -) (⟨0, 0⟩)$
429	400 428	eqtrd	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = (abs \circ -) (⟨0, 0⟩)$
430		fvco3	$⊢ (- : ℂ \times ℂ ⟶ ℂ \land ⟨0, 0⟩ \in (ℂ \times ℂ)) \to (abs \circ -) (⟨0, 0⟩) = \|- (⟨0, 0⟩)\|$
431	137 347 430	mp2an	$⊢ (abs \circ -) (⟨0, 0⟩) = \|- (⟨0, 0⟩)\|$
432		df-ov	$⊢ 0 - 0 = - (⟨0, 0⟩)$
433		0m0e0	$⊢ 0 - 0 = 0$
434	432 433	eqtr3i	$⊢ - (⟨0, 0⟩) = 0$
435	434	fveq2i	$⊢ \|- (⟨0, 0⟩)\| = \|0\|$
436		abs0	$⊢ \|0\| = 0$
437	435 436	eqtri	$⊢ \|- (⟨0, 0⟩)\| = 0$
438	431 437	eqtri	$⊢ (abs \circ -) (⟨0, 0⟩) = 0$
439	429 438	eqtrdi	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = 0$
440		elfzuz	$⊢ m \in (n + 1 \dots t) \to m \in ℤ_{\geq (n + 1)}$
441		c0ex	$⊢ 0 \in V$
442	441	fvconst2	$⊢ m \in ℤ_{\geq (n + 1)} \to (ℤ_{\geq (n + 1)} \times \{0\}) (m) = 0$
443	440 442	syl	$⊢ m \in (n + 1 \dots t) \to (ℤ_{\geq (n + 1)} \times \{0\}) (m) = 0$
444	443	adantl	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to (ℤ_{\geq (n + 1)} \times \{0\}) (m) = 0$
445	439 444	eqtr4d	$⊢ (((n \in ℕ \land t \in ℕ) \land n < t) \land m \in (n + 1 \dots t)) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = (ℤ_{\geq (n + 1)} \times \{0\}) (m)$
446	378 445	seqfveq	$⊢ ((n \in ℕ \land t \in ℕ) \land n < t) \to seq (n + 1) (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) = seq (n + 1) (+ (ℤ_{\geq (n + 1)} \times \{0\})) (t)$
447		eqid	$⊢ ℤ_{\geq (n + 1)} = ℤ_{\geq (n + 1)}$
448	447	ser0	$⊢ t \in ℤ_{\geq (n + 1)} \to seq (n + 1) (+ (ℤ_{\geq (n + 1)} \times \{0\})) (t) = 0$
449	378 448	syl	$⊢ ((n \in ℕ \land t \in ℕ) \land n < t) \to seq (n + 1) (+ (ℤ_{\geq (n + 1)} \times \{0\})) (t) = 0$
450	446 449	eqtrd	$⊢ ((n \in ℕ \land t \in ℕ) \land n < t) \to seq (n + 1) (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) = 0$
451	450	adantlll	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq (n + 1) (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) = 0$
452	385 451	oveq12d	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (n) + seq (n + 1) (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) = seq 1 (+ ((abs \circ -) \circ f)) (n) + 0$
453	172	ffvelrnda	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to ((abs \circ -) \circ f) (m) \in ℝ$
454	326 453	sylan2	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in (1 \dots n)) \to ((abs \circ -) \circ f) (m) \in ℝ$
455	454	adantlr	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land m \in (1 \dots n)) \to ((abs \circ -) \circ f) (m) \in ℝ$
456		readdcl	$⊢ (m \in ℝ \land v \in ℝ) \to m + v \in ℝ$
457	456	adantl	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land (m \in ℝ \land v \in ℝ)) \to m + v \in ℝ$
458	314 455 457	seqcl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ f)) (n) \in ℝ$
459	458	ad2antrr	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ f)) (n) \in ℝ$
460	459	recnd	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ f)) (n) \in ℂ$
461	460	addid1d	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ f)) (n) + 0 = seq 1 (+ ((abs \circ -) \circ f)) (n)$
462	452 461	eqtrd	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (n) + seq (n + 1) (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) = seq 1 (+ ((abs \circ -) \circ f)) (n)$
463	384 462	eqtrd	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) = seq 1 (+ ((abs \circ -) \circ f)) (n)$
464	453	ad5ant15	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \land m \in ℕ) \to ((abs \circ -) \circ f) (m) \in ℝ$
465	326 464	sylan2	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \land m \in (1 \dots n)) \to ((abs \circ -) \circ f) (m) \in ℝ$
466	380 465 364	seqcl	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ f)) (n) \in ℝ$
467	466	leidd	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ f)) (n) \leq seq 1 (+ ((abs \circ -) \circ f)) (n)$
468	463 467	eqbrtrd	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land n < t) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) \leq seq 1 (+ ((abs \circ -) \circ f)) (n)$
469		elnnuz	$⊢ t \in ℕ \leftrightarrow t \in ℤ_{\geq 1}$
470	469	biimpi	$⊢ t \in ℕ \to t \in ℤ_{\geq 1}$
471	470	ad2antlr	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \to t \in ℤ_{\geq 1}$
472		eqidd	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) = (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))$
473		simpr	$⊢ (((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \land z = m) \to z = m$
474		elfzle1	$⊢ m \in (1 \dots t) \to 1 \leq m$
475	474	adantl	$⊢ (((n \in ℕ \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to 1 \leq m$
476	382	nnred	$⊢ m \in (1 \dots t) \to m \in ℝ$
477	476	adantl	$⊢ (((n \in ℕ \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to m \in ℝ$
478		nnre	$⊢ t \in ℕ \to t \in ℝ$
479	478	ad3antlr	$⊢ (((n \in ℕ \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to t \in ℝ$
480	402	ad3antrrr	$⊢ (((n \in ℕ \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to n \in ℝ$
481		elfzle2	$⊢ m \in (1 \dots t) \to m \leq t$
482	481	adantl	$⊢ (((n \in ℕ \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to m \leq t$
483		simplr	$⊢ (((n \in ℕ \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to t \leq n$
484	477 479 480 482 483	letrd	$⊢ (((n \in ℕ \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to m \leq n$
485		elfzelz	$⊢ m \in (1 \dots t) \to m \in ℤ$
486	278	ad2antrr	$⊢ ((n \in ℕ \land t \in ℕ) \land t \leq n) \to n \in ℤ$
487		elfz	$⊢ (m \in ℤ \land 1 \in ℤ \land n \in ℤ) \to (m \in (1 \dots n) \leftrightarrow (1 \leq m \land m \leq n))$
488	174 487	mp3an2	$⊢ (m \in ℤ \land n \in ℤ) \to (m \in (1 \dots n) \leftrightarrow (1 \leq m \land m \leq n))$
489	485 486 488	syl2anr	$⊢ (((n \in ℕ \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to (m \in (1 \dots n) \leftrightarrow (1 \leq m \land m \leq n))$
490	475 484 489	mpbir2and	$⊢ (((n \in ℕ \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to m \in (1 \dots n)$
491	490	ad5ant2345	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to m \in (1 \dots n)$
492	491	adantr	$⊢ (((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \land z = m) \to m \in (1 \dots n)$
493	473 492	eqeltrd	$⊢ (((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \land z = m) \to z \in (1 \dots n)$
494		iftrue	$⊢ z \in (1 \dots n) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) = f (z)$
495	493 494	syl	$⊢ (((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \land z = m) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) = f (z)$
496	237	adantl	$⊢ (((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \land z = m) \to f (z) = f (m)$
497	495 496	eqtrd	$⊢ (((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \land z = m) \to if (z \in (1 \dots n), f (z), ⟨0, 0⟩) = f (m)$
498	382	adantl	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to m \in ℕ$
499	240	a1i	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to f (m) \in V$
500	472 497 498 499	fvmptd	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m) = f (m)$
501	500	fveq2d	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to (abs \circ -) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m)) = (abs \circ -) (f (m))$
502	333 382 334	sylancr	$⊢ m \in (1 \dots t) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = (abs \circ -) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m))$
503	502	adantl	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = (abs \circ -) ((z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)) (m))$
504		simplll	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \to f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}$
505		fvco3	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to ((abs \circ -) \circ f) (m) = (abs \circ -) (f (m))$
506	504 382 505	syl2an	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to ((abs \circ -) \circ f) (m) = (abs \circ -) (f (m))$
507	501 503 506	3eqtr4d	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots t)) \to ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))) (m) = ((abs \circ -) \circ f) (m)$
508	471 507	seqfveq	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) = seq 1 (+ ((abs \circ -) \circ f)) (t)$
509		eluz	$⊢ (t \in ℤ \land n \in ℤ) \to (n \in ℤ_{\geq t} \leftrightarrow t \leq n)$
510	374 278 509	syl2anr	$⊢ (n \in ℕ \land t \in ℕ) \to (n \in ℤ_{\geq t} \leftrightarrow t \leq n)$
511	510	biimpar	$⊢ ((n \in ℕ \land t \in ℕ) \land t \leq n) \to n \in ℤ_{\geq t}$
512	511	adantlll	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \to n \in ℤ_{\geq t}$
513	504 326 453	syl2an	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (1 \dots n)) \to ((abs \circ -) \circ f) (m) \in ℝ$
514		elfzelz	$⊢ m \in (t + 1 \dots n) \to m \in ℤ$
515	514	adantl	$⊢ (t \in ℕ \land m \in (t + 1 \dots n)) \to m \in ℤ$
516		0red	$⊢ (t \in ℕ \land m \in (t + 1 \dots n)) \to 0 \in ℝ$
517		peano2nn	$⊢ t \in ℕ \to t + 1 \in ℕ$
518	517	nnred	$⊢ t \in ℕ \to t + 1 \in ℝ$
519	518	adantr	$⊢ (t \in ℕ \land m \in (t + 1 \dots n)) \to t + 1 \in ℝ$
520	514	zred	$⊢ m \in (t + 1 \dots n) \to m \in ℝ$
521	520	adantl	$⊢ (t \in ℕ \land m \in (t + 1 \dots n)) \to m \in ℝ$
522	517	nngt0d	$⊢ t \in ℕ \to 0 < t + 1$
523	522	adantr	$⊢ (t \in ℕ \land m \in (t + 1 \dots n)) \to 0 < t + 1$
524		elfzle1	$⊢ m \in (t + 1 \dots n) \to t + 1 \leq m$
525	524	adantl	$⊢ (t \in ℕ \land m \in (t + 1 \dots n)) \to t + 1 \leq m$
526	516 519 521 523 525	ltletrd	$⊢ (t \in ℕ \land m \in (t + 1 \dots n)) \to 0 < m$
527	515 526 398	sylanbrc	$⊢ (t \in ℕ \land m \in (t + 1 \dots n)) \to m \in ℕ$
528	527	adantlr	$⊢ ((t \in ℕ \land t \leq n) \land m \in (t + 1 \dots n)) \to m \in ℕ$
529	528	adantlll	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (t + 1 \dots n)) \to m \in ℕ$
530	170	ffvelrnda	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to f (m) \in (ℂ \times ℂ)$
531		ffvelrn	$⊢ (- : ℂ \times ℂ ⟶ ℂ \land f (m) \in (ℂ \times ℂ)) \to - (f (m)) \in ℂ$
532	137 530 531	sylancr	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to - (f (m)) \in ℂ$
533	532	absge0d	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to 0 \leq \|- (f (m))\|$
534		fvco3	$⊢ (- : ℂ \times ℂ ⟶ ℂ \land f (m) \in (ℂ \times ℂ)) \to (abs \circ -) (f (m)) = \|- (f (m))\|$
535	137 530 534	sylancr	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to (abs \circ -) (f (m)) = \|- (f (m))\|$
536	505 535	eqtrd	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to ((abs \circ -) \circ f) (m) = \|- (f (m))\|$
537	533 536	breqtrrd	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land m \in ℕ) \to 0 \leq ((abs \circ -) \circ f) (m)$
538	537	ad5ant15	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in ℕ) \to 0 \leq ((abs \circ -) \circ f) (m)$
539	529 538	syldan	$⊢ ((((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \land m \in (t + 1 \dots n)) \to 0 \leq ((abs \circ -) \circ f) (m)$
540	471 512 513 539	sermono	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \to seq 1 (+ ((abs \circ -) \circ f)) (t) \leq seq 1 (+ ((abs \circ -) \circ f)) (n)$
541	508 540	eqbrtrd	$⊢ (((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \land t \leq n) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) \leq seq 1 (+ ((abs \circ -) \circ f)) (n)$
542	402	ad2antlr	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \to n \in ℝ$
543	478	adantl	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \to t \in ℝ$
544	468 541 542 543	ltlecasei	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land t \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) \leq seq 1 (+ ((abs \circ -) \circ f)) (n)$
545	544	ralrimiva	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to \forall t \in ℕ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) \leq seq 1 (+ ((abs \circ -) \circ f)) (n)$
546		breq1	$⊢ m = seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) \to (m \leq seq 1 (+ ((abs \circ -) \circ f)) (n) \leftrightarrow seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) \leq seq 1 (+ ((abs \circ -) \circ f)) (n))$
547	546	ralrn	$⊢ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) Fn ℕ \to (\forall m \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) m \leq seq 1 (+ ((abs \circ -) \circ f)) (n) \leftrightarrow \forall t \in ℕ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) \leq seq 1 (+ ((abs \circ -) \circ f)) (n))$
548	355 547	syl	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to (\forall m \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) m \leq seq 1 (+ ((abs \circ -) \circ f)) (n) \leftrightarrow \forall t \in ℕ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) \leq seq 1 (+ ((abs \circ -) \circ f)) (n))$
549	548	adantr	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to (\forall m \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) m \leq seq 1 (+ ((abs \circ -) \circ f)) (n) \leftrightarrow \forall t \in ℕ seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) (t) \leq seq 1 (+ ((abs \circ -) \circ f)) (n))$
550	545 549	mpbird	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to \forall m \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) m \leq seq 1 (+ ((abs \circ -) \circ f)) (n)$
551	550	r19.21bi	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land m \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))))) \to m \leq seq 1 (+ ((abs \circ -) \circ f)) (n)$
552	361 362 551	lensymd	$⊢ ((f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \land m \in ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩))))) \to \neg seq 1 (+ ((abs \circ -) \circ f)) (n) < m$
553	311 322 358 552	supmax	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) ℝ^{*} <) = seq 1 (+ ((abs \circ -) \circ f)) (n)$
554	52 553	sylan	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to sup (ran seq 1 (+ ((abs \circ -) \circ (z \in ℕ ⟼ if (z \in (1 \dots n), f (z), ⟨0, 0⟩)))) ℝ^{*} <) = seq 1 (+ ((abs \circ -) \circ f)) (n)$
555	255 309 554	3eqtr3rd	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ f)) (n) = {vol}^{*} (⋃_{z = 1}^{n} [.] (f (z)) \cup ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩))$
556		elfznn	$⊢ z \in (1 \dots n) \to z \in ℕ$
557	164 65	sseldi	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to f (z) \in ℝ^{2}$
558		1st2nd2	$⊢ f (z) \in ℝ^{2} \to f (z) = ⟨1^{st} (f (z)), 2^{nd} (f (z))⟩$
559	558	fveq2d	$⊢ f (z) \in ℝ^{2} \to [.] (f (z)) = [.] (⟨1^{st} (f (z)), 2^{nd} (f (z))⟩)$
560		df-ov	$⊢ [1^{st} (f (z)), 2^{nd} (f (z))] = [.] (⟨1^{st} (f (z)), 2^{nd} (f (z))⟩)$
561	559 560	eqtr4di	$⊢ f (z) \in ℝ^{2} \to [.] (f (z)) = [1^{st} (f (z)), 2^{nd} (f (z))]$
562		xp1st	$⊢ f (z) \in ℝ^{2} \to 1^{st} (f (z)) \in ℝ$
563		xp2nd	$⊢ f (z) \in ℝ^{2} \to 2^{nd} (f (z)) \in ℝ$
564		iccssre	$⊢ (1^{st} (f (z)) \in ℝ \land 2^{nd} (f (z)) \in ℝ) \to [1^{st} (f (z)), 2^{nd} (f (z))] \subseteq ℝ$
565	562 563 564	syl2anc	$⊢ f (z) \in ℝ^{2} \to [1^{st} (f (z)), 2^{nd} (f (z))] \subseteq ℝ$
566	561 565	eqsstrd	$⊢ f (z) \in ℝ^{2} \to [.] (f (z)) \subseteq ℝ$
567	557 566	syl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to [.] (f (z)) \subseteq ℝ$
568	52 556 567	syl2an	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in (1 \dots n)) \to [.] (f (z)) \subseteq ℝ$
569	568	ralrimiva	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to \forall z \in (1 \dots n) [.] (f (z)) \subseteq ℝ$
570		iunss	$⊢ ⋃_{z = 1}^{n} [.] (f (z)) \subseteq ℝ \leftrightarrow \forall z \in (1 \dots n) [.] (f (z)) \subseteq ℝ$
571	569 570	sylibr	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ⋃_{z = 1}^{n} [.] (f (z)) \subseteq ℝ$
572	571	adantr	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to ⋃_{z = 1}^{n} [.] (f (z)) \subseteq ℝ$
573		uzid	$⊢ n + 1 \in ℤ \to n + 1 \in ℤ_{\geq (n + 1)}$
574		ne0i	$⊢ n + 1 \in ℤ_{\geq (n + 1)} \to ℤ_{\geq (n + 1)} \neq \emptyset$
575		iunconst	$⊢ ℤ_{\geq (n + 1)} \neq \emptyset \to ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩) = [.] (⟨0, 0⟩)$
576	373 573 574 575	4syl	$⊢ n \in ℕ \to ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩) = [.] (⟨0, 0⟩)$
577		iccid	$⊢ 0 \in ℝ^{*} \to [0, 0] = \{0\}$
578	259 577	ax-mp	$⊢ [0, 0] = \{0\}$
579		df-ov	$⊢ [0, 0] = [.] (⟨0, 0⟩)$
580	578 579	eqtr3i	$⊢ \{0\} = [.] (⟨0, 0⟩)$
581	576 580	eqtr4di	$⊢ n \in ℕ \to ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩) = \{0\}$
582		snssi	$⊢ 0 \in ℝ \to \{0\} \subseteq ℝ$
583	199 582	ax-mp	$⊢ \{0\} \subseteq ℝ$
584	581 583	eqsstrdi	$⊢ n \in ℕ \to ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩) \subseteq ℝ$
585	584	adantl	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩) \subseteq ℝ$
586	581	fveq2d	$⊢ n \in ℕ \to {vol}^{} (⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩)) = {vol}^{} (\{0\})$
587	586	adantl	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to {vol}^{} (⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩)) = {vol}^{} (\{0\})$
588		ovolsn	$⊢ 0 \in ℝ \to {vol}^{*} (\{0\}) = 0$
589	199 588	ax-mp	$⊢ {vol}^{*} (\{0\}) = 0$
590	587 589	eqtrdi	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to {vol}^{*} (⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩)) = 0$
591		ovolunnul	$⊢ (⋃_{z = 1}^{n} [.] (f (z)) \subseteq ℝ \land ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩) \subseteq ℝ \land {vol}^{} (⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩)) = 0) \to {vol}^{} (⋃_{z = 1}^{n} [.] (f (z)) \cup ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩)) = {vol}^{*} (⋃_{z = 1}^{n} [.] (f (z)))$
592	572 585 590 591	syl3anc	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to {vol}^{} (⋃_{z = 1}^{n} [.] (f (z)) \cup ⋃_{z \in ℤ_{\geq (n + 1)}} [.] (⟨0, 0⟩)) = {vol}^{} (⋃_{z = 1}^{n} [.] (f (z)))$
593	555 592	eqtrd	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to seq 1 (+ ((abs \circ -) \circ f)) (n) = {vol}^{*} (⋃_{z = 1}^{n} [.] (f (z)))$
594	593	breq2d	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to (M < seq 1 (+ ((abs \circ -) \circ f)) (n) \leftrightarrow M < {vol}^{*} (⋃_{z = 1}^{n} [.] (f (z))))$
595	594	biimpd	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land n \in ℕ) \to (M < seq 1 (+ ((abs \circ -) \circ f)) (n) \to M < {vol}^{*} (⋃_{z = 1}^{n} [.] (f (z))))$
596	595	reximdva	$⊢ f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to (\exists n \in ℕ M < seq 1 (+ ((abs \circ -) \circ f)) (n) \to \exists n \in ℕ M < {vol}^{*} (⋃_{z = 1}^{n} [.] (f (z))))$
597	596	adantl	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to (\exists n \in ℕ M < seq 1 (+ ((abs \circ -) \circ f)) (n) \to \exists n \in ℕ M < {vol}^{} (⋃_{z = 1}^{n} [.] (f (z))))$
598	194 597	mpd	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to \exists n \in ℕ M < {vol}^{} (⋃_{z = 1}^{n} [.] (f (z)))$
599		fzfi	$⊢ (1 \dots n) \in Fin$
600		icccld	$⊢ (1^{st} (f (z)) \in ℝ \land 2^{nd} (f (z)) \in ℝ) \to [1^{st} (f (z)), 2^{nd} (f (z))] \in Clsd (topGen (ran (.)))$
601	562 563 600	syl2anc	$⊢ f (z) \in ℝ^{2} \to [1^{st} (f (z)), 2^{nd} (f (z))] \in Clsd (topGen (ran (.)))$
602	561 601	eqeltrd	$⊢ f (z) \in ℝ^{2} \to [.] (f (z)) \in Clsd (topGen (ran (.)))$
603	557 602	syl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to [.] (f (z)) \in Clsd (topGen (ran (.)))$
604	556 603	sylan2	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in (1 \dots n)) \to [.] (f (z)) \in Clsd (topGen (ran (.)))$
605	604	ralrimiva	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to \forall z \in (1 \dots n) [.] (f (z)) \in Clsd (topGen (ran (.)))$
606		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
607	606	iuncld	$⊢ (topGen (ran (.)) \in Top \land (1 \dots n) \in Fin \land \forall z \in (1 \dots n) [.] (f (z)) \in Clsd (topGen (ran (.)))) \to ⋃_{z = 1}^{n} [.] (f (z)) \in Clsd (topGen (ran (.)))$
608	1 599 605 607	mp3an12i	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ⋃_{z = 1}^{n} [.] (f (z)) \in Clsd (topGen (ran (.)))$
609	608	adantr	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (n \in ℕ \land M < {vol}^{*} (⋃_{z = 1}^{n} [.] (f (z))))) \to ⋃_{z = 1}^{n} [.] (f (z)) \in Clsd (topGen (ran (.)))$
610		fveq2	$⊢ b = f (z) \to [.] (b) = [.] (f (z))$
611	610	sseq1d	$⊢ b = f (z) \to ([.] (b) \subseteq A \leftrightarrow [.] (f (z)) \subseteq A)$
612	611	elrab	$⊢ f (z) \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \leftrightarrow (f (z) \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \land [.] (f (z)) \subseteq A)$
613	612	simprbi	$⊢ f (z) \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \to [.] (f (z)) \subseteq A$
614	65 73 613	3syl	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in ℕ) \to [.] (f (z)) \subseteq A$
615	556 614	sylan2	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land z \in (1 \dots n)) \to [.] (f (z)) \subseteq A$
616	615	ralrimiva	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to \forall z \in (1 \dots n) [.] (f (z)) \subseteq A$
617		iunss	$⊢ ⋃_{z = 1}^{n} [.] (f (z)) \subseteq A \leftrightarrow \forall z \in (1 \dots n) [.] (f (z)) \subseteq A$
618	616 617	sylibr	$⊢ f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \to ⋃_{z = 1}^{n} [.] (f (z)) \subseteq A$
619	618	adantr	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (n \in ℕ \land M < {vol}^{*} (⋃_{z = 1}^{n} [.] (f (z))))) \to ⋃_{z = 1}^{n} [.] (f (z)) \subseteq A$
620		simprr	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (n \in ℕ \land M < {vol}^{} (⋃_{z = 1}^{n} [.] (f (z))))) \to M < {vol}^{} (⋃_{z = 1}^{n} [.] (f (z)))$
621		sseq1	$⊢ s = ⋃_{z = 1}^{n} [.] (f (z)) \to (s \subseteq A \leftrightarrow ⋃_{z = 1}^{n} [.] (f (z)) \subseteq A)$
622		fveq2	$⊢ s = ⋃_{z = 1}^{n} [.] (f (z)) \to {vol}^{} (s) = {vol}^{} (⋃_{z = 1}^{n} [.] (f (z)))$
623	622	breq2d	$⊢ s = ⋃_{z = 1}^{n} [.] (f (z)) \to (M < {vol}^{} (s) \leftrightarrow M < {vol}^{} (⋃_{z = 1}^{n} [.] (f (z))))$
624	621 623	anbi12d	$⊢ s = ⋃_{z = 1}^{n} [.] (f (z)) \to ((s \subseteq A \land M < {vol}^{} (s)) \leftrightarrow (⋃_{z = 1}^{n} [.] (f (z)) \subseteq A \land M < {vol}^{} (⋃_{z = 1}^{n} [.] (f (z)))))$
625	624	rspcev	$⊢ (⋃_{z = 1}^{n} [.] (f (z)) \in Clsd (topGen (ran (.))) \land (⋃_{z = 1}^{n} [.] (f (z)) \subseteq A \land M < {vol}^{} (⋃_{z = 1}^{n} [.] (f (z))))) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{} (s))$
626	609 619 620 625	syl12anc	$⊢ (f : ℕ ⟶ \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (n \in ℕ \land M < {vol}^{} (⋃_{z = 1}^{n} [.] (f (z))))) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{} (s))$
627	52 626	sylan	$⊢ (f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\} \land (n \in ℕ \land M < {vol}^{} (⋃_{z = 1}^{n} [.] (f (z))))) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{} (s))$
628	627	adantll	$⊢ (((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \land (n \in ℕ \land M < {vol}^{} (⋃_{z = 1}^{n} [.] (f (z))))) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{*} (s))$
629	598 628	rexlimddv	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{} (s))$
630	629	adantlr	$⊢ (((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land A \neq \emptyset) \land f : ℕ \underset{1-1 onto}{⟶} \{a \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} \| \forall c \in \{b \in ran (x \in ℤ, y \in ℕ_{0} ⟼ ⟨\frac{x}{2^{y}}, \frac{x + 1}{2^{y}}⟩) \| [.] (b) \subseteq A\} ([.] (a) \subseteq [.] (c) \to a = c)\}) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{} (s))$
631	17 630	exlimddv	$⊢ ((A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \land A \neq \emptyset) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{} (s))$
632	15 631	pm2.61dane	$⊢ (A \in topGen (ran (.)) \land M \in ℝ \land M < {vol}^{} (A)) \to \exists s \in Clsd (topGen (ran (.))) (s \subseteq A \land M < {vol}^{} (s))$

Metamath Proof Explorer

Theorem mblfinlem2

Proof