poimirlem29

Description: Lemma for poimir connecting cubes of the tessellation to neighborhoods. (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	$⊢ φ \to N \in ℕ$
	poimir.i	$⊢ I = {[0, 1]}^{(1 \dots N)}$
	poimir.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
	poimir.1	$⊢ φ \to F \in ((R ↾_{𝑡} I) Cn R)$
	poimirlem30.x	$⊢ X = F ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (n)$
	poimirlem30.2	$⊢ φ \to G : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
	poimirlem30.3	$⊢ (φ \land k \in ℕ) \to ran 1^{st} (G (k)) \subseteq (0 ..^k)$
	poimirlem30.4	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N) \land r \in \{\leq \leq^{-1}\})) \to \exists j \in (0 \dots N) 0 r X$
Assertion	poimirlem29	$⊢ φ \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (C \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$

Proof

Step	Hyp	Ref	Expression
1		poimir.0	$⊢ φ \to N \in ℕ$
2		poimir.i	$⊢ I = {[0, 1]}^{(1 \dots N)}$
3		poimir.r	$⊢ R = \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\})$
4		poimir.1	$⊢ φ \to F \in ((R ↾_{𝑡} I) Cn R)$
5		poimirlem30.x	$⊢ X = F ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (n)$
6		poimirlem30.2	$⊢ φ \to G : ℕ ⟶ ({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
7		poimirlem30.3	$⊢ (φ \land k \in ℕ) \to ran 1^{st} (G (k)) \subseteq (0 ..^k)$
8		poimirlem30.4	$⊢ (φ \land (k \in ℕ \land n \in (1 \dots N) \land r \in \{\leq \leq^{-1}\})) \to \exists j \in (0 \dots N) 0 r X$
9		fzfi	$⊢ (1 \dots N) \in Fin$
10		retop	$⊢ topGen (ran (.)) \in Top$
11	10	fconst6	$⊢ ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top$
12		pttop	$⊢ ((1 \dots N) \in Fin \land ((1 \dots N) \times \{topGen (ran (.))\}) : (1 \dots N) ⟶ Top) \to \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) \in Top$
13	9 11 12	mp2an	$⊢ \prod_{𝑡} ((1 \dots N) \times \{topGen (ran (.))\}) \in Top$
14	3 13	eqeltri	$⊢ R \in Top$
15		ovex	$⊢ {[0, 1]}^{(1 \dots N)} \in V$
16	2 15	eqeltri	$⊢ I \in V$
17		elrest	$⊢ (R \in Top \land I \in V) \to (v \in (R ↾_{𝑡} I) \leftrightarrow \exists z \in R v = z \cap I)$
18	14 16 17	mp2an	$⊢ v \in (R ↾_{𝑡} I) \leftrightarrow \exists z \in R v = z \cap I$
19		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
20	3 19	ptrecube	$⊢ (z \in R \land C \in z) \to \exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \subseteq z$
21	20	ex	$⊢ z \in R \to (C \in z \to \exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \subseteq z)$
22		inss1	$⊢ z \cap I \subseteq z$
23		sseq1	$⊢ v = z \cap I \to (v \subseteq z \leftrightarrow z \cap I \subseteq z)$
24	22 23	mpbiri	$⊢ v = z \cap I \to v \subseteq z$
25	24	sseld	$⊢ v = z \cap I \to (C \in v \to C \in z)$
26		ssrin	$⊢ ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \subseteq z \to ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq z \cap I$
27		sseq2	$⊢ v = z \cap I \to (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v \leftrightarrow ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq z \cap I)$
28	26 27	imbitrrid	$⊢ v = z \cap I \to (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \subseteq z \to ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v)$
29	28	reximdv	$⊢ v = z \cap I \to (\exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \subseteq z \to \exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v)$
30	25 29	imim12d	$⊢ v = z \cap I \to ((C \in z \to \exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \subseteq z) \to (C \in v \to \exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v))$
31	21 30	syl5com	$⊢ z \in R \to (v = z \cap I \to (C \in v \to \exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v))$
32	31	rexlimiv	$⊢ \exists z \in R v = z \cap I \to (C \in v \to \exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v)$
33	18 32	sylbi	$⊢ v \in (R ↾_{𝑡} I) \to (C \in v \to \exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v)$
34	33	imp	$⊢ (v \in (R ↾_{𝑡} I) \land C \in v) \to \exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v$
35	34	adantl	$⊢ (φ \land (v \in (R ↾_{𝑡} I) \land C \in v)) \to \exists c \in ℝ^{+} ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v$
36		resttop	$⊢ (R \in Top \land I \in V) \to R ↾_{𝑡} I \in Top$
37	14 16 36	mp2an	$⊢ R ↾_{𝑡} I \in Top$
38		reex	$⊢ ℝ \in V$
39		unitssre	$⊢ [0, 1] \subseteq ℝ$
40		mapss	$⊢ (ℝ \in V \land [0, 1] \subseteq ℝ) \to {[0, 1]}^{(1 \dots N)} \subseteq ℝ^{(1 \dots N)}$
41	38 39 40	mp2an	$⊢ {[0, 1]}^{(1 \dots N)} \subseteq ℝ^{(1 \dots N)}$
42	2 41	eqsstri	$⊢ I \subseteq ℝ^{(1 \dots N)}$
43		ovex	$⊢ (1 \dots N) \in V$
44		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
45	3 44	ptuniconst	$⊢ ((1 \dots N) \in V \land topGen (ran (.)) \in Top) \to ℝ^{(1 \dots N)} = ⋃ R$
46	43 10 45	mp2an	$⊢ ℝ^{(1 \dots N)} = ⋃ R$
47	46	restuni	$⊢ (R \in Top \land I \subseteq ℝ^{(1 \dots N)}) \to I = ⋃ (R ↾_{𝑡} I)$
48	14 42 47	mp2an	$⊢ I = ⋃ (R ↾_{𝑡} I)$
49	48	eltopss	$⊢ (R ↾_{𝑡} I \in Top \land v \in (R ↾_{𝑡} I)) \to v \subseteq I$
50	37 49	mpan	$⊢ v \in (R ↾_{𝑡} I) \to v \subseteq I$
51	50	sselda	$⊢ (v \in (R ↾_{𝑡} I) \land C \in v) \to C \in I$
52		2rp	$⊢ 2 \in ℝ^{+}$
53		rpdivcl	$⊢ (2 \in ℝ^{+} \land c \in ℝ^{+}) \to \frac{2}{c} \in ℝ^{+}$
54	52 53	mpan	$⊢ c \in ℝ^{+} \to \frac{2}{c} \in ℝ^{+}$
55	54	rpred	$⊢ c \in ℝ^{+} \to \frac{2}{c} \in ℝ$
56		ceicl	$⊢ \frac{2}{c} \in ℝ \to - ⌊- \frac{2}{c}⌋ \in ℤ$
57	55 56	syl	$⊢ c \in ℝ^{+} \to - ⌊- \frac{2}{c}⌋ \in ℤ$
58		0red	$⊢ c \in ℝ^{+} \to 0 \in ℝ$
59	57	zred	$⊢ c \in ℝ^{+} \to - ⌊- \frac{2}{c}⌋ \in ℝ$
60	54	rpgt0d	$⊢ c \in ℝ^{+} \to 0 < \frac{2}{c}$
61		ceige	$⊢ \frac{2}{c} \in ℝ \to \frac{2}{c} \leq - ⌊- \frac{2}{c}⌋$
62	55 61	syl	$⊢ c \in ℝ^{+} \to \frac{2}{c} \leq - ⌊- \frac{2}{c}⌋$
63	58 55 59 60 62	ltletrd	$⊢ c \in ℝ^{+} \to 0 < - ⌊- \frac{2}{c}⌋$
64		elnnz	$⊢ - ⌊- \frac{2}{c}⌋ \in ℕ \leftrightarrow (- ⌊- \frac{2}{c}⌋ \in ℤ \land 0 < - ⌊- \frac{2}{c}⌋)$
65	57 63 64	sylanbrc	$⊢ c \in ℝ^{+} \to - ⌊- \frac{2}{c}⌋ \in ℕ$
66		fveq2	$⊢ i = - ⌊- \frac{2}{c}⌋ \to ℤ_{\geq i} = ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}$
67		oveq2	$⊢ i = - ⌊- \frac{2}{c}⌋ \to \frac{1}{i} = \frac{1}{- ⌊- \frac{2}{c}⌋}$
68	67	oveq2d	$⊢ i = - ⌊- \frac{2}{c}⌋ \to C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i}) = C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})$
69	68	eleq2d	$⊢ i = - ⌊- \frac{2}{c}⌋ \to ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})))$
70	69	ralbidv	$⊢ i = - ⌊- \frac{2}{c}⌋ \to (\forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})))$
71	66 70	rexeqbidv	$⊢ i = - ⌊- \frac{2}{c}⌋ \to (\exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \leftrightarrow \exists k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})))$
72	71	rspcv	$⊢ - ⌊- \frac{2}{c}⌋ \in ℕ \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \exists k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})))$
73	65 72	syl	$⊢ c \in ℝ^{+} \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \exists k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})))$
74	73	adantl	$⊢ ((φ \land C \in I) \land c \in ℝ^{+}) \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \exists k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})))$
75		uznnssnn	$⊢ - ⌊- \frac{2}{c}⌋ \in ℕ \to ℤ_{\geq (- ⌊- \frac{2}{c}⌋)} \subseteq ℕ$
76	65 75	syl	$⊢ c \in ℝ^{+} \to ℤ_{\geq (- ⌊- \frac{2}{c}⌋)} \subseteq ℕ$
77	76	sseld	$⊢ c \in ℝ^{+} \to (k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)} \to k \in ℕ)$
78	77	adantl	$⊢ ((φ \land C \in I) \land c \in ℝ^{+}) \to (k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)} \to k \in ℕ)$
79	78	imdistani	$⊢ (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ)$
80	65	nnrpd	$⊢ c \in ℝ^{+} \to - ⌊- \frac{2}{c}⌋ \in ℝ^{+}$
81	54 80	lerecd	$⊢ c \in ℝ^{+} \to (\frac{2}{c} \leq - ⌊- \frac{2}{c}⌋ \leftrightarrow \frac{1}{- ⌊- \frac{2}{c}⌋} \leq \frac{1}{\frac{2}{c}})$
82	62 81	mpbid	$⊢ c \in ℝ^{+} \to \frac{1}{- ⌊- \frac{2}{c}⌋} \leq \frac{1}{\frac{2}{c}}$
83		rpcn	$⊢ c \in ℝ^{+} \to c \in ℂ$
84		rpne0	$⊢ c \in ℝ^{+} \to c \neq 0$
85		2cn	$⊢ 2 \in ℂ$
86		2ne0	$⊢ 2 \neq 0$
87		recdiv	$⊢ ((2 \in ℂ \land 2 \neq 0) \land (c \in ℂ \land c \neq 0)) \to \frac{1}{\frac{2}{c}} = \frac{c}{2}$
88	85 86 87	mpanl12	$⊢ (c \in ℂ \land c \neq 0) \to \frac{1}{\frac{2}{c}} = \frac{c}{2}$
89	83 84 88	syl2anc	$⊢ c \in ℝ^{+} \to \frac{1}{\frac{2}{c}} = \frac{c}{2}$
90	82 89	breqtrd	$⊢ c \in ℝ^{+} \to \frac{1}{- ⌊- \frac{2}{c}⌋} \leq \frac{c}{2}$
91	90	ad4antlr	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1}{- ⌊- \frac{2}{c}⌋} \leq \frac{c}{2}$
92		elmapi	$⊢ C \in ({[0, 1]}^{(1 \dots N)}) \to C : (1 \dots N) ⟶ [0, 1]$
93	92 2	eleq2s	$⊢ C \in I \to C : (1 \dots N) ⟶ [0, 1]$
94	93	ad4antlr	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \to C : (1 \dots N) ⟶ [0, 1]$
95	94	ffvelcdmda	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) \in [0, 1]$
96	39 95	sselid	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) \in ℝ$
97		simp-4l	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \to φ$
98		simplr	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \to k \in ℕ$
99	97 98	jca	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \to (φ \land k \in ℕ)$
100	6	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to G (k) \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\})$
101		xp1st	$⊢ G (k) \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 1^{st} (G (k)) \in ({ℕ_{0}}^{(1 \dots N)})$
102		elmapi	$⊢ 1^{st} (G (k)) \in ({ℕ_{0}}^{(1 \dots N)}) \to 1^{st} (G (k)) : (1 \dots N) ⟶ ℕ_{0}$
103	100 101 102	3syl	$⊢ (φ \land k \in ℕ) \to 1^{st} (G (k)) : (1 \dots N) ⟶ ℕ_{0}$
104	103	ffvelcdmda	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots N)) \to 1^{st} (G (k)) (m) \in ℕ_{0}$
105	104	nn0red	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots N)) \to 1^{st} (G (k)) (m) \in ℝ$
106		simplr	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots N)) \to k \in ℕ$
107	105 106	nndivred	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m)}{k} \in ℝ$
108	99 107	sylan	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m)}{k} \in ℝ$
109	96 108	resubcld	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) - (\frac{1^{st} (G (k)) (m)}{k}) \in ℝ$
110	109	recnd	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) - (\frac{1^{st} (G (k)) (m)}{k}) \in ℂ$
111	110	abscld	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| \in ℝ$
112	65	nnrecred	$⊢ c \in ℝ^{+} \to \frac{1}{- ⌊- \frac{2}{c}⌋} \in ℝ$
113	112	ad4antlr	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1}{- ⌊- \frac{2}{c}⌋} \in ℝ$
114		rphalfcl	$⊢ c \in ℝ^{+} \to \frac{c}{2} \in ℝ^{+}$
115	114	rpred	$⊢ c \in ℝ^{+} \to \frac{c}{2} \in ℝ$
116	115	ad4antlr	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{c}{2} \in ℝ$
117		ltletr	$⊢ (\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| \in ℝ \land \frac{1}{- ⌊- \frac{2}{c}⌋} \in ℝ \land \frac{c}{2} \in ℝ) \to ((\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋} \land \frac{1}{- ⌊- \frac{2}{c}⌋} \leq \frac{c}{2}) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{c}{2})$
118	111 113 116 117	syl3anc	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋} \land \frac{1}{- ⌊- \frac{2}{c}⌋} \leq \frac{c}{2}) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{c}{2})$
119	91 118	mpan2d	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋} \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{c}{2})$
120	79 119	sylanl1	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋} \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{c}{2})$
121		simpl	$⊢ (φ \land C \in I) \to φ$
122	76	sselda	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to k \in ℕ$
123	121 122	anim12i	$⊢ ((φ \land C \in I) \land (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)})) \to (φ \land k \in ℕ)$
124	123	anassrs	$⊢ (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to (φ \land k \in ℕ)$
125		1re	$⊢ 1 \in ℝ$
126		snssi	$⊢ 1 \in ℝ \to \{1\} \subseteq ℝ$
127	125 126	ax-mp	$⊢ \{1\} \subseteq ℝ$
128		0re	$⊢ 0 \in ℝ$
129		snssi	$⊢ 0 \in ℝ \to \{0\} \subseteq ℝ$
130	128 129	ax-mp	$⊢ \{0\} \subseteq ℝ$
131	127 130	unssi	$⊢ \{1\} \cup \{0\} \subseteq ℝ$
132		1ex	$⊢ 1 \in V$
133	132	fconst	$⊢ (2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) : 2^{nd} (G (k)) [(1 \dots j)] ⟶ \{1\}$
134		c0ex	$⊢ 0 \in V$
135	134	fconst	$⊢ (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}) : 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{0\}$
136	133 135	pm3.2i	$⊢ ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) : 2^{nd} (G (k)) [(1 \dots j)] ⟶ \{1\} \land (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}) : 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{0\})$
137		xp2nd	$⊢ G (k) \in (({ℕ_{0}}^{(1 \dots N)}) \times \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}) \to 2^{nd} (G (k)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
138	100 137	syl	$⊢ (φ \land k \in ℕ) \to 2^{nd} (G (k)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\}$
139		fvex	$⊢ 2^{nd} (G (k)) \in V$
140		f1oeq1	$⊢ f = 2^{nd} (G (k)) \to (f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N))$
141	139 140	elab	$⊢ 2^{nd} (G (k)) \in \{f \| f : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)\} \leftrightarrow 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
142	138 141	sylib	$⊢ (φ \land k \in ℕ) \to 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
143		dff1o3	$⊢ 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \leftrightarrow (2^{nd} (G (k)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \land Fun {2^{nd} (G (k))}^{-1})$
144	143	simprbi	$⊢ 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to Fun {2^{nd} (G (k))}^{-1}$
145		imain	$⊢ Fun {2^{nd} (G (k))}^{-1} \to 2^{nd} (G (k)) [(1 \dots j) \cap (j + 1 \dots N)] = 2^{nd} (G (k)) [(1 \dots j)] \cap 2^{nd} (G (k)) [(j + 1 \dots N)]$
146	142 144 145	3syl	$⊢ (φ \land k \in ℕ) \to 2^{nd} (G (k)) [(1 \dots j) \cap (j + 1 \dots N)] = 2^{nd} (G (k)) [(1 \dots j)] \cap 2^{nd} (G (k)) [(j + 1 \dots N)]$
147		elfznn0	$⊢ j \in (0 \dots N) \to j \in ℕ_{0}$
148	147	nn0red	$⊢ j \in (0 \dots N) \to j \in ℝ$
149	148	ltp1d	$⊢ j \in (0 \dots N) \to j < j + 1$
150		fzdisj	$⊢ j < j + 1 \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
151	149 150	syl	$⊢ j \in (0 \dots N) \to (1 \dots j) \cap (j + 1 \dots N) = \emptyset$
152	151	imaeq2d	$⊢ j \in (0 \dots N) \to 2^{nd} (G (k)) [(1 \dots j) \cap (j + 1 \dots N)] = 2^{nd} (G (k)) [\emptyset]$
153		ima0	$⊢ 2^{nd} (G (k)) [\emptyset] = \emptyset$
154	152 153	eqtrdi	$⊢ j \in (0 \dots N) \to 2^{nd} (G (k)) [(1 \dots j) \cap (j + 1 \dots N)] = \emptyset$
155	146 154	sylan9req	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to 2^{nd} (G (k)) [(1 \dots j)] \cap 2^{nd} (G (k)) [(j + 1 \dots N)] = \emptyset$
156		fun	$⊢ (((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) : 2^{nd} (G (k)) [(1 \dots j)] ⟶ \{1\} \land (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}) : 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{0\}) \land 2^{nd} (G (k)) [(1 \dots j)] \cap 2^{nd} (G (k)) [(j + 1 \dots N)] = \emptyset) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) : 2^{nd} (G (k)) [(1 \dots j)] \cup 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\}$
157	136 155 156	sylancr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) : 2^{nd} (G (k)) [(1 \dots j)] \cup 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\}$
158		imaundi	$⊢ 2^{nd} (G (k)) [(1 \dots j) \cup (j + 1 \dots N)] = 2^{nd} (G (k)) [(1 \dots j)] \cup 2^{nd} (G (k)) [(j + 1 \dots N)]$
159		nn0p1nn	$⊢ j \in ℕ_{0} \to j + 1 \in ℕ$
160	147 159	syl	$⊢ j \in (0 \dots N) \to j + 1 \in ℕ$
161		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
162	160 161	eleqtrdi	$⊢ j \in (0 \dots N) \to j + 1 \in ℤ_{\geq 1}$
163		elfzuz3	$⊢ j \in (0 \dots N) \to N \in ℤ_{\geq j}$
164		fzsplit2	$⊢ (j + 1 \in ℤ_{\geq 1} \land N \in ℤ_{\geq j}) \to (1 \dots N) = (1 \dots j) \cup (j + 1 \dots N)$
165	162 163 164	syl2anc	$⊢ j \in (0 \dots N) \to (1 \dots N) = (1 \dots j) \cup (j + 1 \dots N)$
166	165	imaeq2d	$⊢ j \in (0 \dots N) \to 2^{nd} (G (k)) [(1 \dots N)] = 2^{nd} (G (k)) [(1 \dots j) \cup (j + 1 \dots N)]$
167		f1ofo	$⊢ 2^{nd} (G (k)) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N) \to 2^{nd} (G (k)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N)$
168		foima	$⊢ 2^{nd} (G (k)) : (1 \dots N) \underset{onto}{⟶} (1 \dots N) \to 2^{nd} (G (k)) [(1 \dots N)] = (1 \dots N)$
169	142 167 168	3syl	$⊢ (φ \land k \in ℕ) \to 2^{nd} (G (k)) [(1 \dots N)] = (1 \dots N)$
170	166 169	sylan9req	$⊢ (j \in (0 \dots N) \land (φ \land k \in ℕ)) \to 2^{nd} (G (k)) [(1 \dots j) \cup (j + 1 \dots N)] = (1 \dots N)$
171	170	ancoms	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to 2^{nd} (G (k)) [(1 \dots j) \cup (j + 1 \dots N)] = (1 \dots N)$
172	158 171	eqtr3id	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to 2^{nd} (G (k)) [(1 \dots j)] \cup 2^{nd} (G (k)) [(j + 1 \dots N)] = (1 \dots N)$
173	172	feq2d	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to (((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) : 2^{nd} (G (k)) [(1 \dots j)] \cup 2^{nd} (G (k)) [(j + 1 \dots N)] ⟶ \{1\} \cup \{0\} \leftrightarrow ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\})$
174	157 173	mpbid	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) : (1 \dots N) ⟶ \{1\} \cup \{0\}$
175	174	ffvelcdmda	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in (\{1\} \cup \{0\})$
176	131 175	sselid	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in ℝ$
177		simpllr	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to k \in ℕ$
178	176 177	nndivred	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ$
179	178	recnd	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℂ$
180	179	absnegd	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| = \|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\|$
181	124 180	sylanl1	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| = \|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\|$
182	124 175	sylanl1	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in (\{1\} \cup \{0\})$
183		elun	$⊢ ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in (\{1\} \cup \{0\}) \leftrightarrow (((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{1\} \lor ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{0\})$
184	182 183	sylib	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{1\} \lor ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{0\})$
185		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
186		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
187	186	rpreccld	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ^{+}$
188	187	rpge0d	$⊢ k \in ℕ \to 0 \leq \frac{1}{k}$
189	185 188	absidd	$⊢ k \in ℕ \to \|\frac{1}{k}\| = \frac{1}{k}$
190	122 189	syl	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to \|\frac{1}{k}\| = \frac{1}{k}$
191	122	nnrecred	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to \frac{1}{k} \in ℝ$
192	112	adantr	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to \frac{1}{- ⌊- \frac{2}{c}⌋} \in ℝ$
193	115	adantr	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to \frac{c}{2} \in ℝ$
194		eluzle	$⊢ k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)} \to - ⌊- \frac{2}{c}⌋ \leq k$
195	194	adantl	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to - ⌊- \frac{2}{c}⌋ \leq k$
196	65	adantr	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to - ⌊- \frac{2}{c}⌋ \in ℕ$
197	196	nnrpd	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to - ⌊- \frac{2}{c}⌋ \in ℝ^{+}$
198	122	nnrpd	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to k \in ℝ^{+}$
199	197 198	lerecd	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to (- ⌊- \frac{2}{c}⌋ \leq k \leftrightarrow \frac{1}{k} \leq \frac{1}{- ⌊- \frac{2}{c}⌋})$
200	195 199	mpbid	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to \frac{1}{k} \leq \frac{1}{- ⌊- \frac{2}{c}⌋}$
201	90	adantr	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to \frac{1}{- ⌊- \frac{2}{c}⌋} \leq \frac{c}{2}$
202	191 192 193 200 201	letrd	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to \frac{1}{k} \leq \frac{c}{2}$
203	190 202	eqbrtrd	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to \|\frac{1}{k}\| \leq \frac{c}{2}$
204		elsni	$⊢ ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{1\} \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) = 1$
205	204	fvoveq1d	$⊢ ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{1\} \to \|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| = \|\frac{1}{k}\|$
206	205	breq1d	$⊢ ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{1\} \to (\|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2} \leftrightarrow \|\frac{1}{k}\| \leq \frac{c}{2})$
207	203 206	syl5ibrcom	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to (((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{1\} \to \|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2})$
208	114	rpge0d	$⊢ c \in ℝ^{+} \to 0 \leq \frac{c}{2}$
209		nncn	$⊢ k \in ℕ \to k \in ℂ$
210		nnne0	$⊢ k \in ℕ \to k \neq 0$
211	209 210	div0d	$⊢ k \in ℕ \to \frac{0}{k} = 0$
212	211	abs00bd	$⊢ k \in ℕ \to \|\frac{0}{k}\| = 0$
213	212	breq1d	$⊢ k \in ℕ \to (\|\frac{0}{k}\| \leq \frac{c}{2} \leftrightarrow 0 \leq \frac{c}{2})$
214	213	biimparc	$⊢ (0 \leq \frac{c}{2} \land k \in ℕ) \to \|\frac{0}{k}\| \leq \frac{c}{2}$
215	208 214	sylan	$⊢ (c \in ℝ^{+} \land k \in ℕ) \to \|\frac{0}{k}\| \leq \frac{c}{2}$
216	122 215	syldan	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to \|\frac{0}{k}\| \leq \frac{c}{2}$
217		elsni	$⊢ ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{0\} \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) = 0$
218	217	fvoveq1d	$⊢ ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{0\} \to \|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| = \|\frac{0}{k}\|$
219	218	breq1d	$⊢ ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{0\} \to (\|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2} \leftrightarrow \|\frac{0}{k}\| \leq \frac{c}{2})$
220	216 219	syl5ibrcom	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to (((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{0\} \to \|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2})$
221	207 220	jaod	$⊢ (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to ((((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{1\} \lor ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{0\}) \to \|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2})$
222	221	adantll	$⊢ (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to ((((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{1\} \lor ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{0\}) \to \|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2})$
223	222	ad2antrr	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{1\} \lor ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in \{0\}) \to \|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2})$
224	184 223	mpd	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2}$
225	181 224	eqbrtrd	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2}$
226	79 111	sylanl1	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| \in ℝ$
227		simpll	$⊢ ((φ \land C \in I) \land c \in ℝ^{+}) \to φ$
228	227	anim1i	$⊢ (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \to (φ \land k \in ℕ)$
229	178	renegcld	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to - \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ$
230	228 229	sylanl1	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to - \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ$
231	230	recnd	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to - \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℂ$
232	231	abscld	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \in ℝ$
233	79 232	sylanl1	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \in ℝ$
234	115 115	jca	$⊢ c \in ℝ^{+} \to (\frac{c}{2} \in ℝ \land \frac{c}{2} \in ℝ)$
235	234	ad4antlr	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (\frac{c}{2} \in ℝ \land \frac{c}{2} \in ℝ)$
236		ltleadd	$⊢ ((\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| \in ℝ \land \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \in ℝ) \land (\frac{c}{2} \in ℝ \land \frac{c}{2} \in ℝ)) \to ((\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{c}{2} \land \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2}) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| < (\frac{c}{2}) + (\frac{c}{2}))$
237	226 233 235 236	syl21anc	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{c}{2} \land \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \leq \frac{c}{2}) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| < (\frac{c}{2}) + (\frac{c}{2}))$
238	225 237	mpan2d	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{c}{2} \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| < (\frac{c}{2}) + (\frac{c}{2}))$
239	110 231	abstrid	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| \leq \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\|$
240	109 230	readdcld	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}) \in ℝ$
241	240	recnd	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}) \in ℂ$
242	241	abscld	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| \in ℝ$
243	111 232	readdcld	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \in ℝ$
244	115 115	readdcld	$⊢ c \in ℝ^{+} \to (\frac{c}{2}) + (\frac{c}{2}) \in ℝ$
245	244	ad4antlr	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (\frac{c}{2}) + (\frac{c}{2}) \in ℝ$
246		lelttr	$⊢ (\|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| \in ℝ \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \in ℝ \land (\frac{c}{2}) + (\frac{c}{2}) \in ℝ) \to ((\|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| \leq \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| < (\frac{c}{2}) + (\frac{c}{2})) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2}))$
247	242 243 245 246	syl3anc	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((\|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| \leq \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| < (\frac{c}{2}) + (\frac{c}{2})) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2}))$
248	239 247	mpand	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| < (\frac{c}{2}) + (\frac{c}{2}) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2}))$
249	79 248	sylanl1	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| + \|- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}\| < (\frac{c}{2}) + (\frac{c}{2}) \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2}))$
250	120 238 249	3syld	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋} \to \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2}))$
251	105	adantlr	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to 1^{st} (G (k)) (m) \in ℝ$
252	251 176	readdcld	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to 1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in ℝ$
253	252 177	nndivred	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ$
254	124 253	sylanl1	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ$
255	250 254	jctild	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (\|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋} \to (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2})))$
256	255	adantld	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋}) \to (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2})))$
257	79	adantr	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \to (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ)$
258	93	ad3antlr	$⊢ (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \to C : (1 \dots N) ⟶ [0, 1]$
259	258	ffvelcdmda	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to C (m) \in [0, 1]$
260	39 259	sselid	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to C (m) \in ℝ$
261	80	rpreccld	$⊢ c \in ℝ^{+} \to \frac{1}{- ⌊- \frac{2}{c}⌋} \in ℝ^{+}$
262	261	rpxrd	$⊢ c \in ℝ^{+} \to \frac{1}{- ⌊- \frac{2}{c}⌋} \in ℝ^{*}$
263	262	ad3antlr	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to \frac{1}{- ⌊- \frac{2}{c}⌋} \in ℝ^{*}$
264	19	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
265		elbl	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land C (m) \in ℝ \land \frac{1}{- ⌊- \frac{2}{c}⌋} \in ℝ^{*}) \to ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \leftrightarrow ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) < \frac{1}{- ⌊- \frac{2}{c}⌋}))$
266	264 265	mp3an1	$⊢ (C (m) \in ℝ \land \frac{1}{- ⌊- \frac{2}{c}⌋} \in ℝ^{*}) \to ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \leftrightarrow ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) < \frac{1}{- ⌊- \frac{2}{c}⌋}))$
267	260 263 266	syl2anc	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \leftrightarrow ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) < \frac{1}{- ⌊- \frac{2}{c}⌋}))$
268		elmapfn	$⊢ 1^{st} (G (k)) \in ({ℕ_{0}}^{(1 \dots N)}) \to 1^{st} (G (k)) Fn (1 \dots N)$
269	100 101 268	3syl	$⊢ (φ \land k \in ℕ) \to 1^{st} (G (k)) Fn (1 \dots N)$
270		vex	$⊢ k \in V$
271		fnconstg	$⊢ k \in V \to ((1 \dots N) \times \{k\}) Fn (1 \dots N)$
272	270 271	mp1i	$⊢ (φ \land k \in ℕ) \to ((1 \dots N) \times \{k\}) Fn (1 \dots N)$
273		fzfid	$⊢ (φ \land k \in ℕ) \to (1 \dots N) \in Fin$
274		inidm	$⊢ (1 \dots N) \cap (1 \dots N) = (1 \dots N)$
275		eqidd	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots N)) \to 1^{st} (G (k)) (m) = 1^{st} (G (k)) (m)$
276	270	fvconst2	$⊢ m \in (1 \dots N) \to ((1 \dots N) \times \{k\}) (m) = k$
277	276	adantl	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots N)) \to ((1 \dots N) \times \{k\}) (m) = k$
278	269 272 273 273 274 275 277	ofval	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots N)) \to (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) = \frac{1^{st} (G (k)) (m)}{k}$
279	278	oveq2d	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots N)) \to C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) = C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1^{st} (G (k)) (m)}{k})$
280	227 279	sylanl1	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) = C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1^{st} (G (k)) (m)}{k})$
281	227 107	sylanl1	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m)}{k} \in ℝ$
282	19	remetdval	$⊢ (C (m) \in ℝ \land \frac{1^{st} (G (k)) (m)}{k} \in ℝ) \to C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1^{st} (G (k)) (m)}{k}) = \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\|$
283	260 281 282	syl2anc	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1^{st} (G (k)) (m)}{k}) = \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\|$
284	280 283	eqtrd	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) = \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\|$
285	284	breq1d	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to (C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) < \frac{1}{- ⌊- \frac{2}{c}⌋} \leftrightarrow \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋})$
286	285	anbi2d	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to (((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) < \frac{1}{- ⌊- \frac{2}{c}⌋}) \leftrightarrow ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋}))$
287	267 286	bitrd	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land m \in (1 \dots N)) \to ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \leftrightarrow ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋}))$
288	257 287	sylan	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \leftrightarrow ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k})\| < \frac{1}{- ⌊- \frac{2}{c}⌋}))$
289		rpxr	$⊢ c \in ℝ^{+} \to c \in ℝ^{*}$
290	289	ad4antlr	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to c \in ℝ^{*}$
291		elbl	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land C (m) \in ℝ \land c \in ℝ^{*}) \to (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \leftrightarrow (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) < c))$
292	264 291	mp3an1	$⊢ (C (m) \in ℝ \land c \in ℝ^{*}) \to (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \leftrightarrow (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) < c))$
293	96 290 292	syl2anc	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \leftrightarrow (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) < c))$
294		elun	$⊢ z \in (\{1\} \cup \{0\}) \leftrightarrow (z \in \{1\} \lor z \in \{0\})$
295		fzofzp1	$⊢ v \in (0 ..^k) \to v + 1 \in (0 \dots k)$
296		elsni	$⊢ z \in \{1\} \to z = 1$
297	296	oveq2d	$⊢ z \in \{1\} \to v + z = v + 1$
298	297	eleq1d	$⊢ z \in \{1\} \to (v + z \in (0 \dots k) \leftrightarrow v + 1 \in (0 \dots k))$
299	295 298	syl5ibrcom	$⊢ v \in (0 ..^k) \to (z \in \{1\} \to v + z \in (0 \dots k))$
300		elfzonn0	$⊢ v \in (0 ..^k) \to v \in ℕ_{0}$
301	300	nn0cnd	$⊢ v \in (0 ..^k) \to v \in ℂ$
302	301	addridd	$⊢ v \in (0 ..^k) \to v + 0 = v$
303		elfzofz	$⊢ v \in (0 ..^k) \to v \in (0 \dots k)$
304	302 303	eqeltrd	$⊢ v \in (0 ..^k) \to v + 0 \in (0 \dots k)$
305		elsni	$⊢ z \in \{0\} \to z = 0$
306	305	oveq2d	$⊢ z \in \{0\} \to v + z = v + 0$
307	306	eleq1d	$⊢ z \in \{0\} \to (v + z \in (0 \dots k) \leftrightarrow v + 0 \in (0 \dots k))$
308	304 307	syl5ibrcom	$⊢ v \in (0 ..^k) \to (z \in \{0\} \to v + z \in (0 \dots k))$
309	299 308	jaod	$⊢ v \in (0 ..^k) \to ((z \in \{1\} \lor z \in \{0\}) \to v + z \in (0 \dots k))$
310	294 309	biimtrid	$⊢ v \in (0 ..^k) \to (z \in (\{1\} \cup \{0\}) \to v + z \in (0 \dots k))$
311	310	imp	$⊢ (v \in (0 ..^k) \land z \in (\{1\} \cup \{0\})) \to v + z \in (0 \dots k)$
312	311	adantl	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land (v \in (0 ..^k) \land z \in (\{1\} \cup \{0\}))) \to v + z \in (0 \dots k)$
313		dffn3	$⊢ 1^{st} (G (k)) Fn (1 \dots N) \leftrightarrow 1^{st} (G (k)) : (1 \dots N) ⟶ ran 1^{st} (G (k))$
314	269 313	sylib	$⊢ (φ \land k \in ℕ) \to 1^{st} (G (k)) : (1 \dots N) ⟶ ran 1^{st} (G (k))$
315	314 7	fssd	$⊢ (φ \land k \in ℕ) \to 1^{st} (G (k)) : (1 \dots N) ⟶ (0 ..^k)$
316	315	adantr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to 1^{st} (G (k)) : (1 \dots N) ⟶ (0 ..^k)$
317		fzfid	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to (1 \dots N) \in Fin$
318	312 316 174 317 317 274	off	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) : (1 \dots N) ⟶ (0 \dots k)$
319	318	ffnd	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) Fn (1 \dots N)$
320	270 271	mp1i	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((1 \dots N) \times \{k\}) Fn (1 \dots N)$
321	269	adantr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to 1^{st} (G (k)) Fn (1 \dots N)$
322	174	ffnd	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) Fn (1 \dots N)$
323		eqidd	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to 1^{st} (G (k)) (m) = 1^{st} (G (k)) (m)$
324		eqidd	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) = ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)$
325	321 322 317 317 274 323 324	ofval	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) (m) = 1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)$
326	276	adantl	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((1 \dots N) \times \{k\}) (m) = k$
327	319 320 317 317 274 325 326	ofval	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) = \frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}$
328	327	eleq1d	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \leftrightarrow \frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ)$
329	228 328	sylanl1	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \leftrightarrow \frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ)$
330	327	adantl3r	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) = \frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}$
331	330	oveq2d	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) = C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})$
332	93	ad3antlr	$⊢ (((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \to C : (1 \dots N) ⟶ [0, 1]$
333	332	ffvelcdmda	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) \in [0, 1]$
334	39 333	sselid	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) \in ℝ$
335	253	adantl3r	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ$
336	19	remetdval	$⊢ (C (m) \in ℝ \land \frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ) \to C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}) = \|C (m) - (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\|$
337	334 335 336	syl2anc	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}) = \|C (m) - (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\|$
338	251	recnd	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to 1^{st} (G (k)) (m) \in ℂ$
339	176	recnd	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m) \in ℂ$
340	209	ad3antlr	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to k \in ℂ$
341	210	ad3antlr	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to k \neq 0$
342	338 339 340 341	divdird	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} = (\frac{1^{st} (G (k)) (m)}{k}) + (\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})$
343	107	recnd	$⊢ ((φ \land k \in ℕ) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m)}{k} \in ℂ$
344	343	adantlr	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m)}{k} \in ℂ$
345	344 179	subnegd	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (\frac{1^{st} (G (k)) (m)}{k}) - (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}) = (\frac{1^{st} (G (k)) (m)}{k}) + (\frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})$
346	342 345	eqtr4d	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} = (\frac{1^{st} (G (k)) (m)}{k}) - (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})$
347	346	oveq2d	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) - (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}) = C (m) - ((\frac{1^{st} (G (k)) (m)}{k}) - (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}))$
348	347	adantl3r	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) - (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}) = C (m) - ((\frac{1^{st} (G (k)) (m)}{k}) - (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}))$
349	334	recnd	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) \in ℂ$
350	107	adantllr	$⊢ (((φ \land C \in I) \land k \in ℕ) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m)}{k} \in ℝ$
351	350	adantlr	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m)}{k} \in ℝ$
352	351	recnd	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{1^{st} (G (k)) (m)}{k} \in ℂ$
353	179	adantl3r	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℂ$
354	353	negcld	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to - \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℂ$
355	349 352 354	subsubd	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) - ((\frac{1^{st} (G (k)) (m)}{k}) - (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})) = C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})$
356	348 355	eqtrd	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) - (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k}) = C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})$
357	356	fveq2d	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to \|C (m) - (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| = \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\|$
358	331 337 357	3eqtrd	$⊢ ((((φ \land C \in I) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) = \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\|$
359	358	adantl3r	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) = \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\|$
360	83	2halvesd	$⊢ c \in ℝ^{+} \to (\frac{c}{2}) + (\frac{c}{2}) = c$
361	360	eqcomd	$⊢ c \in ℝ^{+} \to c = (\frac{c}{2}) + (\frac{c}{2})$
362	361	ad4antlr	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to c = (\frac{c}{2}) + (\frac{c}{2})$
363	359 362	breq12d	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) < c \leftrightarrow \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2}))$
364	329 363	anbi12d	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in ℝ \land C (m) ({(abs \circ -) ↾}_{ℝ^{2}}) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) < c) \leftrightarrow (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2})))$
365	293 364	bitrd	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℕ) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \leftrightarrow (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2})))$
366	79 365	sylanl1	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \leftrightarrow (\frac{1^{st} (G (k)) (m) + ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k} \in ℝ \land \|C (m) - (\frac{1^{st} (G (k)) (m)}{k}) + (- \frac{((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\})) (m)}{k})\| < (\frac{c}{2}) + (\frac{c}{2})))$
367	256 288 366	3imtr4d	$⊢ (((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \land m \in (1 \dots N)) \to ((1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \to ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c))$
368	367	ralimdva	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \to (\forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \to \forall m \in (1 \dots N) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c))$
369		simplr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to k \in ℕ$
370		elfznn0	$⊢ v \in (0 \dots k) \to v \in ℕ_{0}$
371	370	nn0red	$⊢ v \in (0 \dots k) \to v \in ℝ$
372		nndivre	$⊢ (v \in ℝ \land k \in ℕ) \to \frac{v}{k} \in ℝ$
373	371 372	sylan	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to \frac{v}{k} \in ℝ$
374		elfzle1	$⊢ v \in (0 \dots k) \to 0 \leq v$
375	371 374	jca	$⊢ v \in (0 \dots k) \to (v \in ℝ \land 0 \leq v)$
376	186	rpregt0d	$⊢ k \in ℕ \to (k \in ℝ \land 0 < k)$
377		divge0	$⊢ ((v \in ℝ \land 0 \leq v) \land (k \in ℝ \land 0 < k)) \to 0 \leq \frac{v}{k}$
378	375 376 377	syl2an	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to 0 \leq \frac{v}{k}$
379		elfzle2	$⊢ v \in (0 \dots k) \to v \leq k$
380	379	adantr	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to v \leq k$
381	371	adantr	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to v \in ℝ$
382		1red	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to 1 \in ℝ$
383	186	adantl	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to k \in ℝ^{+}$
384	381 382 383	ledivmuld	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to (\frac{v}{k} \leq 1 \leftrightarrow v \leq k \cdot 1)$
385	209	mulridd	$⊢ k \in ℕ \to k \cdot 1 = k$
386	385	breq2d	$⊢ k \in ℕ \to (v \leq k \cdot 1 \leftrightarrow v \leq k)$
387	386	adantl	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to (v \leq k \cdot 1 \leftrightarrow v \leq k)$
388	384 387	bitrd	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to (\frac{v}{k} \leq 1 \leftrightarrow v \leq k)$
389	380 388	mpbird	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to \frac{v}{k} \leq 1$
390		elicc01	$⊢ \frac{v}{k} \in [0, 1] \leftrightarrow (\frac{v}{k} \in ℝ \land 0 \leq \frac{v}{k} \land \frac{v}{k} \leq 1)$
391	373 378 389 390	syl3anbrc	$⊢ (v \in (0 \dots k) \land k \in ℕ) \to \frac{v}{k} \in [0, 1]$
392	391	ancoms	$⊢ (k \in ℕ \land v \in (0 \dots k)) \to \frac{v}{k} \in [0, 1]$
393		elsni	$⊢ z \in \{k\} \to z = k$
394	393	oveq2d	$⊢ z \in \{k\} \to \frac{v}{z} = \frac{v}{k}$
395	394	eleq1d	$⊢ z \in \{k\} \to (\frac{v}{z} \in [0, 1] \leftrightarrow \frac{v}{k} \in [0, 1])$
396	392 395	syl5ibrcom	$⊢ (k \in ℕ \land v \in (0 \dots k)) \to (z \in \{k\} \to \frac{v}{z} \in [0, 1])$
397	396	impr	$⊢ (k \in ℕ \land (v \in (0 \dots k) \land z \in \{k\})) \to \frac{v}{z} \in [0, 1]$
398	369 397	sylan	$⊢ (((φ \land k \in ℕ) \land j \in (0 \dots N)) \land (v \in (0 \dots k) \land z \in \{k\})) \to \frac{v}{z} \in [0, 1]$
399	270	fconst	$⊢ ((1 \dots N) \times \{k\}) : (1 \dots N) ⟶ \{k\}$
400	399	a1i	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((1 \dots N) \times \{k\}) : (1 \dots N) ⟶ \{k\}$
401	398 318 400 317 317 274	off	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ [0, 1]$
402	401	ffnd	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) Fn (1 \dots N)$
403	124 402	sylan	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \to ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) Fn (1 \dots N)$
404	368 403	jctild	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \to (\forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \to (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) Fn (1 \dots N) \land \forall m \in (1 \dots N) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c)))$
405	2	eleq2i	$⊢ (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in I \leftrightarrow (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in ({[0, 1]}^{(1 \dots N)})$
406		ovex	$⊢ [0, 1] \in V$
407	406 43	elmap	$⊢ (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in ({[0, 1]}^{(1 \dots N)}) \leftrightarrow ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ [0, 1]$
408	405 407	bitri	$⊢ (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in I \leftrightarrow ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) : (1 \dots N) ⟶ [0, 1]$
409	401 408	sylibr	$⊢ ((φ \land k \in ℕ) \land j \in (0 \dots N)) \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in I$
410	124 409	sylan	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in I$
411	404 410	jctird	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \to (\forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \to ((((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) Fn (1 \dots N) \land \forall m \in (1 \dots N) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c)) \land (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in I))$
412		elin	$⊢ (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I) \leftrightarrow ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \land (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in I)$
413		ovex	$⊢ (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in V$
414	413	elixp	$⊢ (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \leftrightarrow (((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) Fn (1 \dots N) \land \forall m \in (1 \dots N) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c))$
415	414	anbi1i	$⊢ ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \land (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in I) \leftrightarrow ((((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) Fn (1 \dots N) \land \forall m \in (1 \dots N) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c)) \land (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in I)$
416	412 415	bitri	$⊢ (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I) \leftrightarrow ((((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) Fn (1 \dots N) \land \forall m \in (1 \dots N) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c)) \land (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in I)$
417	411 416	imbitrrdi	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \to (\forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I))$
418		ssel	$⊢ ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v \to ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I) \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v)$
419	418	com12	$⊢ (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I) \to (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v)$
420	417 419	syl6	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \to (\forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \to (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v))$
421	420	impd	$⊢ ((((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \land j \in (0 \dots N)) \to ((\forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \land ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v) \to (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v)$
422	421	ralrimdva	$⊢ (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to ((\forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \land ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v) \to \forall j \in (0 \dots N) (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v)$
423	422	expd	$⊢ (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to (\forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \to (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v \to \forall j \in (0 \dots N) (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v))$
424	8	3exp2	$⊢ φ \to (k \in ℕ \to (n \in (1 \dots N) \to (r \in \{\leq \leq^{-1}\} \to \exists j \in (0 \dots N) 0 r X)))$
425	424	imp43	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land r \in \{\leq \leq^{-1}\})) \to \exists j \in (0 \dots N) 0 r X$
426		r19.29	$⊢ (\forall j \in (0 \dots N) (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \land \exists j \in (0 \dots N) 0 r X) \to \exists j \in (0 \dots N) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \land 0 r X)$
427		fveq2	$⊢ z = (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \to F (z) = F ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}))$
428	427	fveq1d	$⊢ z = (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \to F (z) (n) = F ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\})) (n)$
429	428 5	eqtr4di	$⊢ z = (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \to F (z) (n) = X$
430	429	breq2d	$⊢ z = (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \to (0 r F (z) (n) \leftrightarrow 0 r X)$
431	430	rspcev	$⊢ ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \land 0 r X) \to \exists z \in v 0 r F (z) (n)$
432	431	rexlimivw	$⊢ \exists j \in (0 \dots N) ((1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \land 0 r X) \to \exists z \in v 0 r F (z) (n)$
433	426 432	syl	$⊢ (\forall j \in (0 \dots N) (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \land \exists j \in (0 \dots N) 0 r X) \to \exists z \in v 0 r F (z) (n)$
434	433	expcom	$⊢ \exists j \in (0 \dots N) 0 r X \to (\forall j \in (0 \dots N) (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \to \exists z \in v 0 r F (z) (n))$
435	425 434	syl	$⊢ ((φ \land k \in ℕ) \land (n \in (1 \dots N) \land r \in \{\leq \leq^{-1}\})) \to (\forall j \in (0 \dots N) (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \to \exists z \in v 0 r F (z) (n))$
436	435	ralrimdvva	$⊢ (φ \land k \in ℕ) \to (\forall j \in (0 \dots N) (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
437	122 436	sylan2	$⊢ (φ \land (c \in ℝ^{+} \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)})) \to (\forall j \in (0 \dots N) (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
438	437	anassrs	$⊢ ((φ \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to (\forall j \in (0 \dots N) (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
439	438	adantllr	$⊢ (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to (\forall j \in (0 \dots N) (1^{st} (G (k)) +_{f} ((2^{nd} (G (k)) [(1 \dots j)] \times \{1\}) \cup (2^{nd} (G (k)) [(j + 1 \dots N)] \times \{0\}))) \div_{f} ((1 \dots N) \times \{k\}) \in v \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
440	423 439	syl6d	$⊢ (((φ \land C \in I) \land c \in ℝ^{+}) \land k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)}) \to (\forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \to (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
441	440	rexlimdva	$⊢ ((φ \land C \in I) \land c \in ℝ^{+}) \to (\exists k \in ℤ_{\geq (- ⌊- \frac{2}{c}⌋)} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{- ⌊- \frac{2}{c}⌋})) \to (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
442	74 441	syld	$⊢ ((φ \land C \in I) \land c \in ℝ^{+}) \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
443	442	com23	$⊢ ((φ \land C \in I) \land c \in ℝ^{+}) \to (⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
444	443	impr	$⊢ ((φ \land C \in I) \land (c \in ℝ^{+} \land ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v)) \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
445	51 444	sylanl2	$⊢ ((φ \land (v \in (R ↾_{𝑡} I) \land C \in v)) \land (c \in ℝ^{+} \land ⨉_{m = 1}^{N} (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) c) \cap I \subseteq v)) \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
446	35 445	rexlimddv	$⊢ (φ \land (v \in (R ↾_{𝑡} I) \land C \in v)) \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
447	446	expr	$⊢ (φ \land v \in (R ↾_{𝑡} I)) \to (C \in v \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
448	447	com23	$⊢ (φ \land v \in (R ↾_{𝑡} I)) \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to (C \in v \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
449		r19.21v	$⊢ \forall n \in (1 \dots N) (C \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)) \leftrightarrow (C \in v \to \forall n \in (1 \dots N) \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
450	448 449	imbitrrdi	$⊢ (φ \land v \in (R ↾_{𝑡} I)) \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \forall n \in (1 \dots N) (C \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
451	450	ralrimdva	$⊢ φ \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \forall v \in (R ↾_{𝑡} I) \forall n \in (1 \dots N) (C \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$
452		ralcom	$⊢ \forall v \in (R ↾_{𝑡} I) \forall n \in (1 \dots N) (C \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)) \leftrightarrow \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (C \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n))$
453	451 452	imbitrdi	$⊢ φ \to (\forall i \in ℕ \exists k \in ℤ_{\geq i} \forall m \in (1 \dots N) (1^{st} (G (k)) \div_{f} ((1 \dots N) \times \{k\})) (m) \in (C (m) ball ({(abs \circ -) ↾}_{ℝ^{2}}) (\frac{1}{i})) \to \forall n \in (1 \dots N) \forall v \in (R ↾_{𝑡} I) (C \in v \to \forall r \in \{\leq \leq^{-1}\} \exists z \in v 0 r F (z) (n)))$

Metamath Proof Explorer

Theorem poimirlem29

Proof